A Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols

Simple item page
dc.creatorRaúl Monroy Borja
dc.date2007
dc.date.accessioned2018-10-18T22:08:24Z
dc.date.available2018-10-18T22:08:24Z
dc.descriptionThe 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 [Gavin Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. In TACAs'96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pages 147-166, London, UK, 1996. Springer-Verlag] and OFMC [A.D. Basin, S. Mödersheim, and L. Viganò. An on-the-fly model-checker for security protocol analysis. In D. Gollmann and E. Snekkenes, editors, ESORICS'03: 8th European Symposium on Research in Computer Security, number 2808 in Lecture Notes in Computer Science, pages 253-270, Gjøvik, Norway, 2003. Springer-Verlag]; and ii) theorem proving, e.g. the Isabelle inductive method [Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal in Computer Security, 6(1-2):85-128, 1998] and Coral [G. Steel, A. Bundy, and M. Maidl. Attacking the asokan-ginzboorg protocol for key distribution in an ad-hoc bluetooth network using coral. In H. König, M. Heiner, and A. Wolisz, editors, IFIP TC6 /WG 6.1: Proceedings of 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems, volume 2767, pages 1-10, Berlin, Germany, 2003. FORTE 2003 (work in progress papers)]. 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 [M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6-15, 1996]. 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 [J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. Technical report, Department of Computer Science, University of York, November 1997. A complete specification of the Clark-Jacob library in CAPSL is available at http://www.cs.sri.com/millen/capsl/]. © 2007.
dc.identifier.doi10.1016/j.entcs.2006.12.034
dc.identifier.endpage130
dc.identifier.issn15710661
dc.identifier.issue4
dc.identifier.startpage117
dc.identifier.urihttp://hdl.handle.net/11285/630573
dc.identifier.volume174
dc.languageeng
dc.relationhttps://www.scopus.com/inward/record.uri?eid=2-s2.0-34249097180&doi=10.1016%2fj.entcs.2006.12.034&partnerID=40&md5=0e801aa21e8f8d1e1e9e97bc4f7d147f
dc.relationInvestigadores
dc.relationEstudiantes
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0
dc.sourceElectronic Notes in Theoretical Computer Science
dc.subjectAuthentication
dc.subjectElectric fault location
dc.subjectMathematical models
dc.subjectNetwork protocols
dc.subjectSoftware engineering
dc.subjectFormal methods
dc.subjectFormal verification
dc.subjectMobile security
dc.subjectTheorem proving
dc.subjectVerification
dc.subjectReplay attacks
dc.subjectSecurity protocols
dc.subjectNetwork security
dc.subjectNetwork security
dc.subjectCryptographic protocols
dc.subjectEngineering practices
dc.subjectFault localization
dc.subjectInductive method
dc.subjectpatching
dc.subjectReplay attack
dc.subjectSecurity protocols
dc.subjectState exploration
dc.subject.classification7 INGENIERÍA Y TECNOLOGÍA
dc.titleA Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols
dc.typeArtículo
refterms.dateFOA2018-10-18T22:08:24Z

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
34249097180.pdf
Size:
100.69 KB
Format:
Adobe Portable Document Format
Description:
Artículo
Download

Collections

Artículo
logo

El usuario tiene la obligación de utilizar los servicios y contenidos proporcionados por la Universidad, en particular, los impresos y recursos electrónicos, de conformidad con la legislación vigente y los principios de buena fe y en general usos aceptados, sin contravenir con su realización el orden público, especialmente, en el caso en que, para el adecuado desempeño de su actividad, necesita reproducir, distribuir, comunicar y/o poner a disposición, fragmentos de obras impresas o susceptibles de estar en formato analógico o digital, ya sea en soporte papel o electrónico. Ley 23/2006, de 7 de julio, por la que se modifica el texto revisado de la Ley de Propiedad Intelectual, aprobado

DSpace software copyright © 2002-2026

Licencia