We reported in this paper a new algorithm for the formal automatic verification of authentication protocols. This algorithm does not necessitate any specification of any protocol property or invariant. It takes as parameter the protocol specification and generates the set of flaws, if any, as well as the corresponding attack scenarios. The algorithm involves three steps. First, protocol roles are extracted from the protocol specification. Second, the intruder abilities to perform communications and computations are generated from the protocol specification. In addition to the classical known intruder computational abilities such as encryption and decryption, we also consider those computations that result from different instrumentations of the protocol. The intruder abilities are modeled as a deductive proof system. Third, the extracted roles as well as the deductive system are combined to perform the verification. The latter 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 illustrated 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 discovered new unknown flaws in the Woo and Lam protocol and even in the corrected version of Abadi and Needham. A prototype of this verification algorithm has been implemented in BNR-Prolog.
As future work, we intend to lift this verification algorithm to deal with key-exchange cryptographic protocols. Actually, the same principles apply to these protocols. The two first steps of our verification algorithm remain unchanged. The only step that need to be accommodated is the third verification step. Here, we still continue working with the deductive proof system and the intruder knowledge to capture all the computation abilities of the intruder.