How to obtain a nice trace in Tamarin posted May 2017

This is not a nice trace

Learning about the inners of Tamarin, I've came up to the point where I wanted to get a nice clean trace to convince myself that the protocol I wrote made sense.

The way to check for proper functioning is to create exist-trace lemmas.

Unfortunately, using Tamarin to prove such lemma will not always yield the nicest trace.

Here are some tricks I've used to obtain a simple trace. Note that these matter less when you're writing lemmas to "attack" the protocol (as you really don't want to impose too many restrictions that might not hold in practice).

1. Use a fresh "session id". A random session id can be added to different states and messages to identify a trace from another one.

rule client_start_handshake:
    [!Init($client, ~privkey, pubkey), !Init($server, ~priv, pub), Fr(~sid)]
    --[Start(~sid, $client, $server)]->
    [Out(<'1', ~sid, $client, $server, pubkey>)]

2. Use temporals to make sure that everything happens in order.

Ex sid, client, server, sessionkey #i #j.
      Start(sid, client, server) @ #i & 
      Session_Success(sid, 'server', server, client, sessionkey) @ #j &
    #i < #j

3. Make sure your identities are different. Start by defining your lemma by making sure a server cannot communicate with itself.

Ex sid, client, server, sessionkey #i #j.
      not(server = client) & ...

4. Use constraints to force peers to have a unique key per identity. Without that, you cannot force Tamarin to believe that one identity could create multiple keys. Of course you might want your model to allow many-keys per identity, but we're talking about a nice trace here :)

restriction one_key_per_identity: "All X key key2 #i #j. Gen(X, key) @ #i & Gen(X, key2) @ #j ==> #i = #j"

rule generate_identity_and_key:
    let pub = 'g'^~priv
    in
    [ Fr(~priv) ]--[Gen($A, pub)]->[ !Init($A, ~priv, pub) ]

5. Disable the adversary. This might be the most important rule here, and it ended up being the breakthrough that allowed me to find a nice trace. Unfortunately you cannot disable the adversary, but you can force Ins and Outs to happen via facts (which are not seen by the adversary, and remove any possible interaction from the adversary). For this you can replace every In and Out with InSecure and OutSecure and have these rules:

#ifdef not_debug
[OutSecure(a)] -->[Out(a)]
[In(a)] -->[InSecure(a)]
#endif

#ifdef debug
[OutSecure(a)]-->[InSecure(a)]
#endif

You can now call tamarin like this:

tamarin interactive . -Dnot_debug

And we now have a nice trace!

Our protocol is an opportunistic Diffie-Hellman. You can see the two generate_identity_and_key rules at the top that creates the two different identities: a client and a server.

The second rule client_start_handshake is used to start the handshake. The client sends the first message 1 with a fresh session id ~sid.

The third rule server_handshake propagates the received session id to the next message and to its action fact (so that the lemma can keep the session id consistent).

The protocol ends in the last rule client_handshake_finish being used.

Voila!

PS: thanks to Katriel Cohn-Gordon for answering ten thousands of my questions about Tamarin.