Cryptographic protocols are the backbone of secure communication over open networks and their correctness is therefore crucial. Tool-supported formal analysis of cryptographic protocol designs increases our confidence that these protocols achieve their intended security guarantees. We propose a method to automatically translate textbook style Alice&Bob protocol specifications into a format amenable to formal verification using existing tools. Our translation supports specification modulo equational theories, which enables the faithful representation of algebraic properties of a large class of cryptographic operators.
CITATION STYLE
Basin, D., Keller, M., Radomirović, S., & Sasse, R. (2015). Alice and Bob meet equational theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9200, pp. 160–180). Springer Verlag. https://doi.org/10.1007/978-3-319-23165-5_7
Mendeley helps you to discover research relevant for your work.