Tamarin & Computational Proofs
Use Tamarin prover for multiset rewriting and trace-based verification.
Tamarin & Computational Proofs is a free Cryptology Academy lesson on CoddyKit — lesson 4 of 4. You can read the complete lesson below for free — then practise it hands-on in the browser with a built-in code editor and a 24/7 AI tutor. It is part of the Cryptology Academy learning path, one of 4 lessons in the course, and your progress syncs across the web and the CoddyKit app.
What Is Tamarin?
Tamarin (ETH Zurich, 2012) is a security protocol verifier based on multiset rewriting. Unlike ProVerif's Horn-clause approach, Tamarin reasons about traces of protocol executions with an interactive prover.
Tamarin vs ProVerif
ProVerif: fully automated, may give "cannot be proved." Tamarin: interactive proof assistant + automated mode, handles equational theories (XOR, Diffie-Hellman, bilinear maps). More expressive, steeper learning curve.
Multiset Rewriting Rules
Tamarin models protocols as rewriting rules over facts. Facts represent state. A rule [ L ] --[ A ]-> [ R ] consumes left-hand facts L, produces right-hand facts R, and logs action A in the trace.
Tamarin Input Language (.spthy)
A Tamarin theory file declares functions, equations, rules, and lemmas:
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]Stating Lemmas
Security goals are expressed as lemmas over traces:
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"Running Tamarin
Launch Tamarin's interactive GUI: tamarin-prover interactive my_protocol.spthy. The browser UI shows proof obligations; you guide automated strategies or apply manual steps for non-terminating cases.
Computational Soundness
Symbolic proofs (ProVerif, Tamarin) guarantee security under perfect-crypto assumptions. Computational soundness theorems (Cortier, Backes) lift symbolic proofs to computational security when instantiated with provably secure primitives.
F* and HACL*: Verified Implementations
F* (Microsoft Research) is a proof-oriented programming language. HACL* is a cryptographic library written in F* with machine-verified proofs of correctness and side-channel resistance. Used in Firefox NSS and mbedTLS.
EasyCrypt: Game-Based Computational Proofs
EasyCrypt enables fully computational (game-based) security proofs for cryptographic constructions — not just protocols. TLS 1.3 record layer and ChaCha20-Poly1305 have been verified in EasyCrypt.
Practical Impact
Formally verified crypto is entering production: NSS (Firefox) uses HACL*, AWS uses s2n-tls with proof-carrying assertions, and the Signal protocol has been verified in ProVerif and Tamarin. Formal methods are no longer academic only.
Knowledge Check
How does Tamarin differ from ProVerif in handling cases where automation fails?
Lesson Recap
Tamarin uses multiset rewriting and trace-based reasoning with an interactive proof GUI. It handles DH and XOR equational theories. Lemmas express secrecy and authentication goals. Computational soundness bridges symbolic proofs to real security. HACL* and EasyCrypt extend verification to implementations and constructions.
Frequently asked questions
Is the “Tamarin & Computational Proofs” lesson free?
Yes — the full text of “Tamarin & Computational Proofs” is free to read here on the web, and the Cryptology Academy course includes 4 lessons in total. To practise it interactively (a built-in code editor and a 24/7 AI tutor) and unlock the rest of the Cryptology Academy course, upgrade to CoddyKit PRO.
What will I learn in “Tamarin & Computational Proofs”?
Use Tamarin prover for multiset rewriting and trace-based verification. You practise Cryptology Academy with hands-on code you run directly in the browser, and a 24/7 AI tutor answers your questions as you work through the lesson.
Do I need any experience to start Cryptology Academy?
No prior experience is required. Cryptology Academy on CoddyKit is structured for beginners through advanced learners; this is — lesson 4 of 4, so you can start here or from the beginning and move at your own pace.
How long does the “Tamarin & Computational Proofs” lesson take?
Most CoddyKit lessons take about 5–10 minutes. Each one is bite-sized and interactive, so you make steady progress and pick up exactly where you left off across the web and the app.
Can I write and run code in this Cryptology Academy lesson?
Yes. Every Cryptology Academy lesson includes a built-in code editor, so you write and run real code right in your browser and get instant AI feedback — no local setup required.
All lessons in this course
- Why Informal Proofs Are Not Enough
- Dolev-Yao Attacker Model & Symbolic Crypto
- ProVerif: Automated Protocol Verification
- Tamarin & Computational Proofs