There are three difficulty levels to obtain a better understanding.
First level: we look at some examples of flawed protocol in a simple Alice–and–Bob 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 Alice–and–Bob 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 Alice–and–Bob versus an implementation. In fact, tools can help to derive an implementation skeleton from the Alice–and–Bob notation so that one does not overlook for instance any checks that participants must perform on messages they receive.
