Formal Verification of Cryptographic Protocols

Date: 7 May 1998.
Presenter: Sven Dietrich, NASA GSFC/Raytheon STX (now Raytheon ITSS).

We present an overview of techniques for verifying key-exchange and authentication protocols. In the past, these protocols were considered `safe until broken', but current techniques assist the protocol designer during the design phase, and allow for thorough, and often automatic, verification. We describe five major families of formal methods: finite-state machines, methods not originally designed to analyze cryptographic protocols, logics of knowledge ad belief, formal models based on algebraic term rewriting, complexity-theoretic approaches, and hybrid methods thereof. We look at the safety properties they assess, e.g. secrecy of a session key, and the scope of the analysis. We show examples of protocol analysis, from simple cases as the Needham-Schroeder protocol to more complex ones as SSL 3.0.



Back to my home page
Last modified: 17 March 1999