Maude-NPA

Repository of protocol specifications in Maude-NPA

Home
Denning–Sacco Otway-Rees Amended Needham Schroeder Wide Mouthed Frog Yahalom Carlsen’s Secret Key Initiator ISO 5-pass Authentication Woo and Lam Authentication Kao-Chow Kao-Chow with handshake key Kao-Chow with tickets Secret 06 & 07 Diffie-Hellman
Needham Schroeder Lowe ECB
Needham Schroeder Lowe XOR TMN Wired Equivalent Privacy Smart Cards (SK3)
IBM CCA CCA 0 CCA 0 Küesters IBM’s recommendations to avoid CCA-0’s attack Yubikey
PKCS#11
Choice Protocols Distance-Bounding Protocols Hash Functions Vulnerabilities Contact and links

CCA-0 version of Küesters and Truderung.

Küesters and Truderungs analyzed the CCA API protocols in ProVerif via a protocol transformation technique. However, this work does not support full exclusive-or capabilities and requires restricting the analysis to XOR-linear protocols. Because of this, they need to modify and transform by hand some of the CCA API commands. We will refer to protocols using these manually-modified commands as “XOR-linear versions” of that protocols. Küesters and Truderungs perform a second transformation, in order to obtain an equivalent protocol specification without associative-commutative operators. Such transformation allows the analysis of the transformed protocol specification in ProVerif, which does not support such class of operators. Since this second transformation is performed automatically and it is sound, we have not analyzed in Maude-NPA the protocol specifications obtained after applying this transformation. As we can see in Tables 4 and 5, the transformation of the CCA operators performed by hand by Küesters and Truderungs is as follows. The “KPI-First + KPI-Add/Middle” and “Key Part Import Last” API commands are the equivalent to the original “Key Part Import First”, “Key Part Import Middle” and “Key Part Import Last” commands. Note that now the “Key Translate” command re- quires two steps instead of one in the original version. All the other commands remain the same without any transformation.

We have specified and analyzed in Maude-NPA the transformed version of the CCA-0 protocol described above. In Table 6 we have compared the results of this transformed protocol with the original protocol. In this table, “CCA-0” denotes the original protocol and “CCA-0-XOR-linear” denotes the protocol transformed by Küesters and Truderungs. As we can see in Table 6, both protocols find the initial state at the same depth of the backwards search tree. If the analysis is continued, the XOR-linear version produces a finite search space containing 2495 states in total. Since this protocol is a simplified version of the original protocol, the search space associ- ated to the original protocol is much much bigger and we have used some never patterns to reduce the search space. If the analysis is continued after depth 7 for the original protocol with never patterns, the search space is also finite while finding Bond’s attack. These never patterns are safe and do not interfere with the finiteness of the search space of the original protocol.

 

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