Select Page

Automated Protocol Verification

Who is the material made for?

This course is for developers and designers who are interested in understanding and avoiding the logical attacks that arise out of a “wrong” deployment of cryptographic primitives to achieve secure communication. The course assumes only knowledge of the basic cryptographic concepts like publickey cryptography.


Cryptography offers rather straight forward ways to secure the communication in distributed systems, namely encrypting messages for secrecy and authenticating messages for integrity. However, it is so easy to make simple logical mistakes in the construction so that an attacker or dishonest participant can break the security of the system without breaking the cryptography.This course is dedicated to understanding, automatically finding and then avoiding such mistakes.


There are three difficulty levels to obtain a better understanding.

First level: we look at some examples of flawed protocol in a simple AliceandBob notation and use a tool, OFMC, to automatically find an attack. The challenge is to understand the attack and modify the protocol to fix the attack, so that OFMC finds no more attack.

Second level: designing a larger protocol in AliceandBob notation and verifying it with OFMC. As an example, we consider a movie theatre that allows movie goers to buy electronic tickets and show them at the entrance, and of course avoiding that with one ticket a whole group of friends can see the movie.

Third level: we consider the relation between a formal model in AliceandBob versus an implementation. In fact, tools can help to derive an implementation skeleton from the AliceandBob notation so that one does not overlook for instance any checks that participants must perform on messages they receive.