ProVerif: verifica automatizzata dei protocolli
Specifichi e verifichi le proprietà dell'handshake TLS con ProVerif.
ProVerif: verifica automatizzata dei protocolli è una lezione Cryptology Academy gratuita su CoddyKit. Questa è la lezione 3 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'è ProVerif?
ProVerif (Bruno Blanchet, 2001) è uno strumento automatizzato per la verifica dei protocolli crittografici. Riceve un protocollo descritto nel calcolo pi applicato e determina automaticamente le proprietà di segretezza e autenticazione.
Come funziona ProVerif
ProVerif traduce il protocollo in clausole di Horn e applica un algoritmo basato sulla risoluzione per dedurre ciò che l'attaccante può apprendere. Se un fatto di segretezza è derivabile, il protocollo è compromesso; altrimenti, ne viene dimostrata la sicurezza.
Linguaggio di input di ProVerif
I protocolli vengono descritti in modo dichiarativo: si dichiarano canali, tipi, funzioni (enc, dec, sign, verify), equazioni (dec(enc(m,k),k)=m) e processi che comunicano attraverso i canali.
Dichiarazione delle primitive crittografiche
Esempio di dichiarazioni 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.Scrittura di un semplice processo di protocollo
Si modellano Alice e Bob come processi paralleli:
(* 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)))Definizione delle query di sicurezza
ProVerif verifica query come:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpretazione dell'output di ProVerif
ProVerif restituisce "RESULT ... is true" (sicurezza dimostrata) oppure "RESULT ... is false" e stampa una traccia di attacco come controesempio, mostrando i messaggi dell'attaccante. La traccia mostra esattamente come funziona l'attacco.
Verifica di TLS 1.3 con ProVerif
Bhargavan et al. (2016) hanno utilizzato ProVerif per analizzare un modello di TLS 1.3. Hanno trovato e segnalato un attacco al meccanismo di ripresa 0-RTT, che è stato corretto prima della finalizzazione dell'RFC.
Limitazioni: approssimazione e cicli
ProVerif calcola un'approssimazione per eccesso: può segnalare attacchi inesistenti (dire "false" quando il protocollo è in realtà sicuro), ma non perde mai gli attacchi reali. Le sessioni di protocollo non limitate potrebbero non terminare: ProVerif espande i cicli in modo euristico.
Quando ProVerif restituisce "Cannot Be Proved"
Se ProVerif non riesce a determinare il risultato nell'ambito della propria approssimazione, restituisce "CANNOT BE PROVED." Questo non dimostra che il protocollo sia insicuro: significa che lo strumento ha esaurito la propria capacità euristica. In questi casi Tamarin potrebbe riuscire.
Verifica delle conoscenze
Che cosa significa l'output di ProVerif "RESULT ... is false" per una query di segretezza?
Riepilogo della lezione
ProVerif automatizza la verifica dei protocolli utilizzando la risoluzione su clausole di Horn. I protocolli sono scritti nel calcolo pi applicato con equazioni crittografiche. Le query riguardano segretezza e autenticazione. False significa sicurezza dimostrata; true significa protocollo compromesso (con relativa traccia di attacco). Limitazioni: le approssimazioni possono restituire "cannot be proved."
Domande Frequenti
La lezione «ProVerif: verifica automatizzata dei protocolli» è gratuita?
Sì — il testo completo di «ProVerif: verifica automatizzata dei protocolli» è 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 «ProVerif: verifica automatizzata dei protocolli»?
Specifichi e verifichi le proprietà dell'handshake TLS con ProVerif. 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 3 di 4.
Quanto tempo richiede la lezione «ProVerif: verifica automatizzata dei protocolli»?
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