Perché le dimostrazioni informali non bastano

I progettisti di protocolli producono regolarmente argomentazioni informali sulla sicurezza: ragionamenti in prosa sul motivo per cui un attaccante non può avere successo. La storia dimostra che queste argomentazioni sono spesso errate, anche quando i protocolli sono progettati da esperti.

Needham-Schroeder (1978) è stato progettato per l'autenticazione reciproca. Nel 1995, Gavin Lowe ha scoperto un attacco man-in-the-middle utilizzando la verifica automatizzata, 17 anni dopo la pubblicazione. La dimostrazione informale non aveva rilevato un sottile attacco di replay.

WEP è stato approvato dall'IEEE nel 1997 sulla base di affermazioni informali sulla sicurezza. Nel 2001, i ricercatori hanno scoperto il riutilizzo del keystream RC4, collisioni degli IV e assenza di integrità, riuscendo a comprometterlo in pochi minuti. Il ragionamento informale non aveva rilevato nulla di tutto ciò.

La sicurezza dei protocolli dipende dalle interazioni tra numerose sessioni concorrenti, attaccanti attivi e assunzioni crittografiche. Il ragionamento umano fatica a gestire l'esplosione degli stati e le esecuzioni concorrenti intercalate.

I metodi formali modellano matematicamente il protocollo e dimostrano, oppure confutano, le proprietà di sicurezza (segretezza, autenticazione, forward secrecy) per tutte le possibili strategie dell'attaccante, non solo per quelle considerate dal progettista.

Simbolico (Dolev-Yao): la crittografia è una black box perfetta; l'attenzione si concentra sulla logica del protocollo. Computazionale: effettivi giochi di sicurezza probabilistici, più vicini alle garanzie del mondo reale. Entrambi individuano bug reali.

POODLE (2014) ha sfruttato un padding oracle nel CBC di SSL 3.0. La vulnerabilità era un difetto di progettazione a livello di protocollo, non un bug di implementazione. Un'analisi formale della specifica SSL 3.0 avrebbe segnalato l'oracolo prima della distribuzione.

TLS 1.3 (RFC 8446) è stato progettato insieme ad analisi formali utilizzando ProVerif e miTLS. La specifica è stata sottoposta a iterazioni sulla base dei risultati formali: una tappa fondamentale nell'adozione dei metodi formali da parte degli organismi di standardizzazione.

Gli strumenti formali verificano il modello del protocollo, non l'implementazione. Un protocollo verificato formalmente può comunque avere un'implementazione non sicura. F* / HACL* estende la verifica anche al codice crittografico.

La verifica formale è costosa: la modellazione del protocollo richiede settimane e competenze specialistiche. Tuttavia, per obiettivi di grande valore (TLS, SSH, Signal), il costo è giustificato: un singolo difetto del protocollo può interessare miliardi di utenti.

Che cosa ha reso significativa la scoperta di Lowe del 1995 sull'attacco a Needham-Schroeder?

Le dimostrazioni informali falliscono perché il ragionamento umano non rileva le interazioni tra sessioni concorrenti e le strategie degli attaccanti. Needham-Schroeder, WEP e POODLE presentavano tutti argomentazioni informali sulla sicurezza. TLS 1.3 ha integrato l'analisi formale durante la progettazione. Gli strumenti formali individuano i bug a livello di protocollo prima della distribuzione.