I was at Eurocrypt’s workshop in Paris last week. One of the reason is because I really like workshops. It was good. Good because of the Tamarin workshop, less good because it ended up just being like a normal conference, but still good because it was incredibly close to Real World Crypto.

Tamarin is a “protocol” verification tool. You give it a protocol, a set of security properties it should respect and Tamarin gives you a formal proof (using constraints solving) that the security guarantees are indeed provided OR it gives you a counter example (an attack).

By default, the adversary is a Dolev-Yao adversary that controls the network and can delete, inject, modify and intercept messages on the network

The thing is realllyyyy easy to install.

You gotta love good scientists pic.twitter.com/xC9qgVMmUu

— David Wong (@lyon01_david) April 28, 2017

In the morning, Cas Cremers gave us an intro to Tamarin and taught us how to read inputs and outputs of the tool. In the afternoon, Ralf Sasse told us about more complex concepts while forcing us to write some input for Tamarin.

It was a lot of fun. Way more fun than I expected. I have to admit that I came skeptical, and never really considered formal verification as “practical”. But this day changed my mind.

In an afternoon I was capable of creating a pretty simple input to model an opportunistic ephemeral Diffie-Hellman key agreement. The input I wrote is available here. (I have made a better one here and Santiago Zanella made one here as well).

You can see a lot of rules describing the possible transitions of the state machine, and a final lemma which is saying “for any created session (where neither a key or a session key has been leaked) a man-in-the-middle attacker cannot influence the protocol to retrieve the session key”. Of course this is ugly, and reading it again a week afterwards I see things I want to rewrite, and probably some “pros” are going to cringe… But it worked out! and Tamarin ended up finding the trivial man-in-the-middle attack.

I broke opportunistic Diffie-Hellman with Tamarin :D code here: https://t.co/VkahJbStfo pic.twitter.com/QDFERr7xvX

— David Wong (@lyon01_david) April 29, 2017

If you want to play with it, check the online manual which is just great. It provides a few examples that quickly get you started. The hardest part, you must have guessed, is to translate your protocol into this Tamarin input language.