Tamarin e dimostrazioni computazionali
Utilizzi il prover Tamarin per la riscrittura di multinsiemi e la verifica basata su tracce.
Tamarin e dimostrazioni computazionali è una lezione Cryptology Academy gratuita su CoddyKit. Questa è la lezione 4 di 4. Puoi leggere la lezione completa qui gratuitamente — poi esercitati direttamente nel browser con un editor di codice integrato e un tutor IA disponibile 24/7. Fa parte del percorso di apprendimento Cryptology Academy, e i tuoi progressi si sincronizzano tra il web e l'app CoddyKit. Il corso Cryptology Academy include 4 lezioni in totale.
Che cos'è Tamarin?
Tamarin (ETH Zurich, 2012) è uno strumento per la verifica dei protocolli di sicurezza basato sulla riscrittura di multinsiemi. A differenza dell'approccio basato su clausole di Horn di ProVerif, Tamarin ragiona sulle tracce delle esecuzioni del protocollo con un dimostratore interattivo.
Tamarin e ProVerif a confronto
ProVerif: completamente automatizzato, può restituire "cannot be proved." Tamarin: assistente interattivo per le dimostrazioni con modalità automatica, gestisce teorie equazionali (XOR, Diffie-Hellman, mappe bilineari). È più espressivo, ma presenta una curva di apprendimento più ripida.
Regole di riscrittura dei multinsiemi
Tamarin modella i protocolli come regole di riscrittura applicate ai fatti. I fatti rappresentano lo stato. Una regola [ L ] --[ A ]-> [ R ] consuma i fatti a sinistra L, produce i fatti a destra R e registra l'azione A nella traccia.
Linguaggio di input di Tamarin (.spthy)
Un file di teoria Tamarin dichiara funzioni, equazioni, regole e lemmi:
/* 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) ]Definizione dei lemmi
Gli obiettivi di sicurezza sono espressi come lemmi sulle tracce:
/* 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"Esecuzione di Tamarin
Avvii la GUI interattiva di Tamarin: tamarin-prover interactive my_protocol.spthy. L'interfaccia del browser mostra gli obblighi di dimostrazione; può guidare le strategie automatizzate o applicare manualmente dei passaggi nei casi non terminanti.
Solidità computazionale
Le dimostrazioni simboliche (ProVerif, Tamarin) garantiscono la sicurezza assumendo una crittografia perfetta. I teoremi di solidità computazionale (Cortier, Backes) estendono le dimostrazioni simboliche alla sicurezza computazionale quando vengono utilizzate primitive la cui sicurezza è stata dimostrata.
F* e HACL*: implementazioni verificate
F* (Microsoft Research) è un linguaggio di programmazione orientato alle dimostrazioni. HACL* è una libreria crittografica scritta in F*, con dimostrazioni verificate dalla macchina sulla correttezza e sulla resistenza agli attacchi a canale laterale. È utilizzata in Firefox NSS e mbedTLS.
EasyCrypt: dimostrazioni computazionali basate su giochi
EasyCrypt consente di realizzare dimostrazioni di sicurezza completamente computazionali (basate su giochi) per le costruzioni crittografiche, non solo per i protocolli. Il livello record di TLS 1.3 e ChaCha20-Poly1305 sono stati verificati in EasyCrypt.
Impatto pratico
La crittografia verificata formalmente sta entrando in produzione: NSS (Firefox) utilizza HACL*, AWS utilizza s2n-tls con asserzioni accompagnate da prove e il protocollo Signal è stato verificato in ProVerif e Tamarin. I metodi formali non sono più soltanto accademici.
Verifica delle conoscenze
In che modo Tamarin si differenzia da ProVerif nella gestione dei casi in cui l'automazione non riesce?
Riepilogo della lezione
Tamarin utilizza la riscrittura di multinsiemi e il ragionamento basato sulle tracce con una GUI interattiva per le dimostrazioni. Gestisce le teorie equazionali DH e XOR. I lemmi esprimono gli obiettivi di segretezza e autenticazione. La solidità computazionale collega le dimostrazioni simboliche alla sicurezza reale. HACL* ed EasyCrypt estendono la verifica alle implementazioni e alle costruzioni crittografiche.
Impara Cryptology Academy con un tutor IA — gratis
Scrivi ed esegui vero codice nel tuo browser, ricevi aiuto istantaneo da un tutor IA disponibile 24/7, e riprendi da dove hai lasciato sul web o nell'app.
- Corsi
- 67
- Lezioni
- 261
Domande Frequenti
La lezione «Tamarin e dimostrazioni computazionali» è gratuita?
Sì — il testo completo di «Tamarin e dimostrazioni computazionali» è gratuito qui sul web. Per esercitarvi in modo interattivo (un editor di codice integrato e un tutor IA 24/7) e sbloccare il resto del corso Cryptology Academy, passa a CoddyKit PRO. Il corso Cryptology Academy include 4 lezioni in totale.
Cosa imparerò in «Tamarin e dimostrazioni computazionali»?
Utilizzi il prover Tamarin per la riscrittura di multinsiemi e la verifica basata su tracce. Eserciti Cryptology Academy con codice pratico che esegui direttamente nel browser, e un tutor IA 24/7 risponde alle tue domande mentre lavori sulla lezione.
Ho bisogno di esperienza per iniziare Cryptology Academy?
Non è richiesta alcuna esperienza precedente. Cryptology Academy su CoddyKit è strutturato per principianti e studenti avanzati, quindi puoi iniziare da qui o dall'inizio e procedere al tuo ritmo. Questa è la lezione 4 di 4.
Quanto tempo richiede la lezione «Tamarin e dimostrazioni computazionali»?
La maggior parte delle lezioni CoddyKit richiede circa 5–10 minuti. Ogni lezione è breve e interattiva, quindi fai progressi costanti e riprendi esattamente da dove hai lasciato su web e app.
Posso scrivere ed eseguire codice in questa lezione Cryptology Academy?
Sì. Ogni lezione Cryptology Academy include un editor di codice integrato, quindi scrivi ed esegui codice reale direttamente nel tuo browser e ricevi feedback istantaneo dall'IA — nessuna configurazione locale necessaria.
Tutte le lezioni di questo corso
- Perché le dimostrazioni informali non bastano
- Modello di attacco Dolev-Yao e crittografia simbolica
- ProVerif: verifica automatizzata dei protocolli
- Tamarin e dimostrazioni computazionali