A formal specification of mobile trusted computing

Trusted Computing provides a new way of protecting the mobile nodes from attacks. However, due to the complexity of specification of Trusted Computing and lack of formal methods, the security of mobile software design is still not guaranteed. In this paper, we propose a formal specification of mobile Trusted Computing (TC-Spec) by using the B method. TCSpec is a library which encapsulates the Trusted Computing and other secure related operations, and satisfies requirements of most mobile secure software. We give an example of using TCSpec in mobile routing protocols. Moreover, we make analysis and prove that the security of private information is preserved by using TCSpec in design of mobile software.