Once upon a time...
Both proofs have seen several corrections, and live in similar, but slightly separate models.
Tamarin models protocols as rules that take in a set of variables and one or more messages, and then emit new variables and messages.
The (Dolev-Yao) attacker controls the network and can read, send, change, drop all messages.
Any cryptographic operation is perfect. Cryptographic compromise is modeled through manually modeled "oracles" that reveal specific keys.
rule ProtocolMessageI: [ In(message), VariableI(x) ] --[ ReceivedMessageFact(message, x) ]-> [ Out(SomeOtherMessage), VariableII(operation(x)) ]
lemma my_lemma: "All key #i #j. ExchangedKey(key)@#i // some protocol-emitted fact // over `key` at time #i & K(key)@#j // Adversary knows `key` at #j ==> /* then */ /* exists a time #z */ Ex #z. /* at which key was revealed */ RevealedKey(key)@#z /* and #z was before #j */ & #z < #j "
|Feature||Model #1||Model #2|
|Encrypted handshake messages||✅||❌|
|HKDF and HMAC decomposed into hash||✅||❌|
|Key exchange and auth KEMs are same algorithm||✅||❌|
|Adversary can reveal long-term keys||✅||✅|
|Adversary can reveal ephemeral keys||✅||❌|
|Adversary can reveal intermediate session keys||❌||✅|
|Secrecy of handshake and traffic keys||✅||✅|
|Multiple flavours of forward secrecy||❌||✅|
Model your own protocols!
Thanks for your attention