¡¡Chinese Journal of Computers   Full Text
  TitleThe Formal Analysis and Testing of Trusted Platform Module
  AuthorsCHEN Xiao-Feng
  Address(State Key Laboratory of Information Security, Institute of Software, Chinese Academy of Sciences, Beijng 100190)
(National Engineering Research Center of Information Security, Beijing 100190)
  Year2009
  IssueNo.4(646¡ª653)
  Abstract &
  Background 		Abstract Trusted platform module is the core component of trusted computing platform, the functional testing and validation is an important method to ensure the correctness and specification compliance of the trusted platform module, but until now, there is no valid formal testing and validation method, meanwhile the specification which is given by trusted computing group is descriptive, it is not convenient for product development and testing. The paper firstly analyzes the problem of the trusted platform module, and then gives the Z specification of TPM¡¯s cryptography system, based on this formal specification, gives the extended finite state machine model. Finally, the authors use the EFSM model for generating the test case and analyze the testing results.
Keywords trusted computing platform; trusted platform module; compliance testing; formal analysis
Background This work is supported by National Natural Science Foundation of China under grant No.60673083, No.60603017 and National Basic Research Program of China (973 Plan) under grant No.2007CB311202.
In trusted computing platform proposed by TCG group, the TPM is the core component the functional testing and validation is an important method to ensure the correctness and specification compliance of the trusted platform module, but until now, there is no valid formal testing and validation method, meanwhile the specification which is given by trusted computing group is descriptive, it is not convenient for product development and testing.
This paper firstly analyzes the problem of the trusted platform module, and then gives the Z specification of TPM¡¯s cryptography system, based on this formal specification, gives the extended finite state machine model. Finally, the authors use the EFSM model for generating the test case and analyze the testing results.