M. Debbabi
M. Mejri
N. Tawbi
I. Yahmadi
Computer Science Department,
Laval University, Quebec, G1K 7P4,
Canada.
{debabi,mejri,tawbi,yahmadi}@ift.ulaval.ca
We present a new formal automatic approach to the verification of authentication protocols. Our method could be applied without any prior specification of properties or invariant. It only needs the protocol specification from which it generates, if any, the set of possible flaws as well as the corresponding attack scenarios. This approach consists of three steps. First, the extraction of roles from the protocol specification. Second, the generation of a proof system that models the intruder abilities to perform communications and computations from the protocol specification. In addition to the classical known intruder computational abilities such as encryption and decryption, we also consider the computations that result from the possible instrumentations of the protocol. Third, the verification is performed according to the extracted roles as well as to the deductive system. This verification consists in checking whether the intruder can answer all the challenges uttered by a particular role. If it is the case, an attack scenario is automatically constructed. To exemplify the usefulness and efficiency of our approach, we illustrate it on Woo and Lam authentication protocol. Abadi and Needham have shown that the protocol is insecure and they proposed a new corrected version. In this paper, we present new unknown flaws in the Woo and Lam protocol as well as in its corrected version.
Keywords: Algorithm, Automatic Formal Verification, Cryptographic Protocols, Authentication, Proof System, Flaws, Attack Scenario.