david wong

Hey! I'm David, cofounder of zkSecurity and the author of the Real-World Cryptography book. I was previously a crypto architect at O(1) Labs (working on the Mina cryptocurrency), before that 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.

Well done! You've reached the end of my post. Now you can leave a comment or read something else.

Comments

Zeeshan

Hi, can you please help me solving this error:

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

leave a comment...