| Title: | Using Interpolation for the Verification of Security Protocols (Extended Abstract) |
| Authors: | Marco Rocchetto, Luca Viganò and Marco Volpe |
| Proceedings: | iPRA 2014 Proceedings |
| Editors: | Laura Kovacs and Georg Weissenbacher |
| Keywords: | Craig's interpolation, Formal verification, 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 such idiosyncrasies that make them unsuitable to the direct application of such methods. In this paper, we address this problem and present an interpolation-based method for security protocol verication. Our method starts from a formal protocol specication 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 an implementation of our method and its application to concrete examples. |
| Pages: | 2 |
| Talk: | Jul 18 14:30 |
| Paper: |  |