An interpolation-based method for the verification of security protocols

Abstract

Interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. Security protocols, however, exhibit idiosyncrasies that make them unsuitable for the direct application of interpolation. We address this problem and present an interpolation-based method for security protocol verification. Our method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev–Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. We illustrate our method by means of concrete examples and discuss the results obtained by using a prototype implementation.

Keywords

Security protocols Craig interpolation symbolic execution verification

Get full access to this article

View all access options for this article.

References

Armando ,

Arsac ,

Avanesov ,

Barletta ,

Calvi ,

Cappai ,

Carbone ,

Chevalier ,

Compagna ,

Cuéllar ,

Erzse ,

Frau ,

Minea ,

Mödersheim ,

von Oheimb ,

Pellegrino ,

S.E.

Ponta ,

Rocchetto ,

Rusinowitch ,

Torabi Dashti ,

Turuani and

Viganò , The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures, in: TACAS,

Flanagan and

König , eds, LNCS 7214, Springer, 2012, pp. 267–282. doi:10.1007/978-3-642-28756-5_19. http://www.avantssar.eu.

Armando ,

Basin ,

Boichut ,

Chevalier ,

Compagna ,

Cuellar ,

Hankes Drielsma ,

P.-C.

Héam ,

Mantovani ,

Mödersheim ,

von Oheimb ,

Rusinowitch ,

Santiago ,

Turuani ,

Viganò and

Vigneron , The AVISPA tool for the automated validation of Internet security protocols and applications, in: CAV, LNCS 3576, Springer, 2005, pp. 281–285. doi:10.1007/11513988_27. http://www.avispa-project.org.

Armando ,

Carbone ,

Compagna ,

Cuéllar and

Tobarra , Formal analysis of SAML 2.0 Web browser single sign-on: Breaking the SAML-based single sign-on for Google apps, in: FMSE, ACM Press, 2008.

Armando and

Compagna , SATMC: A SAT-based model checker for security protocols, in: JELIA, LNAI 3229, Springer, 2004, pp. 730–733.

Armando ,

Pellegrino ,

Carbone ,

Merlo and

Balzarotti , From model-checking to automated testing of security protocols: Bridging the Gap, in: TAP, LNCS 7305, Springer, 2012, pp. 3–18.

AVANTSSAR, Deliverable 2.3 (update): ASLan

+ +

specification and tutorial, 2011, available at: http://www.avantssar.eu.

Basin ,

Mödersheim and

Viganò , OFMC: A symbolic model checker for security protocols, International Journal of Information Security 4(3) (2005), 181–208. doi:10.1007/s10207-004-0055-7. doi:10.1007/s10207-004-0055-7.

Blanchet , An efficient cryptographic protocol verifier based on prolog rules, in: CSFW, IEEE CS, 2001, pp. 82–96.

Boyd and

Mathuria , Protocols for Authentication and Key Establishment, Springer, 2010.

10.

Büchler ,

Oudinet and

Pretschner , Security mutants for property-based testing, in: TAP, LNCS 6706, Springer, 2011, pp. 69–77.

11.

Cortier ,

Delaune and

Lafourcade , A survey of algebraic properties used in cryptographic protocols, Journal of Computer Security 1 (2006), 1–43. doi:10.3233/JCS-2006-14101.

12.

Craig , Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic 22(3) (1957), 269–285. ISSN 00224812. doi:10.2307/2963594.

13.

Cremers and

Mauw , Operational Semantics and Verification of Security Protocols, Springer, 2012. doi:10.1007/978-3-540-78636-8.

14.

C.J.F.

Cremers , The Scyther Tool: Verification, falsification, and analysis of security protocols, in: Proceedings of CAV 2008, LNCS 5123, Springer, 2008, pp. 414–418.

15.

de Moura and

Bjorner , Z3: An efficient SMT solver, in: TACAS, LNCS 4963, Springer, 2008, pp. 337–340. ISBN 978-3-540-78799-0.

16.

Dolev and

Yao , On the security of public-key protocols, IEEE Transactions on Information Theory 29(2) (1983), 198–208.

17.

Escobar ,

Meadows and

Meseguer , Maude-NPA: Cryptographic protocol analysis modulo equational properties, in: FOSAD, Springer, 2007, pp. 1–50.

18.

Escobar ,

Meadows ,

Meseguer and

Santiago , State space reduction in the Maude-NRL protocol analyzer, Information and Computation 238 (2014), 157–186. doi:10.1016/j.ic.2014.07.007.

19.

Kahn , Natural semantics, in: STACS, 4th Annual Symposium, 1987, pp. 22–39. doi:10.1007/BFb0039592. http://dx.doi.org/10.1007/BFb0039592.

20.

J.C.

King , Symbolic execution and program testing, CACM 19(7) (1976), 385–394. ISSN 0001-0782. doi:10.1145/360248.360252.

21.

Lowe , Breaking and fixing the Needham–Shroeder public-key protocol using FDR, in: TACAS, LNCS 1055, Springer, 1996, pp. 147–166.

22.

K.L.

McMillan , An interpolating theorem prover, in: Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2004, pp. 16–30.

23.

K.L.

McMillan , Applications of Craig interpolants in model checking, in: TACAS, LNCS 3440, Springer, 2005, pp. 1–12. ISBN 978-3-540-25333-4.

24.

K.L.

McMillan , An interpolating theorem prover, Theoretical Computer Science 345(1) (2005), 101–121. ISSN 0304-3975. doi:10.1016/j.tcs.2005.07.003.

25.

K.L.

McMillan , Lazy abstraction with interpolants, in: CAV, 18th International Conference, Springer, 2006, pp. 123–136.

26.

K.L.

McMillan , Lazy annotation for program testing and verification, in: CAV, LNCS 6174, Springer, 2010, pp. 104–118. ISBN 978-3-642-14294-9.

27.

K.L.

McMillan , Interpolants from Z3 proofs, in: FMCAD, 2011, pp. 19–27. ISBN 978-0-9835678-1-3.

28.

K.L.

McMillan , Lazy annotation revisited, in: Computer Aided Verification – 26th International Conference, 2014, pp. 243–259.

29.

Mödersheim , Algebraic properties in Alice and Bob notation, in: Ares, IEEE CS, 2009, pp. 433–440.

30.

Mödersheim and

Viganò , The open-source fixed-point model checker for symbolic analysis of security protocols, in: FOSAD 2008/2009, LNCS 5705, Springer, 2009, pp. 166–194. doi:10.1007/978-3-642-03829-7_6.

31.

Mödersheim and

Viganò , Secure pseudonymous channels, in: Esorics, LNCS 5789, Springer, 2009, pp. 337–354. doi:10.1007/978-3-642-04444-1_21.

32.

Rocchetto ,

Viganò ,

Volpe and

Dalle Vedove , Using interpolation for the verification of security protocols, in: STM, Springer, 2013, pp. 99–114. doi:10.1007/978-3-642-41098-7_7.

33.

Rusinowitch and

Turuani , Protocol insecurity with a finite number of sessions and composed keys is NP-complete, Theor. Comput. Sci. 299(1–3) (2003), 451–475. ISSN 0304-3975. doi:10.1016/S0304-3975(02)00490-5.

34.

Schmidt ,

Sasse ,

Cremers and

D.A.

Basin , Automated verification of group key agreement protocols, in: IEEE Symposium on Security and Privacy, SP, 2014, pp. 179–194. doi:10.1109/SP.2014.19.

35.

Turuani , The CL-atse protocol analyser, in: Term Rewriting and Applications, LNCS 4098, Springer, 2006, pp. 277–286. ISBN 978-3-540-36834-2.

36.

Viganò , the SPaCIoS project: Secure provision and consumption in the Internet of services, in: ICST, IEEE CS Press, 2013. doi:10.1109/ICST.2013.75. www.spacios.eu.

37.

von Oheimb and

Mödersheim , ASLan++ – a formal security specification language for distributed systems, in: FMCO, LNCS 6957, Springer, 2010, pp. 1–22.