Hey! I'm David, the author of the Real-World Cryptography book. I'm a crypto engineer at O(1) Labs on the Mina cryptocurrency, previously I was the security lead for Diem (formerly Libra) at Novi (Facebook), and a security consultant for the Cryptography Services of NCC Group. This is my blog about cryptography and security and other related topics that I find interesting.

# Tamarin Prover posted May 2017

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.

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.

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.

#### Zeeshan

WARNING: the following wellformedness checks failed!

unbound:
rule create_user_cert' has unbound variables:
CertU, SigReq

rule user_rec_signed_cert' has unbound variables:
~ltkCAx1, ~ltkCAx2, ~ltkU, ContactCA

rule Udata_reg' has unbound variables:
RegReq

rule data_reg_CA1_Next' has unbound variables:
ukdata

rule `data_reg_data' has unbound variables:
CertU, Msg1

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
here is the source code

theory create_certificate
begin
builtins: hashing, asymmetric-encryption

// creating user certificate

rule create_user_cert:
let udata=$ukdata pkU =pk(~ltkU) in [ !Ltk ($U, ~ltkU), N_Cert($U, pkU)] --[Single('Create_User_Cert') ,ReqCert($U, ~ltkU)]->
[DMCert($U, CertU,$CA1, $CA2), // Domain combine Certificate Out(<$U, $CA1, SigReq>), Out(<$U, $CA2, SigReq>)] rule user_rec_signed_cert: let CA=$CA1 in
[DMCert($U, CertU,$CA1, $CA2), In (<$CA1, $U, SignCert1>), In (<$CA2, $U, SignCert2>)] --[NotEqual (~ltkCAx1, ~ltkCAx2), ReceiveCASignCert($U, ~ltkU)]->
[DomHasCert($U, ContactCA, CertU)] rule Udata_reg: let Udata =$Ukdata in
[DomHasCert($U,$CA1, CertU)
, !Ltk($U, ~ltkU), !Ltk($CA1, ~ltkCAx1)
,!Ltk($CA2, ~ltkCAx2)] --[Single(<'Udata_reg', ~ltkU>)]-> [Out (<$U, $CA1, RegReq>), DomainHasCert($U,$CA1, CertU)] rule data_reg_CA1_Next: [In (<$U, $CA1, RegReq>)]--[]-> [Out (<$CA1, ukdata, RegReq>)
,ContactCADataReg($U,$CA1, RegReq)]

rule data_reg_data:
[In (<$CA1,$ukdata, RegReq>), !Ltk($ukdata, ~ltkK) , !Ltk($CA1, ~ltkCAx1), !Ltk($CA2, ~lltkCAx2) , Adddata(~ltkK,$ukdata, AddList)]
--[Single(<'RegisterDomain', $U>)]-> [Out (<$ukdata, $CA2, Msg1>) , Adddata(~ltkK,$ukdata, AddList, CertU)]

lemma main_auth:
" ( All certid a b reason prevkey key #i1 #i2 #i3 #i4 .
( New_Ltk (a, prevkey, 'trusted') @i1 // 'Honest agent'
& ReqCert(a, prevkey) @i2 //domain asked for cert with this key
& ReceivedSignCert(a, prevkey) @i3 //conformation that certificate has been issued with this exact key

& ConnectionAccepted(certid, b, a, reason, key) @i4 //connection accepted by browser based on
& i3 < i4) //private key 'key' for domain a.
==>
( (not (Ex #j. K(key) @j)) ) )
" //adversary cannot know the private key.
end