ProVerif: Automatisierte Protokollverifikation
Spezifizieren und überprüfen Sie Eigenschaften des TLS-Handshakes mit ProVerif.
ProVerif: Automatisierte Protokollverifikation ist eine kostenlose Cryptology Academy-Lektion auf CoddyKit. Dies ist Lektion 3 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 ProVerif?
ProVerif (Bruno Blanchet, 2001) ist ein automatisiertes Verifikationswerkzeug für kryptografische Protokolle. Es nimmt ein im Applied Pi-Kalkül beschriebenes Protokoll entgegen und entscheidet automatisch über Geheimhaltungs- und Authentifizierungseigenschaften.
So funktioniert ProVerif
ProVerif übersetzt das Protokoll in Horn-Klauseln und wendet einen auf Resolution basierenden Algorithmus an, um abzuleiten, was der Angreifer lernen kann. Wenn ein Geheimhaltungsfakt ableitbar ist, ist das Protokoll gebrochen; andernfalls ist seine Sicherheit bewiesen.
Eingabesprache von ProVerif
Protokolle werden deklarativ beschrieben: Kanäle, Typen, Funktionen (enc, dec, sign, verify), Gleichungen (dec(enc(m,k),k)=m) und Prozesse deklarieren, die über Kanäle kommunizieren.
Kryptografische Primitive deklarieren
Beispieldeklarationen für ProVerif:
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.Einen einfachen Protokollprozess schreiben
Modellieren Sie Alice und Bob als parallele Prozesse:
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))Sicherheitsabfragen formulieren
ProVerif prüft Abfragen wie:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).ProVerif-Ausgaben interpretieren
ProVerif gibt „RESULT ... is true“ (Sicherheit bewiesen) oder „RESULT ... is false“ aus und gibt eine Gegenbeispiel-Angriffsspur aus, die die Nachrichten des Angreifers zeigt. Die Spur zeigt genau, wie der Angriff funktioniert.
TLS 1.3 mit ProVerif verifizieren
Bhargavan et al. (2016) analysierten mit ProVerif ein Modell von TLS 1.3. Sie fanden einen Angriff auf den 0-RTT-Resumption-Mechanismus und berichteten darüber; der Angriff wurde vor der Finalisierung des RFC behoben.
Einschränkungen: Approximation und Schleifen
ProVerif überapproximiert: Es kann falsche Angriffe melden (also „false“ ausgeben, obwohl das Protokoll tatsächlich sicher ist), übersieht aber niemals echte Angriffe. Unbegrenzte Protokollsitzungen werden möglicherweise nicht beendet – ProVerif rollt Schleifen heuristisch ab.
Wenn ProVerif „Cannot Be Proved“ meldet
Wenn ProVerif das Ergebnis innerhalb seiner Approximation nicht bestimmen kann, gibt es „CANNOT BE PROVED.“ aus. Dies ist kein Beweis für Unsicherheit – es bedeutet, dass das Werkzeug seine heuristischen Möglichkeiten ausgeschöpft hat. Tamarin kann in diesen Fällen erfolgreich sein.
Wissensüberprüfung
Was bedeutet die ProVerif-Ausgabe „RESULT ... is false“ für eine Geheimhaltungsabfrage?
Zusammenfassung der Lektion
ProVerif automatisiert die Protokollverifikation mithilfe der Resolution von Horn-Klauseln. Protokolle werden im Applied Pi-Kalkül mit kryptografischen Gleichungen geschrieben. Abfragen beziehen sich auf Geheimhaltung und Authentifizierung. False bedeutet, dass die Sicherheit bewiesen ist; true bedeutet, dass das Protokoll gebrochen ist (mit Angriffsspur). Einschränkungen: Approximationen können dazu führen, dass etwas „cannot be proved“ ist.
Häufig gestellte Fragen
Ist die Lektion „ProVerif: Automatisierte Protokollverifikation“ kostenlos?
Ja — der vollständige Text von „ProVerif: Automatisierte Protokollverifikation“ 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 „ProVerif: Automatisierte Protokollverifikation“?
Spezifizieren und überprüfen Sie Eigenschaften des TLS-Handshakes mit ProVerif. 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 3 von 4.
Wie lange dauert die Lektion „ProVerif: Automatisierte Protokollverifikation“?
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