A BRICS Mini-Course
August 10 and 11, 2004
Birgit Pfitzmann, firstname.lastname@example.org
IBM Research Zürich
For a long time, cryptography and formal methods provided two almost unrelated ways of proving security of protocols: Cryptography provides precise and realistic definitions of the security of cryptographic primitives e.g., encryption and signatures, and protocols, e.g., secure channels or fair exchange. However, these definitions and corresponding proofs are long and difficult because many details are explicit, e.g., active attacks, error probabilities, and computational restrictions.
Formal methods, on the other hand, have well-defined protocol languages and provide tool support for proofs, such as model checking or theorem proving. This is particularly useful for distributed-system aspects of protocols, which are particularly tedious and error-prone if proved by hand.
However, almost all formal methods abstract from cryptography using so-called Dolev-Yao models. These models idealize cryptography as term algebras with fixed cancellation rules, and assume that knowledge that cannot be derived by these rules cannot be derived at all. For twenty years there was no justification for this abstraction.
These talks give an overview of recent advances of linking cryptography and formal methods. Particular emphasis will be on the cryptographic justification of a Dolev-Yao model under active attacks and for arbitrary protocol environment. We will also survey how cryptographic theorems for composition and property preservation enable this link and where actual tool-supported verification over proven abstractions stands.