Combining cryptographic and formal proof techniques

Cryptographic protocols are a tricky issue. Even seemingly simple protocols Such as the exchange of secret keys using public keys have often turned out to be wrong. Hence it is essential to prove their security.

Cryptography provides precise and realistic definitions of the security of cryptographic primitives (like encryption and signatures) and protocols (like secure channels or fair exchange). However, these definitions are long and difficult to grasp because they are full of details. One has to model all active attacks that adversaries might carry out, most primitives are probabilistic, and most properties have some error probability. Further, computational restrictions are considered. Consequently, it is not easy to see if a cryptographic definition captures reality well, and many proofs are rather sketchy and some have, for this reason, not been correct.

Formal methods, on the other hand, have well-defined protocol languages, which support a systematic presentation of protocols and properties. Most importantly, they provide tool support for proofs, such as model checking or theorem proving. Such tools are particularly useful for distributed protocols, which are particularly tedious and error-prone if proved by hand. Hence it was natural to try to apply formal methods also to distributed cryptographic protocols.

However, almost all formal methods abstract from cryptography using the Dolev-Yao model, and for many years there was no justification at all for this abstraction. The Dolev-Yao model represents cryptographic objects as terms (not bit strings). For instance, the term D_x(E_x(E_x(m))) represents a message encrypted twice with key x and then decrypted once. Then there are cancellation rules, e.g. D_x E_x = i, where i is the identity function. This identity is indeed true for real cryptosystems. However, in security proofs one assumes that no cancellation rule ever holds unless one has specified it explicitly. This property is not justified in any easy way by cryptographic definitions, and indeed not true in general and for unmodified cryptographic systems.

Cryptographically justifying a Dolev-Yao model: slides with speaker/reader notes. We have also symbolically proved protocols over this model, see below. This was the first result on justifying a Dolev-Yao model while including active attacks, and thus for a realistic scenario. Compared with later results by others, it proves by far the strongest properties: We allow multiple primitives, an arbitrary protocol environment, and prove reactive simulatability of the entire Dolev-Yao model, from which almost arbitrary property preservation can be derived. Later results are best described as attempting to find out how much one can simplify by giving up some of these properties, e.g., by restricting the protocol language or the desired properties.

Without research reports essentially superseded by publications. (For other publications of the authors see the group publications page.)