Tamarin en computationele bewijzen
Gebruik de Tamarin-prover voor multiset rewriting en tracegebaseerde verificatie.
Tamarin en computationele bewijzen is een gratis Cryptology Academy-les op CoddyKit. Dit is les 4 van 4. Je kunt de volledige les hieronder gratis lezen en daarna in de browser praktisch oefenen met een ingebouwde code-editor en een AI-begeleider die 24/7 beschikbaar is. Deze les maakt deel uit van het leertraject Cryptology Academy. Je voortgang wordt gesynchroniseerd op het web en in de CoddyKit-app. De cursus Cryptology Academy bevat in totaal 4 lessen.
Wat is Tamarin?
Tamarin (ETH Zurich, 2012) is een verificateur voor beveiligingsprotocollen die op het herschrijven van multisets is gebaseerd. In tegenstelling tot de Horn-clausuleaanpak van ProVerif redeneert Tamarin met een interactieve bewijsassistent over sporen van protocoluitvoeringen.
Tamarin versus ProVerif
ProVerif: volledig automatisch, maar kan "cannot be proved" geven. Tamarin: interactieve bewijsassistent plus geautomatiseerde modus, die equatietheorieën verwerkt (XOR, Diffie-Hellman, bilineaire afbeeldingen). Expressiever, maar met een steilere leercurve.
Regels voor het herschrijven van multisets
Tamarin modelleert protocollen als herschrijfregels voor feiten. Feiten vertegenwoordigen de toestand. Een regel [ L ] --[ A ]-> [ R ] verbruikt de feiten L aan de linkerkant, produceert de feiten R aan de rechterkant en registreert actie A in het spoor.
Invoertaal van Tamarin (.spthy)
Een Tamarin-theoriebestand declareert functies, vergelijkingen, regels en lemma's:
/* 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) ]Lemma's formuleren
Beveiligingsdoelen worden uitgedrukt als lemma's over sporen:
/* 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"Tamarin uitvoeren
Start de interactieve grafische gebruikersinterface van Tamarin: tamarin-prover interactive my_protocol.spthy. De browserinterface toont bewijsverplichtingen; je stuurt geautomatiseerde strategieën aan of past handmatige stappen toe voor gevallen waarin beëindiging uitblijft.
Computationele correctheid
Symbolische bewijzen (ProVerif, Tamarin) garanderen beveiliging onder aannames van perfecte cryptografie. Stellingen over computationele correctheid (Cortier, Backes) tillen symbolische bewijzen op naar computationele beveiliging wanneer ze worden geïnstantieerd met aantoonbaar veilige primitieven.
F* en HACL*: geverifieerde implementaties
F* (Microsoft Research) is een op bewijzen gerichte programmeertaal. HACL* is een cryptografische bibliotheek die in F* is geschreven, met machinegecontroleerde bewijzen van correctheid en weerstand tegen zijkanaalaanvallen. De bibliotheek wordt gebruikt in Firefox NSS en mbedTLS.
EasyCrypt: op spellen gebaseerde computationele bewijzen
EasyCrypt maakt volledig computationele beveiligingsbewijzen op basis van spellen mogelijk voor cryptografische constructies — niet alleen voor protocollen. De TLS 1.3-recordlaag en ChaCha20-Poly1305 zijn in EasyCrypt geverifieerd.
Praktische impact
Formeel geverifieerde cryptografie komt in productieomgevingen terecht: NSS (Firefox) gebruikt HACL*, AWS gebruikt s2n-tls met beweringen waaraan bewijzen zijn gekoppeld en het Signal-protocol is geverifieerd in ProVerif en Tamarin. Formele methoden zijn niet langer uitsluitend academisch.
Kennistoets
Waarin verschilt Tamarin van ProVerif bij het verwerken van gevallen waarin automatisering faalt?
Lesoverzicht
Tamarin gebruikt het herschrijven van multisets en redeneert op basis van sporen met een interactieve bewijsinterface. Het verwerkt equatietheorieën voor DH en XOR. Lemma's drukken doelen voor geheimhouding en authenticatie uit. Computationele correctheid overbrugt symbolische bewijzen naar echte beveiliging. HACL* en EasyCrypt breiden verificatie uit naar implementaties en constructies.
Leer Cryptology Academy met een AI-tutor — gratis
Schrijf echte code en voer die uit in je browser, krijg direct hulp van een AI-tutor die 24/7 beschikbaar is en ga verder waar je gebleven bent op het web of in de app.
- Cursussen
- 67
- Lessen
- 261
Veelgestelde vragen
Is de les “Tamarin en computationele bewijzen” gratis?
Ja — de volledige tekst van “Tamarin en computationele bewijzen” kun je hier gratis op het web lezen. Als je interactief wilt oefenen met een ingebouwde code-editor en een AI-begeleider die 24/7 beschikbaar is, en de rest van de cursus Cryptology Academy wilt ontgrendelen, kun je upgraden naar CoddyKit PRO. De cursus Cryptology Academy bevat in totaal 4 lessen.
Wat leer ik in “Tamarin en computationele bewijzen”?
Gebruik de Tamarin-prover voor multiset rewriting en tracegebaseerde verificatie. Je oefent met Cryptology Academy door code rechtstreeks in de browser uit te voeren. Een AI-begeleider die 24/7 beschikbaar is beantwoordt je vragen terwijl je de les doorwerkt.
Heb ik ervaring nodig om met Cryptology Academy te beginnen?
Ervaring vooraf is niet nodig. Cryptology Academy op CoddyKit is opgebouwd voor beginners tot gevorderden, zodat je hier of bij het begin kunt starten en in je eigen tempo kunt leren. Dit is les 4 van 4.
Hoe lang duurt de les “Tamarin en computationele bewijzen”?
De meeste lessen van CoddyKit duren ongeveer 5–10 minuten. Elke les is kort en interactief, zodat je gestaag vooruitgaat en op het web en in de app precies verdergaat waar je was gebleven.
Kan ik code schrijven en uitvoeren in deze les over Cryptology Academy?
Ja. Elke les over Cryptology Academy bevat een ingebouwde code-editor, zodat je rechtstreeks in je browser echte code kunt schrijven en uitvoeren en direct feedback van AI krijgt — lokale installatie is niet nodig.
Alle lessen in deze cursus
- Waarom informele bewijzen niet volstaan
- Dolev-Yao-aanvallersmodel en symbolische cryptografie
- ProVerif: geautomatiseerde protocolverificatie
- Tamarin en computationele bewijzen