CN101266571A - Credible password module test case creation method and its test system - Google Patents

Abstract

The invention discloses a method for generating a test case of a trusted cryptographic module and a test system thereof, belonging to the technical field of computers. The method of the present invention is: modeling inside the subsystem divided by trusted cryptographic modules, generating the extended finite state machine of the subsystem, and then generating test cases by extending the finite state machine; the test system of the present invention includes: a script analysis engine , results analysis engine and communication module. Compared with the prior art, the test case of the present invention can be generated in an automated manner, which avoids the problem that the manual test case cannot guarantee the integrity of the test and thus the reliability of the test result is not high, and the present invention provides The system is an automated test system, which reduces some manual intervention and saves costs.

Description

A test case generation method and test system for a trusted cryptographic module

technical field

The invention relates to a testing method of an embedded system and a system thereof, in particular to a method for generating a test case of a trusted cryptographic module and a testing system thereof, belonging to the technical field of computers.

Background technique

Trusted computing platform technology is a new technology to solve security problems through hardware root of trust. Trusted platform module (TPM) is the core and foundation of trusted computing platform, and is the key to the promotion and application of trusted computing platform. The development and application of the trusted computing platform are inseparable from the corresponding technical specifications. In order to promote the development of the trusted computing platform, in 2003, the Trusted Computing Group (TCG) gave the trusted platform module (Trusted PlatformModuel, TPM for short) 1.2 specification defines the functions of TPM in detail. At the same time, in order to promote the development of the domestic trusted computing platform industry, the National Commercial Cryptography Management Office released the relevant standards of the domestic trusted cryptographic module (Trusted Cryphographic Module, referred to as TCM), which defined the functions of the domestic TCM in detail. It laid the foundation for the development of the trusted computing platform in China.

In terms of formal analysis and modeling of trusted platform modules, Matthew Barrett formally analyzed some key security mechanisms of TPM, and the models he established are mainly used for security analysis. At the same time, Danilo Bruschi and others conducted a formal analysis of the TPM authorization protocol, and analyzed the attack methods of the protocol through model detection technology.

The test method and test system of the trusted cryptographic module conduct comprehensive and complete tests on the functions and compliance requirements of the trusted cryptographic module, and a complete solution is needed to support the implementation of the test. Ahmad-Reza Sadeghi et al. gave a detailed test plan and test results for TPM, and analyzed the test results in detail.

All these analysis and testing methods for TPM or TCM do not give a complete system, and do not give a way how to generate test cases from specifications.

Contents of the invention

Aiming at the test requirements of trusted cryptographic modules, the present invention provides a method for generating test cases of trusted cryptographic modules and a testing system thereof, which uses extended finite state machines to model trusted cryptographic modules, and then expands finite state The test case is generated by the computer, and the test case is input into the test system to carry out a complete test on the trusted cryptographic module. The present invention improves the accuracy and coverage of the test. The method and system proposed by the present invention can solve the following problems:

(1) Formal modeling of trusted cryptographic modules

At present, the TCM specification given by the National Commercial Encryption Management Office is descriptive, which is easy to cause ambiguity and is not conducive to product development. Therefore, it is very necessary to provide an accurate formal model, and an accurate formal model can give TCM functions Verification, analysis, and formal testing provide the basis.

(2) Quantity and quality of test cases for conformance testing

At present, the test cases for trusted cryptographic modules are all done manually, and the biggest problem of manual testing is that the integrity and coverage of the test cannot be solved, resulting in low credibility of the test results. In addition, the validity of test cases will directly affect the test efficiency and test cost of TCM. How to realize the automatic generation of test cases becomes an urgent problem to be solved.

(3) The testing of trusted cryptographic modules lacks the support of automated testing schemes

Because the TCM specification involves a wide range of content, purely manual testing requires a lot of manpower and material resources, and there is an urgent need for an automated testing solution to support the automation of testing and provide a corresponding support system.

The steps of the test case generation method include:

1. Division of trusted cryptographic module systems

The trusted cryptographic module is a complete information system, which is composed of multiple interrelated but not very close systems. First, it is divided according to the functions of the trusted cryptographic module system, and the dependencies of each subsystem after division are established. picture. The granularity of division depends on the specific situation;

2. Generation of extended finite state machines for subsystems

On the basis of the division of the subsystems in the first step, the internal modeling of the system is carried out for each subsystem, the relationship between each command is established, and the extended finite state machine of the subsystem is generated;

3. Generation of test cases

Generate test cases based on the generated extended finite state machine.

Preferably, in step 2, the extended finite state machine can be generated using the following steps and methods

1) Divide the internal state of the subsystem to form the internal state of the subsystem;

2) Establish the execution sequence dependency graph between the commands in the subsystem,

3) According to the state in the subsystem, starting from the initial state, according to the execution order of the commands, apply an executable command on the corresponding state to cause state migration, thereby extracting the migration path;

4) According to the states and migration paths generated in steps 1) and 3), an extended finite state machine can be formed.

Preferably, the state division in step 1) can adopt a type-based state division method, and the state extraction method is described as follows:

Let the state variables that determine the state space be x _{1 .xi} .x _n , A ₁ ..A _j ..A _l , where _xi represents a single-valued variable whose types are T ₁ ,...,T _n , and A _j is a set variable, and the element types in the set are TT ₁ ,..., TT ₁ (the type determines the value space of the variable, and the present invention does not distinguish type and value space)

(a) The initial state space is

(b) Subdivision of states

The following subdivides the state according to the state variables:

■Single value variable

Based on a certain strategy, the value of the single-valued variable x _i is divided, such as boundary value analysis method and category division method. In this way, the state can be further subdivided. Based on the strategy policy, the division of the state S with respect to the state variable x _i is defined as:

Among them, AS _j represents the sub-state of state S subdivided by state variable x _i , and P _j is the predicate logic that constrains variable x _i , such as x _i ＞=0; AS _j1 (xi ₎ represents the state in state AS _j1 The value space of variable x _i .

■Collection variable

For set variables, use the type-based partition method to divide the state space, first define the concept of set partition:

Definition 3.2 Suppose A is a non-empty set, if there is a subset family π of A, satisfy the following conditions:

2) Any two elements in π are disjoint;

3) The union of all elements in π is equal to A;

Then π is called a partition of the set A.

■ Combined state variables

If the internal state variables include both single-valued variables x ₁ , ... x _n , and set variables A ₁ , ..., A _l , then the final state space is a complete combination of variables. The state number obtained is

$\underset{\mathrm{<span\; class="notranslate">\; i</span>}<span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; 1</span>}<span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; j</span>}<span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; 1</span>}}{\overset{\mathrm{<span\; class="notranslate">\; i</span>}<span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; no</span>}<span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; j</span>}<span\; class="notranslate">\; =</span>\mathrm{<span\; class="notranslate">\; 1</span>}}{\mathrm{<span\; class="notranslate">\; \&Pi;</span>}}}{\mathrm{<span\; class="notranslate">\; m</span>}}_{\mathrm{<span\; class="notranslate">\; i</span>}}<span\; class="notranslate">\; \&times;</span><span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; 2</span>}}^{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; 1</span>}<span\; class="notranslate">\; )</span>$

(c) Reduction of state

From the above analysis, it can be seen that if the number of state variables is large, the existing state space will increase sharply. One solution is to control the division granularity of each state variable in the step of state subdivision; another One solution is to limit the final state space according to requirements (such as test requirements). The following describes the type-based state division method through the extraction of TCM states.

Preferably, the following function-based set division method can be used in step (b).

If there is a function f from a set T to a type V: T→V, and the type V is a finite set, ran(f)={v ₁ , v ₂ ...v _n }. Then the function value division of type T

$\mathrm{<span\; class="notranslate">\; \&pi;</span>}<span\; class="notranslate">\; =</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; 2</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; no</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; \}</span><span\; class="notranslate">\; .</span>$

Therefore, the function f can divide the state S according to the state set variable A _j , and the divided result is:

$\mathrm{<span\; class="notranslate">\; Partition</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; S</span>}<span\; class="notranslate">\; ,</span>{\mathrm{<span\; class="notranslate">\; A</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}<span\; class="notranslate">\; ,</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span><span\; class="notranslate">\; \{</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; ,</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; ,</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; |</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; \&Element;</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; A</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; A</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; \&Element;</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; A</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; BS</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; (</span>{\mathrm{<span\; class="notranslate">\; A</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; \}</span>$

Where BS ₁ (A _j ) represents the set of elements of type TT _j in the value space of the set variable A _j in state BS ₁ . Each partition is combined with each other to obtain the final state space. The number of state spaces obtained by combining states between partitions is:

${\mathrm{<span\; class="notranslate">\; C</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}^{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; +</span>{\mathrm{<span\; class="notranslate">\; C</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}^{\mathrm{<span\; class="notranslate">\; 2</span>}}<span\; class="notranslate">\; +</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; +</span>{\mathrm{<span\; class="notranslate">\; C</span>}}_{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}^{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; 2</span>}}^{{\mathrm{<span\; class="notranslate">\; k</span>}}_{\mathrm{<span\; class="notranslate">\; j</span>}}}<span\; class="notranslate">\; -</span>\mathrm{<span\; class="notranslate">\; 1</span>}<span\; class="notranslate">\; .</span>$

Preferably, when generating test cases in step 3, test cases can be generated according to status or migration criteria.

The test system mainly includes:

1. Script analysis engine: analyze and analyze the script describing the test case, and execute the script by calling the command of the trusted cryptographic module;

2. Result analysis engine: analyze the results generated by the test, generate appropriate statistical data and statistical reports, and generate comprehensive report documents;

3. Communication module: communicate with trusted cryptographic modules and databases.

Preferably, the test script language recognized by the script analysis engine adopts a procedural language, and the specific script language can be designed and implemented by itself.

Preferably, the trusted cryptographic module and the test system can be distributed on different networks, and the communication module completes data interaction and collection.

The generated test cases are input into the test system (in the form of scripts), and the test cases can be tested by the script analysis engine to interpret and execute the test cases.

Positive effect of the present invention:

After adopting the invention, the test case can be generated in an automatic manner, avoiding the problem that the manual test case cannot guarantee the integrity of the test and thus the reliability of the test result is not high. Moreover, the system provided by the present invention is an automatic test system, which reduces some manual interventions and saves costs.

Description of drawings

Fig. 1 is a trusted cryptographic module test case generation method;

Figure 2 is the system abstract state and initialization definition;

Figure 3 is the operation mode of key generation, loading, and loading;

Figure 4 is the encapsulation and decapsulation operation mode;

Fig. 5 is the extraction algorithm of state transition;

Figure 6 is an EFSM diagram of the codon system;

Fig. 7 is a structural diagram of a trusted cryptographic module testing system;

FIG. 8 is a dependency diagram of each subsystem of the TCM;

Figure 9 shows the command dependencies within the cryptosystem.

Detailed ways

Specific embodiments of the present invention will be described in detail below in conjunction with the accompanying drawings.

First, divide the subsystems of the trusted cryptographic module, and strictly divide them according to the functions realized by each subsystem, so that the dependence of each partitioned subsystem is low; here, the trusted cryptographic module can be divided into the following subsystems: cryptographic subsystem , TCM management subsystem, platform identity management subsystem, storage protection subsystem, identification and authentication subsystem, integrity protection subsystem, trusted path subsystem.

The dependency relationship between various subsystems is shown in Figure 8, where the arrow points to indicate the dependency relationship, for example, the cryptographic subsystem points to the integrity protection subsystem, indicating that the cryptographic subsystem depends on the integrity protection subsystem.

Secondly, EFSM modeling is carried out for each subsystem respectively. The cryptographic subsystem of the trusted cryptographic module is used as an example to illustrate the method of generating test cases, and the cryptographic subsystem of TCM is used as the object of modeling.

In the specific modeling process, due to the complex specific data structure specified in the TCM specification, a certain degree of data abstraction is required. From the status point of view, the initial state of the TCM is that the owner identity (Take Owner) has been established, and the relevant information of the key will be stored in the TCM, the most important is the handle of the key and the attributes of the key (such as type ), introduce the following abstract data types and global variables.

[KeyHandle, KeyType]

maxcount: N;

KeyType: =TCM_STORAGE|TCM_SIGN|TCM_BIND;

Among them, KeyHandle is the handle type of the TCM internal key; KeyType is the type of the key, and there are three different key types.

From the operation point of view, there are mainly operations such as creating keys, destroying keys, and using keys. The description of the abstract state of the cryptographic subsystem and the definition of system initialization is shown in Figure 2, where the function keyHasType maps key handles to different key types. Initially, there is a storage root key SRK inside the TCM. Key generation, loading, and loading out operation modes are shown in Figure 3.

Figure 4 shows the TCM encapsulation operation and the operation mode of the decapsulation operation. Other operations related to the TCM key such as decryption and signature operations can be given in a similar form.

The corresponding extended finite state machine (EFSM) diagram is given below through state division and transition extraction. The states within the cryptosystem are partitioned according to the abstract states described by the Z-spec.

1. The division of states in the cryptosystem

In the Z language specification shown in Figure 2 and Figure 3, there is only one set variable keys, and there is a constraint function keyHasType.

(1) The first step: give the initial state

${\mathrm{<span\; class="notranslate">\; S</span>}}_{\mathrm{<span\; class="notranslate">\; Initial</span>}}\stackrel{\mathrm{<span\; class="notranslate">\; \&Delta;</span>}}{<span\; class="notranslate">\; =</span>}<span\; class="notranslate">\; \{</span>\mathrm{<span\; class="notranslate">\; keys</span>}<span\; class="notranslate">\; |</span><span\; class="notranslate">\; \#</span>\mathrm{<span\; class="notranslate">\; keys</span>}<span\; class="notranslate">\; \&le;</span>\mathrm{<span\; class="notranslate">\; max</span>}\mathrm{<span\; class="notranslate">\; count</span>}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; ;</span>$

(2) The second step: subdivision of state (collection variables)

Partition(S _Initial , keys, keyHasType) = {S _Sign , S _Storage , S _Bind }

All element key handles in S _sign are signature keys, and other definitions are similar.

(3) The third step: Combination of states

Number of state combinations $\mathrm{no}=C_3^2+C_3^1+C_3^3=2^{\mathrm{no}}-1=7$

So the final state given is:

s ₁ ={S _Sign }, s ₂ ={S _Storage }, s ₃ ={S _Bind }, s ₄ ={S _Sign ,S _Storage }, s ₅ ={S _Storage ,S _Bind },

s ₆ ={S _Bind , S _Sign }, s ₇ ={S _Bind , S _Sign , S _Storage }

(4) The fourth step: state reduction

If the constraints $P\left(S\right)\stackrel{\mathrm{\&Delta;}}{=}\left\{S\right|\&ForAll;\mathrm{key}\&Element;\mathrm{keys},\mathrm{keyHasType}\left(\mathrm{key}\right)=\mathrm{TCM}\_\mathrm{SIGN}\},$ The state space can be reduced to four, which are s ₁ , s ₄ , s ₆ , and s ₇ .

2. Establish command dependencies within the cryptosystem

The command dependencies are shown in Figure 9, where the arrows point to identify the dependencies, for example, TCMSeal points to TCMlocalkey, indicating that TCMSeal depends on TCMlocalkey.

3. Migration extraction

Fig. 5 shows the extraction algorithm of state transition.

where def(s)={key|key∈s}, S is the set of internal states, OP represents the set of TCM operations, in the cryptographic subsystem,

OP={TCMCreateKey, TCMLoadKey, TCMEvictKey, TCMSeal,

TCMUnSeal, TCMSign, TCMVerify, TCMEncrypt, TCMDecrypt}

4. The final EFSM diagram is shown in Figure 6:

See Table 1 and Table 2 for specific state meanings and state transitions. Tables 1 and 2 only show the migration of one of the paths, and the migration of other paths is similar. In the migration mark (sx, P/op, y->s'), s represents the current state, x' represents the state after migration, x represents the input, P represents the condition of the transfer, op represents the operation in the transfer, y Indicates the output. The symbols involved are: input variable set: x _tag , x _ordinal , x _KeyHandle , x _keyType ; output variable set: y _tag , y _retValue , y _ordinal , y _keyHandle , y _keyType . The input commands include: TCM_CWK (generating a key), TCM_EK, TCM_LK, TCM_UB, TCM_Seal, TCM_UnSeal, TCM_Sign, and the symbol y _tag (value) means assigning a value to the variable y _tag . Environment variable and global variable collection: keys (handle collection in TCM), etc.

Table 1 EFSM status description

state describe state describe s ₀ Initial state, already TakeOwner, has SRK, and TCM is enabled, in the s1 operation state of TCM s ₁ Inside the TCM are encryption keys s ₂ Inside the TCM is the signature key s ₃ Inside the TCM are storage keys s ₄ Both encryption key and storage key s ₅ There are both signing keys and storage keys inside s ₆ Both encryption key and signing key s ₇ There are encryption key, signature key and storage key at the same time

Table 2 State Transition Table

state transition describe t1 {s ₀ -TCM_CWK, P _t3 /<y _retValue (0), y _ordinal (TCM_CWK), y _tag (RspTag), y _keyType (x _keyType )>, 0->s ₀ } where P _t3 = x _tag (auth1Tag ), x _keyHandle ∈ keys) t2, t6, t11 {s ₂ (s ₅ , s ₇ )-TCM_EK, P _t2 /<y _retValue (0), y _ordinal (TCM_EK), y _tag (RSPTag)>, 0->s ₀ (s ₂ , s ₅ )} where P _t2 =< x _tag (reqAuth), x _keyHandle ∈ keys > t3, t5, t10 {s ₀ (s ₂ , s ₅ )-TCM_LK, P _t3 /<y _retVatue (0), y _ordinal (TCM_LK), y _tag (resAuth1)>, its 0->s ₂ (s ₅ , s ₇ )} where P _t3 = (x _tag (reqAuth1), x _pkeyHandle ∈ keys, x _keyType (SignKey)) t4, t7, t12 {s ₂ (s ₅ , s ₇ )-TCM_Sign, P _t16 /<y _tag (rspAuth2), y _retValue (0), y _ordinal (TCM_Sign)>, 0->s ₂ (s ₅ , s ₇ )} where P _t16 = (x _tag (reqAuth2)) t8, t13 {s ₅ (s ₇ )-TCM_Seal, P _t10 /<y _tag (rspAuth1), y _retValue (0)>, 0->s ₅ (s ₇ )} where P _t10 = (x _tag (reqAuth1), x _keyHandle ∈keys∧x _keyType (TCM_STORAGE)) t9, t14 {s ₅ (s ₇ )-TCM_UnSeal, P _t11 /<y _tag (rspAuth2), y _retValue (0), y _ordinat (TCM_UnSeal)>, 0->s ₅ (s ₇ )} where P _t11 = x _tag ( reqAuth2)) t15 {s ₇ -TCM_UB, P _t9 /<y _tag (repAuth1), y _retVatue (0), y _ordinal (TCM_UB)>, 0->s ₇ } where P _t9 = (x _tag (reqAuth1), x _KeyHandle ∈ keys )

Finally, the corresponding test case is generated through the EFSM diagram, and the generation of the test case follows the generation method proposed by C.Bourhfir [Reference: Automatic executable test case generation for EFSM specified protocols, C.Bourhfir, R.Dssouli, E.Aboulhamid, and N. Rico, IWTCS '97, pp.75-90, 1997].

The software implementation structure of the test system is shown in Figure 7. The system interacts with the trusted cryptographic module through the TDDL module. The test system, database, and trusted cryptographic module can be distributed in different networks and communicate through network communication protocols.

Claims (10)

1. A test case generation method of a trusted cryptographic module, the steps of which are: 1) Divide the trusted cryptographic module into multiple subsystems; 2) Establish the command dependencies within the subsystem, thereby generating the extended finite state machine of the subsystem; 3) Generate the test case of the subsystem according to the generated extended finite state machine. 2. The method according to claim 1, wherein the subsystems are divided according to the functions of each system in the trusted cryptographic module system; the subsystems include: a cryptographic subsystem, a TCM management subsystem, and a platform identity management subsystem System, Storage Protection Subsystem, Identification and Authentication Subsystem, Integrity Protection Subsystem, Trusted Path Subsystem. 3. The method according to claim 1, characterized in that the command dependency relationship within the subsystem is established according to the command execution sequence within the subsystem. 4. The method according to claim 3, characterized in that the extended finite state machine generating method of the subsystem is: 1) Divide the state in the trusted cryptographic module subsystem to form the internal state of the subsystem; 2) According to the command dependencies inside the subsystem and the internal state of the subsystem, a migration path between states is formed; 3) Extract the migration path according to the relationship between the generated states; 4) Generate an extended finite state machine according to the internal state of the subsystem and the extracted transition path. 5. The method according to claim 4, wherein the method for dividing the state in the trusted cryptographic module subsystem is: 1) The initial state space is:

Among them, x ₁ .x _i .x _n , A ₁ ..A _j ..A _l are the state variables that determine the state space, and _xi represents a single-valued variable whose types are T ₁ ,..., T _n , A _j is a set variable, and the element types in the set are TT ₁ ,..., TT _l ; 2) Divide the state according to the different state variables; 3) Combining the divided state variables; 4) Reduce the combined state variables according to the constraints. 6. The method according to claim 5, characterized in that the single-valued variables are divided into state values using a division method based on strategy policy; the set variables are divided into state spaces using a type-based division method . 7. method as claimed in claim 5 is characterized in that adopting the set division method based on function to carry out the division of state space to described set variable: by the function f of set T to type V: T→V, and type V is Finite set, ran(f)={v ₁ , v ₂ ...v _n }, then the function values of type T are divided into: $\mathrm{<span\; class="notranslate">\; \&pi;</span>}<span\; class="notranslate">\; =</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; 1</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; 2</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; .</span><span\; class="notranslate">\; ,</span><span\; class="notranslate">\; \{</span><span\; class="notranslate">\; \&ForAll;</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; :</span>\mathrm{<span\; class="notranslate">\; T</span>}<span\; class="notranslate">\; |</span>\mathrm{<span\; class="notranslate">\; f</span>}<span\; class="notranslate">\; (</span>\mathrm{<span\; class="notranslate">\; t</span>}<span\; class="notranslate">\; )</span><span\; class="notranslate">\; =</span>{\mathrm{<span\; class="notranslate">\; v</span>}}_{\mathrm{<span\; class="notranslate">\; no</span>}}<span\; class="notranslate">\; \}</span><span\; class="notranslate">\; \}</span><span\; class="notranslate">\; .</span>$ 8. The method according to claim 1, characterized in that the test case generation method proposed by C.Bourhfir is followed when the test case of the subsystem is generated according to the extended finite state machine generated. 9. A test system for detecting a test case as claimed in claim 1, comprising Script parsing engine: analyze the script describing the test case, and parse it, call the command of the trusted cryptographic module to execute the script; Result analysis engine: analyze the results generated by the test, generate statistical data and statistical reports, and generate comprehensive report documents; Communication module: communicate with trusted cryptographic modules and databases. 10. The system according to claim 9, wherein the test script language recognizable by the script analysis engine is a procedural language.

Images