Tamarin og beregningsmessige bevis
Bruk Tamarin prover til multiset-rewriting og sporbasert verifisering.
Tamarin og beregningsmessige bevis er en gratis leksjon i Cryptology Academy på CoddyKit. Dette er leksjon 4 av 4. Du kan lese hele leksjonen gratis nedenfor – og deretter øve praktisk i nettleseren med en innebygd kodeeditor og en AI-veileder som er tilgjengelig døgnet rundt. Den er en del av læringsløpet i Cryptology Academy, og fremdriften din synkroniseres mellom nettet og CoddyKit-appen. Kurset i Cryptology Academy inneholder totalt 4 leksjoner.
Hva er Tamarin?
Tamarin (ETH Zurich, 2012) er en verifikator for sikkerhetsprotokoller basert på omskriving av multisett. I motsetning til ProVerifs Horn-klausulbaserte tilnærming resonnerer Tamarin over spor av protokollkjøringer med en interaktiv bevisassistent.
Tamarin kontra ProVerif
ProVerif: fullstendig automatisert, men kan gi «cannot be proved». Tamarin: interaktiv bevisassistent med en automatisert modus, og håndterer ekvasjonsteorier (XOR, Diffie-Hellman, bilineære avbildninger). Mer uttrykksfullt, men med en brattere læringskurve.
Regler for omskriving av multisett
Tamarin modellerer protokoller som omskrivingsregler over fakta. Fakta representerer tilstand. En regel [ L ] --[ A ]-> [ R ] bruker fakta på venstresiden L, produserer fakta på høyresiden R og logger handlingen A i sporet.
Tamarins inndataspråk (.spthy)
En Tamarin-teorifil deklarerer funksjoner, 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) ]Angi lemmaer
Sikkerhetsmål uttrykkes 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"Kjøre Tamarin
Start Tamarins interaktive GUI: tamarin-prover interactive my_protocol.spthy. Nettlesergrensesnittet viser bevisforpliktelser. De kan styre automatiserte strategier eller bruke manuelle trinn i tilfeller som ikke terminerer.
Beregningsmessig soundness
Symbolske bevis (ProVerif, Tamarin) garanterer sikkerhet under antakelser om perfekt kryptografi. Teoremer om computational soundness (Cortier, Backes) løfter symbolske bevis til beregningsmessig sikkerhet når de instansieres med primitiver som har beviselig sikkerhet.
F* og HACL*: Verifiserte implementasjoner
F* (Microsoft Research) er et bevisorientert programmeringsspråk. HACL* er et kryptografisk bibliotek skrevet i F*, med maskinverifiserte bevis for korrekthet og motstandsdyktighet mot sidekanalangrep. Det brukes i Firefox NSS og mbedTLS.
EasyCrypt: Beregningsmessige spillbaserte bevis
EasyCrypt muliggjør fullstendig beregningsmessige, spillbaserte sikkerhetsbevis for kryptografiske konstruksjoner – ikke bare protokoller. TLS 1.3-recordlaget og ChaCha20-Poly1305 er verifisert i EasyCrypt.
Praktisk betydning
Formelt verifisert kryptografi tas nå i bruk i produksjon: NSS (Firefox) bruker HACL*, AWS bruker s2n-tls med bevisførende påstander, og Signal-protokollen er verifisert i ProVerif og Tamarin. Formelle metoder er ikke lenger bare akademiske.
Kunnskapstest
Hvordan skiller Tamarin seg fra ProVerif når automatiseringen ikke lykkes?
Oppsummering av leksjonen
Tamarin bruker omskriving av multisett og sporbassert resonnering med et interaktivt bevisgrensesnitt. Det håndterer ekvasjonsteorier for DH og XOR. Lemmaer uttrykker mål for hemmelighold og autentisering. Beregningsmessig soundness bygger bro fra symbolske bevis til reell sikkerhet. HACL* og EasyCrypt utvider verifiseringen til implementasjoner og konstruksjoner.
Lær deg Cryptology Academy med en AI-veileder – gratis
Skriv og kjør ekte kode i nettleseren, få umiddelbar hjelp fra en AI-veileder som er tilgjengelig døgnet rundt, og fortsett der du slapp – på nettet eller i appen.
- Kurs
- 67
- Leksjoner
- 261
Ofte stilte spørsmål
Er leksjonen «Tamarin og beregningsmessige bevis» gratis?
Ja – hele teksten i «Tamarin og beregningsmessige bevis» er gratis å lese her på nettet. For å øve interaktivt med en innebygd kodeeditor og en AI-veileder som er tilgjengelig døgnet rundt, og for å låse opp resten av Cryptology Academy-kurset, kan du oppgradere til CoddyKit PRO. Kurset i Cryptology Academy inneholder totalt 4 leksjoner.
Hva lærer jeg i «Tamarin og beregningsmessige bevis»?
Bruk Tamarin prover til multiset-rewriting og sporbasert verifisering. Du øver på Cryptology Academy med praktisk kode som du kjører direkte i nettleseren, mens en AI-veileder som er tilgjengelig døgnet rundt, svarer på spørsmålene dine mens du jobber deg gjennom leksjonen.
Trenger jeg erfaring for å begynne med Cryptology Academy?
Ingen tidligere erfaring er nødvendig. Cryptology Academy på CoddyKit er lagt opp for både nybegynnere og viderekomne, så De kan begynne her eller helt fra start og lære i Deres eget tempo. Dette er leksjon 4 av 4.
Hvor lang tid tar leksjonen «Tamarin og beregningsmessige bevis»?
De fleste CoddyKit-leksjoner tar omtrent 5–10 minutter. Hver leksjon er kort og interaktiv, slik at De gjør jevne fremskritt og kan fortsette akkurat der De slapp – både på nettet og i appen.
Kan jeg skrive og kjøre kode i denne Cryptology Academy-leksjonen?
Ja. Alle Cryptology Academy-leksjoner har en innebygd kodeeditor, slik at De kan skrive og kjøre ekte kode direkte i nettleseren og få umiddelbar tilbakemelding fra AI – uten lokal konfigurering.
Alle leksjonene i dette kurset
- Hvorfor uformelle bevis ikke er nok
- Dolev-Yao-angripermodellen og symbolsk kryptografi
- ProVerif: automatisert protokollverifisering
- Tamarin og beregningsmessige bevis