Introduction

Security requirements for real-life applications still increase. For this purpose, many people develop cryptographic protocols in order to fulfill these needs.

When someone designs a new protocol, he usually uses cryptographic tools for which he is confident. The design and the analysis of these tools is the domain of the mathematician and the cryptographer. In many cases, a cryptoalgorithm is proved as secure as solving hard problems (e.g., factoring large composite numbers). No such ``proofs'' exist for the cryptanalysis of protocols. By definition, a protocol designer must suspect everything. The use of strong cryptoalgorithms is not sufficient to guarantee the security of a protocol. In some situations, a protocol may be completely subverted without compromising the security of the underpinning cryptoalgorithm. Such situations are called protocol failures  [11].

Protocols are for example designed in order to establish a session key, to authenticate a transaction, to sign a document, etc... This is usually achieved by exchanging some messages between two or several people. In the sequel, we will show a failure on the most widely used public-key cryptosystem, the so-called RSA [13]. It may be briefly described as follows. Suppose that Alice wants to send a message m to Bob. To setup the system, Bob carefully selects two large primes p and q , computes $n_{\!B}=pq$, chooses a encryption key $e_{\!B}$ relatively prime to $\phi(n_{\!B})$, and computes the decryption key $d_{\!B}$ according to $e_{\!B} d_{\!B} \equiv 1 \pmod{\phi(n_{\!B})}$. The public key of Bob is the pair $(n_{\!B},e_{\!B})$ and his secret key is $d_{\!B}$. To send m to Bob, Alice forms the ciphertext $c=m^{e_{\!B}}\bmod{n_{\!B}}$ and sends it to Bob. Then, Bob recovers the plaintext by computing $m=c^{d_{\!B}} \bmod{n_{\!B}}$ with his secret key $d_{\!B}$. The security of this scheme relies on the intractability to factor $n_{\!B}$. The aim of a pirate, say Carol, is to recover m . This can be done as follows. Carol chooses a random number k , intercepts c , replaces it by $c'=ck^{e_{\!B}}\bmod{n_{\!B}}$, and sends c' to Bob. Now, when Bob deciphers c' , he obtains $m' \equiv (c')^{d_{\!B}} \equiv mk \pmod{n_{\!B}}$. Since m' is meaningless, Bob discards it. If Carol can get access to this discard, she finds $m=m'k^{-1} \bmod{n_{\!B}}$. This failure was first pointed out by Davida [5]. Avoiding this attack is easy, the users have to really destroy the discards, or in other words to protect their bins. The lesson of this failure is that the protocol designer has to pay attention to what is generally accepted but not explicitly stated.

   Figure 1: Davida's attack.

The decryption process can be speeded up by the Chinese Remainder Theorem (CRT). From p and q , Bob computes $m_p=c^{d_{\!B}\bmod{p-1}}\bmod{p}$ and $m_q=c^{d_{\!B}\bmod{q-1}}\bmod{q}$, and finally finds $m=\mathop{\mathrm{CRT}}(m_p,m_q)$ [12]. Suppose that Carol induces an external constraint on the deciphering device of Bob (e.g., ionizing or microwave radiation). Assume that the computation of $m_p$ is correctly performed but not computation of $m_q$. So, Bob gets $m'=\mathop{\mathrm{CRT}}(m_p,m'_q)$ instead of m . If Bob discards m' and if Carol can get access to m' , then she finds the secret factor p by computing $\gcd\bigl((m')^{e_{\!B}}-c \bmod{n_{\!B}}, n_{\!B}\bigr)$. Hence, $q=n_{\!B}/p$ and Carol can compute the secret decryption key $d_{\!B}$ [10,7].

   Figure 2: Lenstra's attack.

This second attack is more dangerous because it completely breaks the system. This shows clearly the importance of checking cryptographic protocols for faults [3]. Note also that if Bob protects his bin, the attack does not remain applicable.

The two previous attacks show that it is extremely difficult for a protocol designer to determine whether his protocol is sound, even for very simple protocols. Some researchers proposed formal techniques for analyzing the soundness of protocols, such as the BAN logic [4] or the three systems presented in [8].

Another approach for the protocol designer is to try to find flaws in his protocol with all his experience of good and bad practice. In [1], Abadi and Needham give general rules helping protocol designers to avoid many of the pitfalls (see also [2]). In this paper, we push their work further, and show that the protocol designers must also take care about the hardware and software implementation of the protocol.