Introduction to Formal Methods for the Analysis and Design of Cryptographic Protocols

This chapter introduces formal methods, and how they are applied to cryptographic protocols to achieve high security assurance. It introduces formal methods, and how they can be applied to cryptographic protocols, in order to detect their weaknesses early and achieve high assurance about their correctness. The chapter starts with an introduction to cryptographic protocols and to formal methods. It presents the various ways formal methods can be used throughout the cryptographic protocols lifecycle. Cryptographic protocols aim to guarantee security proprieties in a distributed system against the antagonistic actions of attackers who threaten the system. Formal methods are rigorous, mathematically-based techniques used to analyze, design and implement computer-based systems. Formal methods are particularly important for protocols, for example as a way to enable protocol interoperability, i.e., the possibility for different implementations of the same protocol, developed by different software providers, to work together and to achieve the protocol goals.