An interpolation-based method for the verification of security protocols

Marco Rocchetto (1) , Luca Viganò (2) , Marco Volpe (3, 4)

1 UNIVR | DI - Department of Computer Science [Verona]
2 Department of Computer Science [London]
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
4 PARSIFAL - Proof search and reasoning with logic specifications

Interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. Security protocols, however, exhibit such idiosyncrasies that make them unsuitable to 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.

Mots clés: Security protocols; Craig interpolation; Symbolic execution; Verification

Domaines: Logique en informatique [cs.LO]; Cryptographie et sécurité [cs.CR]

Marco Rocchetto, Luca Viganò, Marco Volpe. An interpolation-based method for the verification of security protocols. 2015. ⟨hal-01245442⟩