Publication
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), located at Associated with CAV 2006, August 21, Seattle, WA, USA, Pages 117-130, Vol. 174, No. 4, Electronic Notes in Theoretical Computer Science, 2007.
Abstract
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.