Maude-NPA Protocols

IBM’s recommendations to avoid CCA-0’s attack

In order to prevent the attack of the CCA-0 protocol, IBM made two recommendations. In the first one, they argue that the attack would have to be carried out by an insider and that the vulnerability is intrinsic to public key schemes. IBM suggested that access control should be used to restrict any single insider from having access to a new command called “PKA Symmetric Key Import”, which implies the exchange of messages shown below.

The “PKA Symmetric Key Import” takes an encrypted data block containing the key to be imported, the corresponding type information and returns the key encrypted under the local master key. Therefore, IBM suggested two new versions of the CCA-0 protocol following this recommendation, namely CCA- 1A and CCA-1B. The difference between these versions and the original version is that they cannot handle the entire exclusive-or theory and because of that the original “Key Translate API operator” command is transformed into the “PKA Symmetric Key Import” command.

The second recommendation suggested by IBM to avoid the attack of the CCA-0 protocol was to use some role-based access control. Users of IBM’s 4758 HSM are assigned to roles that determine which commands they are allowed to execute. The goal is to prevent one single individual from having access to all the commands required to mount Bond’s attack. This is enforced using access controls. IBM provided an example of the KEK transfer process involving five roles (A-E) such that no single role is able to mount the attack, as shown in Table 7. For each role a new protocol version was proposed. We will consider three new protocol versions for roles B, C, and E, that will be referred as CCA-2B, CCA-2C, and CCA-2D, respectively.

In Table 8 we summarize which API commands can be accessed by each protocol. In the original attack, the intruder played the roles C and E together. Note that roles A and D do not have any access privileges at the destination security module. IBM stated in their recommendation that roles A and B could actually be played by the same individual.

CCA-1A Protocol

In this section, we explain the CCA-1A protocol, that restricts the kind of commands that certain rules may perform. This version of the protocol uses a subset of operations of the original CCA-0 protocol. Table 9 summarizes the result of the analysis of the protocol specified in Maude-NPA. Note that this protocol is XOR-linear and Ku ̈esters and Truderung do not transform it. The analysis of this protocol uses the same never patterns than CCA-0 and the search space is finite after depth 5, finding no initial state for Bond’s attack.

To download the complete protocol specification in Maude-NPA syntax click here

CCA-1B Protocol

This protocol is not XOR-linear and Küesters and Truderung manually transform it. In Tables 10 and 11 we can see the differences between the two CCA-1B protocols, the original and the XOR-linear versions. Table 12 summarizes the results of the analysis of both versions. As we can see, the XOR-linear version is extremely simple and the analysis is almost immediate in Maude-NPA. The analysis of the original CCA-1B protocol uses the same never patterns than CCA-0 and the search space is finite after depth 6, finding no initial state for Bond’s attack.

To download the complete protocol specification in Maude-NPA syntax of the CCA-1B protocol click here and for the CCA-1B-XOR-linear click here.

CCA-2B Protocol

This protocol follows the second recommendation of IBM that implements the role of person B, who enters the first key part into the destination security module as shown in Table 7. Table 13 summarizes the result of the analysis of the protocol specified in Maude-NPA. Note that this protocol is XOR-linear and Kü̈esters and Truderung do not transform it. The analysis of this protocol uses the same never patterns than CCA-0 and the search space is finite after depth 11, finding no initial state for Bond’s attack.

The protocol is secure against the attack that we could found in the original version and, when this protocol is analyzed with Maude-NPA, it generates a finite search state space finding no initial state.

To download the complete protocol specification in Maude-NPA syntax click here

CCA-2C Protocol

In this protocol version, the user enters the two clear key parts, using the “Random Number Generate” command, and the key verification pattern for the complete key encryption key (KEK). The first key part is given to roles B, the second to role C, and the verification pattern to roles C and E. Tables 14 and 15 show the origi- nal protocol and the XOR-linear version provided by Küesters and Truderungs. Table 16 summarizes the results of the analysis of both versions. As we can see, the XOR-linear version is simpler than the original protocol and, indeed, finds a finite search space earlier than the original protocol The analysis of the original CCA-2C protocol uses the same never patterns than CCA-0 and the search space is finite after depth 7, finding no initial state for Bond’s attack.

To download the complete protocol specification in Maude-NPA syntax of the CCA-2C protocol click here and for the CCA-2C-XOR-linear click here.

CCA-2E Protocol

In this section, we explain the analysis of the CCA-2E protocol, the fixed version of the CCA-0 following IBM’s second recommendation in which the role of person E verifies that the KEK is correct, and then imports the PDK (see Table 7). Table 17 summarizes the result of the analysis of the protocol specified in Maude- NPA. Note that this protocol is XOR-linear and Küesters and Truderung do not transform it. The analysis of this protocol uses the same never patterns than CCA-0 and the search space is finite after depth 6, finding no initial state for Bond’s attack.

To download the complete set of protocol specification in Maude-NPA syntax click HERE

Never Patterns

As shown in previous sections, the analysis of the original versions of the CCA-0, CCA-1A, CCA-1B, CCA-2A, CCA-2B, CCA-2C, and CCA-2E use some never patterns to obtain a reasonable analysis time and a finite search space. Never patterns can be used in Maude-NPA not only for authentication, but also to cut down the search space. Although never patterns can have a dramatic effect on search space size, they should be used with care, because improper use of never patterns can cause Maude-NPA to miss a genuine attack.

However, using never patterns to reduce search space size can be very useful in debugging protocols, since they allow the user to pinpoint weaknesses without performing a full-scale Maude-NPA search. If we had not used never patterns in the protocol analyses shown in previous sections, it would have been only a matter of time to find the desired initial state or find a finite search space, since these never patterns do not interfere with the finiteness of the search tree.

The aim of the never patterns used in the protocol analyses is to discard states in which the intruder learns any of the following message patterns.

Term PDK. Searching back for term PDK is pointless, since learning e(PDK, PDK) would allow the intruder to learn PDK.
Pattern e(Key, KM * Msg). Searching back for terms of the form e(Key, KM * Msg) is also pointless, since the master’s key is never given in plaintext. However, the automatic optimizations available in Maude-NPA for finding terms unreachable to the intruder cannot identify this pattern.
Pattern e(IMP * KM, Type * Key). Searching back for terms of the form e(IMP * KM, Type * Key) is likewise pointless, since the “Key Import” command assumes only a key, instead of a xor-expression with a type and a key. Note that Bond’s attack uses a type with more than one key, so they do not interfere with this pattern.
Pattern X * Y where X and Y are different from constants PIN, EXP and Km3. Let us explained then in detail. Searching back for terms of the form X ∗ Y is also pointless, since XOR-expressions using constants PIN, EXP and Km3 are used during Bond’s attack but any other xor- expression is irrelevant.