Tamarin i dowody obliczeniowe
Użyć weryfikatora Tamarin do przepisywania multizbiorów i weryfikacji opartej na śladach
Tamarin i dowody obliczeniowe to bezpłatna lekcja Cryptology Academy na CoddyKit. To lekcja 4 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 Tamarin?
Tamarin (ETH Zurich, 2012) to weryfikator protokołów bezpieczeństwa oparty na przepisywaniu multizbiorów. W przeciwieństwie do podejścia ProVerif opartego na klauzulach Horna, Tamarin analizuje ślady wykonań protokołu za pomocą interaktywnego asystenta dowodzenia.
Tamarin a ProVerif
ProVerif: w pełni automatyczny, może zwrócić wynik „cannot be proved”. Tamarin: interaktywny asystent dowodzenia oraz tryb automatyczny, obsługuje teorie równościowe (XOR, Diffie-Hellman, odwzorowania biliniowe). Większe możliwości wyrazu, bardziej stroma krzywa uczenia się.
Reguły przepisywania multizbiorów
Tamarin modeluje protokoły jako reguły przepisywania działające na faktach. Fakty reprezentują stan. Reguła [ L ] --[ A ]-> [ R ] zużywa fakty po lewej stronie L, tworzy fakty po prawej stronie R i zapisuje działanie A w śladzie.
Język wejściowy Tamarin (.spthy)
Plik teorii Tamarin deklaruje funkcje, równania, reguły i lematy:
/* 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) ]Formułowanie lematów
Cele bezpieczeństwa wyraża się jako lematy dotyczące śladów:
/* 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"Uruchamianie Tamarin
Interaktywny interfejs GUI Tamarin można uruchomić poleceniem: tamarin-prover interactive my_protocol.spthy. Interfejs przeglądarkowy pokazuje zobowiązania dowodowe; można w nim kierować strategiami automatycznymi lub stosować kroki ręczne w przypadkach, gdy procedura nie może się zakończyć.
Poprawność obliczeniowa
Dowody symboliczne (ProVerif, Tamarin) gwarantują bezpieczeństwo przy założeniu doskonałej kryptografii. Twierdzenia o poprawności obliczeniowej (Cortier, Backes) przenoszą dowody symboliczne na grunt bezpieczeństwa obliczeniowego, gdy protokół zostanie zbudowany z prymitywów, których bezpieczeństwo zostało dowiedzione.
F* i HACL*: zweryfikowane implementacje
F* (Microsoft Research) to język programowania ukierunkowany na dowodzenie. HACL* to biblioteka kryptograficzna napisana w F*, zawierająca zweryfikowane maszynowo dowody poprawności i odporności na kanały boczne. Jest używana w Firefox NSS i mbedTLS.
EasyCrypt: obliczeniowe dowody oparte na grach
EasyCrypt umożliwia przeprowadzanie w pełni obliczeniowych dowodów bezpieczeństwa opartych na grach dla konstrukcji kryptograficznych — nie tylko dla protokołów. Warstwa rekordów TLS 1.3 oraz ChaCha20-Poly1305 zostały zweryfikowane w EasyCrypt.
Praktyczne znaczenie
Formalnie zweryfikowana kryptografia trafia do zastosowań produkcyjnych: NSS (Firefox) korzysta z HACL*, AWS używa s2n-tls wraz z asercjami przenoszącymi dowody, a protokół Signal został zweryfikowany w ProVerif i Tamarin. Metody formalne nie są już wyłącznie akademickie.
Sprawdzenie wiedzy
Czym Tamarin różni się od ProVerif w obsłudze przypadków, w których automatyzacja zawodzi?
Podsumowanie lekcji
Tamarin wykorzystuje przepisywanie multizbiorów i rozumowanie oparte na śladach, korzystając z interaktywnego GUI do dowodzenia. Obsługuje teorie równościowe DH i XOR. Lematami wyraża się cele dotyczące poufności i uwierzytelniania. Poprawność obliczeniowa łączy dowody symboliczne z rzeczywistym bezpieczeństwem. HACL* i EasyCrypt rozszerzają weryfikację na implementacje i konstrukcje.
Ucz się Cryptology Academy dzięki korepetycjom AI — za darmo
Pisz i uruchamiaj kod w przeglądarce, otrzymuj natychmiastową pomoc od korepetytora AI dostępnego 24/7 i kontynuuj naukę w sieci lub w aplikacji.
- Kursy
- 67
- Lekcje
- 261
Często zadawane pytania
Czy lekcja „Tamarin i dowody obliczeniowe” jest bezpłatna?
Tak — pełny tekst „Tamarin i dowody obliczeniowe” 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 „Tamarin i dowody obliczeniowe”?
Użyć weryfikatora Tamarin do przepisywania multizbiorów i weryfikacji opartej na śladach Ć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 4 z 4.
Ile czasu zajmuje lekcja „Tamarin i dowody obliczeniowe”?
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