A method for patching interleaving-replay attacks in faulty security protocols

Juan Lopez-Pimentel, Raul Monroy, Dieter Hutter

In: R. Bloem (Hrsg.). Proceedings of First Workshop on Verification and Debugging. Workshop on Verification and Debugging (V&D-2006) befindet sich Associated with CAV 2006 August 21 Seattle WA United States Seiten 117-130 174 4 Electronic Notes in Theoretical Computer Science 2007.


The verification of security protocols has attracted a lot of interest in the formal methods community, yielding two main verification approaches: i) state exploration, e.g. FDR and OFMC and ii) theorem proving, e.g. the Isabelle inductive method and Coral. Complementing formal methods, Abadi and Needham's principles aim to guide the design of security protocols in order to make them simple and, hopefully, correct. We are interested in a problem related to verification but far less explored: the correction of faulty security protocols. Experience has shown that the analysis of counterexamples or failed proof attempts often holds the key to the completion of proofs and for the correction of a faulty model. In this paper, we introduce a method for patching faulty security protocols that are susceptible to an interleaving-replay attack. Our method makes use of Abadi and Needham's principles for the prudent engineering practice for cryptographic protocols in order to guide the location of the fault in a protocol as well as the proposition of candidate patches. We have run a test on our method with encouraging results. The test set includes 21 faulty security protocols borrowed from the Clark-Jacob library.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence