Tamarin og beregningsmæssige beviser
Brug Tamarin prover til multiset rewriting og sporbaseret verifikation.
Tamarin og beregningsmæssige beviser er en gratis Cryptology Academy-lektion på CoddyKit. Dette er lektion 4 af 4. Du kan læse hele lektionen gratis nedenfor — og derefter øve dig praktisk i browseren med en indbygget kodeeditor og en AI-vejleder, der er tilgængelig døgnet rundt. Den er en del af læringsforløbet i Cryptology Academy, og dine fremskridt synkroniseres på tværs af nettet og CoddyKit-appen. Cryptology Academy-kurset indeholder 4 lektioner i alt.
Hvad er Tamarin?
Tamarin (ETH Zurich, 2012) er et værktøj til verifikation af sikkerhedsprotokoller baseret på omskrivning af multimængder. I modsætning til ProVerifs tilgang med Horn-klausuler ræsonnerer Tamarin over spor af protokoludførelser med en interaktiv bevissøger.
Tamarin kontra ProVerif
ProVerif: fuldautomatisk, men kan give "cannot be proved." Tamarin: interaktiv bevishjælper + automatisk tilstand, som håndterer ækvationsteorier (XOR, Diffie-Hellman, bilineære afbildninger). Mere udtryksfuldt, men med en stejlere læringskurve.
Regler for omskrivning af multimængder
Tamarin modellerer protokoller som omskrivningsregler for fakta. Fakta repræsenterer tilstand. En regel [ L ] --[ A ]-> [ R ] forbruger fakta på venstresiden L, producerer fakta på højresiden R og registrerer handlingen A i sporet.
Tam arins inputsprog (.spthy)
En Tamarin-teorifil deklarerer funktioner, ligninger, regler og lemmaer:
/* 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) ]Angivelse af lemmaer
Sikkerhedsmål udtrykkes som lemmaer over spor:
/* 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"Kørsel af Tamarin
Start Tam arins interaktive grafiske brugerflade: tamarin-prover interactive my_protocol.spthy. Brugerfladen i browseren viser bevisforpligtelser; du kan styre automatiserede strategier eller anvende manuelle trin i tilfælde, der ikke afsluttes.
Beregningsmæssig sundhed
Symbolske beviser (ProVerif, Tamarin) garanterer sikkerhed under antagelser om perfekt kryptografi. Sætninger om beregningsmæssig sundhed (Cortier, Backes) løfter symbolske beviser til beregningsmæssig sikkerhed, når de instansieres med primitiver, hvis sikkerhed kan bevises.
F* og HACL*: Verificerede implementeringer
F* (Microsoft Research) er et bevisorienteret programmeringssprog. HACL* er et kryptografisk bibliotek skrevet i F* med maskinverificerede beviser for korrekthed og modstandsdygtighed over for sidekanalangreb. Det anvendes i Firefox NSS og mbedTLS.
EasyCrypt: Beregningsmæssige spilbaserede beviser
EasyCrypt gør det muligt at udarbejde fuldt beregningsmæssige, spilbaserede sikkerhedsbeviser for kryptografiske konstruktioner — ikke kun protokoller. TLS 1.3's postlag og ChaCha20-Poly1305 er blevet verificeret i EasyCrypt.
Praktisk betydning
Formelt verificeret kryptografi er ved at blive taget i brug i produktion: NSS (Firefox) bruger HACL*, AWS bruger s2n-tls med bevisbærende påstande, og Signal-protokollen er blevet verificeret i ProVerif og Tamarin. Formelle metoder er ikke længere kun akademiske.
Videntest
Hvordan adskiller Tamarin sig fra ProVerif i håndteringen af tilfælde, hvor automatiseringen mislykkes?
Opsummering af lektionen
Tamarin bruger omskrivning af multimængder og sporbจaseret ræsonnering med en interaktiv bevissøger. Det håndterer ækvationsteorier for DH og XOR. Lemmaer udtrykker mål for hemmeligholdelse og autentificering. Beregningsmæssig sundhed bygger bro mellem symbolske beviser og reel sikkerhed. HACL* og EasyCrypt udvider verifikationen til implementeringer og konstruktioner.
Lær Cryptology Academy med en AI-underviser — gratis
Skriv og kør rigtig kode i din browser, få øjeblikkelig hjælp fra en AI-underviser døgnet rundt, og fortsæt, hvor du slap, på web eller i appen.
- Kurser
- 67
- Lektioner
- 261
Ofte stillede spørgsmål
Er lektionen “Tamarin og beregningsmæssige beviser” gratis?
Ja — hele teksten til “Tamarin og beregningsmæssige beviser” kan læses gratis her på nettet. Hvis du vil øve dig interaktivt med en indbygget kodeeditor og en AI-vejleder døgnet rundt og få adgang til resten af Cryptology Academy-kurset, skal du opgradere til CoddyKit PRO. Cryptology Academy-kurset indeholder 4 lektioner i alt.
Hvad lærer jeg i “Tamarin og beregningsmæssige beviser”?
Brug Tamarin prover til multiset rewriting og sporbaseret verifikation. Du øver dig i Cryptology Academy med praktisk kode, som du kører direkte i browseren, og en AI-vejleder døgnet rundt besvarer dine spørgsmål, mens du arbejder dig gennem lektionen.
Skal jeg have erfaring for at begynde på Cryptology Academy?
Der kræves ingen tidligere erfaring. Cryptology Academy på CoddyKit er tilrettelagt for både begyndere og øvede, så du kan starte her eller fra begyndelsen og lære i dit eget tempo. Dette er lektion 4 af 4.
Hvor lang tid tager lektionen “Tamarin og beregningsmæssige beviser”?
De fleste CoddyKit-lektioner tager cirka 5–10 minutter. Hver lektion er kort og interaktiv, så du gør løbende fremskridt og kan fortsætte, hvor du slap – på både web og app.
Kan jeg skrive og køre kode i denne Cryptology Academy-lektion?
Ja. Alle Cryptology Academy-lektioner har en indbygget kodeeditor, så du kan skrive og køre rigtig kode direkte i din browser og få øjeblikkelig feedback fra AI – uden lokal opsætning.
Alle lektioner i dette kursus
- Hvorfor uformelle beviser ikke er nok
- Dolev-Yao-angriber modellen og symbolsk kryptografi
- ProVerif: Automatiseret protokolverifikation
- Tamarin og beregningsmæssige beviser