An interpolation-based method for the verification of security protocols

Article type: Research Article

Authors: Rocchetto, Marco^a | Viganò, Luca^{b; *} | Volpe, Marco^c

Affiliations: [a] ALES, United Technologies Research Center, Italy. E-mail: marco.rocchetto@utrc.utc.com | [b] Department of Informatics, King’s College London, UK. E-mail: luca.vigano@kcl.ac.uk | [c] INRIA and LIX, École Polytechnique, France. E-mail: marco.volpe@inria.fr

Correspondence: [*] Corresponding author. E-mail: luca.vigano@kcl.ac.uk.

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

DOI: 10.3233/JCS-16832

Journal: Journal of Computer Security, vol. 25, no. 6, pp. 463-510, 2017