ProVerif: automatyczna weryfikacja protokołów
Specyfikować i weryfikować właściwości uzgadniania TLS za pomocą ProVerif
ProVerif: automatyczna weryfikacja protokołów to bezpłatna lekcja Cryptology Academy na CoddyKit. To lekcja 3 z 4. Możesz przeczytać całą lekcję poniżej za darmo — a potem ćwiczyć ją interaktywnie w przeglądarce z wbudowanym edytorem kodu i tutorem AI dostępnym 24/7. To część ścieżki edukacyjnej Cryptology Academy, a Twój postęp synchronizuje się między webem a aplikacją CoddyKit. Kurs Cryptology Academy zawiera 4 lekcji w sumie.
Czym jest ProVerif?
ProVerif (Bruno Blanchet, 2001) to automatyczny weryfikator protokołów kryptograficznych. Przyjmuje protokół opisany w rachunku pi z zastosowaniami i automatycznie rozstrzyga właściwości poufności oraz uwierzytelniania.
Jak działa ProVerif
ProVerif tłumaczy protokół na klauzule Horna i stosuje algorytm oparty na rezolucji, aby wyprowadzić informacje o tym, czego może dowiedzieć się atakujący. Jeśli można wyprowadzić fakt dotyczący poufności, protokół jest złamany; w przeciwnym razie jego bezpieczeństwo zostaje dowiedzione.
Język wejściowy ProVerif
Protokoły opisuje się deklaratywnie: deklaruje się kanały, typy, funkcje (enc, dec, sign, verify), równania (dec(enc(m,k),k)=m) oraz procesy komunikujące się za pośrednictwem kanałów.
Deklarowanie prymitywów kryptograficznych
Przykładowe deklaracje 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.Pisanie procesu prostego protokołu
Modelujemy Alice i Boba jako procesy równoległe:
(* 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)))Formułowanie zapytań dotyczących bezpieczeństwa
ProVerif sprawdza zapytania takie jak:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpretowanie wyników ProVerif
ProVerif wyświetla „RESULT ... is true” (bezpieczeństwo dowiedzione) albo „RESULT ... is false” i drukuje kontrprzykładowy ślad ataku pokazujący wiadomości wysyłane przez atakującego. Ślad pokazuje dokładnie, jak działa atak.
Weryfikowanie TLS 1.3 za pomocą ProVerif
Bhargavan i in. (2016) użyli ProVerif do przeanalizowania modelu TLS 1.3. Znaleźli i opisali atak na mechanizm wznawiania 0-RTT, który naprawiono przed sfinalizowaniem RFC.
Ograniczenia: przybliżenia i pętle
ProVerif stosuje nadprzybliżenie: może zgłaszać fałszywe ataki (mówić „false”, gdy protokół jest w rzeczywistości bezpieczny), ale nigdy nie pomija prawdziwych ataków. Nieograniczone sesje protokołu mogą się nie zakończyć — ProVerif rozwija pętle heurystycznie.
Gdy ProVerif mówi „Cannot Be Proved”
Jeśli ProVerif nie może określić wyniku w ramach swojego przybliżenia, wyświetla „CANNOT BE PROVED.” Nie jest to dowód braku bezpieczeństwa — oznacza jedynie, że narzędzie wyczerpało możliwości swoich heurystyk. W takich przypadkach może zadziałać Tamarin.
Sprawdzenie wiedzy
Co oznacza wynik ProVerif „RESULT ... is false” dla zapytania o poufność?
Podsumowanie lekcji
ProVerif automatyzuje weryfikację protokołów za pomocą rezolucji klauzul Horna. Protokoły zapisuje się w rachunku pi z zastosowaniami, używając równań kryptograficznych. Zapytania dotyczą poufności i uwierzytelniania. Wynik false oznacza dowiedzione bezpieczeństwo, a true — złamanie protokołu (wraz ze śladem ataku). Ograniczenia: przybliżenia mogą prowadzić do wyniku „cannot be proved”.
Często zadawane pytania
Czy lekcja „ProVerif: automatyczna weryfikacja protokołów” jest bezpłatna?
Tak — pełny tekst „ProVerif: automatyczna weryfikacja protokołów” jest dostępny za darmo tutaj w sieci. Aby ćwiczyć ją interaktywnie (wbudowany edytor kodu i tutor AI dostępny 24/7) i odblokować resztę kursu Cryptology Academy, przejdź na CoddyKit PRO. Kurs Cryptology Academy zawiera 4 lekcji w sumie.
Co nauczysz się w „ProVerif: automatyczna weryfikacja protokołów”?
Specyfikować i weryfikować właściwości uzgadniania TLS za pomocą ProVerif Ćwiczysz Cryptology Academy z praktycznym kodem, który uruchamiasz bezpośrednio w przeglądarce, a tutor AI dostępny 24/7 odpowiada na Twoje pytania podczas pracy nad lekcją.
Czy potrzebuję doświadczenia, aby zacząć Cryptology Academy?
Nie wymagamy żadnego doświadczenia. Cryptology Academy w CoddyKit jest strukturyzowany dla początkujących i zaawansowanych użytkowników, więc możesz zacząć tutaj lub od początku i uczyć się w swoim tempie. To lekcja 3 z 4.
Ile czasu zajmuje lekcja „ProVerif: automatyczna weryfikacja protokołów”?
Większość lekcji CoddyKit trwa około 5–10 minut. Każda lekcja to mały, interaktywny krok, dzięki czemu robisz systematyczne postępy i zawsze wracasz dokładnie do tego samego miejsca — na webie i w aplikacji.
Czy mogę pisać i uruchamiać kod w tej lekcji Cryptology Academy?
Tak. Każda lekcja Cryptology Academy zawiera wbudowany edytor kodu, więc piszesz i uruchamiasz prawdziwy kod bezpośrednio w przeglądarce i od razu otrzymujesz sprzężenie zwrotne od AI — bez konfiguracji na komputerze.
Wszystkie lekcje w tym kursie
- Dlaczego nieformalne dowody nie wystarczają
- Model atakującego Dolev–Yao i kryptografia symboliczna
- ProVerif: automatyczna weryfikacja protokołów
- Tamarin i dowody obliczeniowe