Maude-NPA

Repository of protocol specifications in Maude-NPA

Home Choice Protocols Distance-Bounding Protocols Hash Functions Vulnerabilities Contact and links

CCA-0 Protocol

The CCA-0 protocol is insecure, since it is subject to the attack found by Bond. As a result of the attack, the intruder obtains a PIN derivation key in clear, like in the IBM attack and, hence, can compute PINs from bank account numbers. This attack is the same found by Küesters and Truderungs.

Using the same assumptions in terms of the role played by the intruder and its knowledge, Maude-NPA finds the attack of the CCA-0 protocol after 7 steps of protocol analysis. Table 2 shows the sequence of exchanged messages with some explanations. Our analysis looks for e(PDK,PDK) instead of PDK, but the intruder can use the Decipher command with inputs e(PDK,PDK) and e(KM,PDK) and obtains PDK, which can be then used to obtain the PIN for any account number. Given an account number, the corresponding PIN is derived by encrypting the account number under PDK. Terms e(IMP * KP * KM, km1 * km2) and e(PIN * Km1 * Km2 * Km3, PDK) are part of the intruder’s knowledge, as assumed in Bond attack. Table 3 shows the numbers of states generated at each level of the backwards reachability analysis from an attack state stating whether the intruder can learn the expression e(PDK,PDK).

 

 

 

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