Tamarin und rechnerische Beweise
Verwenden Sie den Tamarin-Prover für Multiset-Rewriting und tracebasierte Verifikation.
Tamarin und rechnerische Beweise ist eine kostenlose Cryptology Academy-Lektion auf CoddyKit. Dies ist Lektion 4 von 4. Du kannst die komplette Lektion unten kostenlos lesen – dann übst du sie direkt im Browser mit einem integrierten Code-Editor und einem KI-Tutor rund um die Uhr. Sie ist Teil des Cryptology Academy-Lernpfads, und dein Fortschritt wird über Web und CoddyKit-App synchronisiert. Der Cryptology Academy-Kurs umfasst insgesamt 4 Lektionen.
Was ist Tamarin?
Tamarin (ETH Zurich, 2012) ist ein Verifikationswerkzeug für Sicherheitsprotokolle auf Basis von Multimengen-Rewriting. Anders als ProVerifs Horn-Klausel-Ansatz analysiert Tamarin mit einem interaktiven Beweiser Traces von Protokollausführungen.
Tamarin vs. ProVerif
ProVerif: vollständig automatisiert, meldet möglicherweise „cannot be proved“. Tamarin: interaktiver Beweisassistent plus automatisierter Modus, verarbeitet Gleichungstheorien (XOR, Diffie-Hellman, bilineare Abbildungen). Ausdrucksstärker, aber mit steilerer Lernkurve.
Regeln für Multimengen-Rewriting
Tamarin modelliert Protokolle als Umschreibungsregeln für Fakten. Fakten stellen den Zustand dar. Eine Regel [ L ] --[ A ]-> [ R ] verbraucht Fakten der linken Seite L, erzeugt Fakten der rechten Seite R und protokolliert die Aktion A im Trace.
Eingabesprache von Tamarin (.spthy)
Eine Tamarin-Theoriedatei deklariert Funktionen, Gleichungen, Regeln und Lemmata:
/* 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) ]Lemmata formulieren
Sicherheitsziele werden als Lemmata über Traces formuliert:
/* 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 ausführen
Starten Sie die interaktive GUI von Tamarin: tamarin-prover interactive my_protocol.spthy. Die Browseroberfläche zeigt Beweisverpflichtungen; Sie steuern automatisierte Strategien oder wenden für nicht terminierende Fälle manuelle Schritte an.
Computational Soundness
Symbolische Beweise (ProVerif, Tamarin) garantieren Sicherheit unter Annahmen perfekter Kryptografie. Sätze zur Computational soundness (Cortier, Backes) übertragen symbolische Beweise auf rechnerische Sicherheit, wenn sie mit nachweislich sicheren Primitiven instanziiert werden.
F* und HACL*: Verifizierte Implementierungen
F* (Microsoft Research) ist eine beweisorientierte Programmiersprache. HACL* ist eine in F* geschriebene Kryptobibliothek mit maschinell verifizierten Beweisen für Korrektheit und Seitenkanalresistenz. Sie kommt in Firefox NSS und mbedTLS zum Einsatz.
EasyCrypt: Spielbasierte rechnerische Beweise
EasyCrypt ermöglicht vollständig rechnerische (spielbasierte) Sicherheitsbeweise für kryptografische Konstruktionen – nicht nur für Protokolle. Die Record Layer von TLS 1.3 und ChaCha20-Poly1305 wurden in EasyCrypt verifiziert.
Praktische Auswirkungen
Formal verifizierte Kryptografie hält Einzug in die Produktion: NSS (Firefox) verwendet HACL*, AWS nutzt s2n-tls mit beweistragenden Zusicherungen, und das Signal-Protokoll wurde in ProVerif und Tamarin verifiziert. Formale Methoden sind nicht mehr nur akademischer Natur.
Wissensüberprüfung
Wie unterscheidet sich Tamarin von ProVerif beim Umgang mit Fällen, in denen die Automatisierung scheitert?
Zusammenfassung der Lektion
Tamarin verwendet Multimengen-Rewriting und eine Trace-basierte Argumentation mit einer interaktiven Beweis-GUI. Es verarbeitet Gleichungstheorien für DH und XOR. Lemmata formulieren Ziele für Geheimhaltung und Authentifizierung. Computational Soundness überbrückt die Lücke zwischen symbolischen Beweisen und realer Sicherheit. HACL* und EasyCrypt erweitern die Verifikation auf Implementierungen und Konstruktionen.
Häufig gestellte Fragen
Ist die Lektion „Tamarin und rechnerische Beweise“ kostenlos?
Ja — der vollständige Text von „Tamarin und rechnerische Beweise“ ist hier im Web kostenlos zu lesen. Um sie interaktiv zu üben (integrierter Code-Editor und 24/7 KI-Tutor) und den Rest des Cryptology Academy-Kurses freizuschalten, upgrade auf CoddyKit PRO. Der Cryptology Academy-Kurs umfasst insgesamt 4 Lektionen.
Was lerne ich in „Tamarin und rechnerische Beweise“?
Verwenden Sie den Tamarin-Prover für Multiset-Rewriting und tracebasierte Verifikation. Du übst Cryptology Academy mit praktischem Code, den du direkt im Browser ausführst, und ein 24/7 KI-Tutor beantwortet deine Fragen während du die Lektion bearbeitest.
Brauche ich Erfahrung, um Cryptology Academy zu starten?
Keine Vorkenntnisse erforderlich. Cryptology Academy auf CoddyKit ist für Anfänger bis fortgeschrittene Lernende strukturiert, sodass du hier starten oder von Anfang an beginnen und in deinem eigenen Tempo voranschreiten kannst. Dies ist Lektion 4 von 4.
Wie lange dauert die Lektion „Tamarin und rechnerische Beweise“?
Die meisten CoddyKit-Lektionen dauern etwa 5–10 Minuten. Jede ist kompakt und interaktiv, sodass du stetig Fortschritte machst und genau dort weitermachst, wo du aufgehört hast – im Web und in der App.
Kann ich in dieser Cryptology Academy-Lektion Code schreiben und ausführen?
Ja. Jede Cryptology Academy-Lektion enthält einen integrierten Code-Editor, sodass du echten Code direkt in deinem Browser schreibst und ausführst und sofort KI-Feedback erhältst — ohne lokale Einrichtung erforderlich.
Alle Lektionen in diesem Kurs
- Warum informelle Beweise nicht ausreichen
- Dolev-Yao-Angreifermodell und symbolische Kryptografie
- ProVerif: Automatisierte Protokollverifikation
- Tamarin und rechnerische Beweise