Il protocollo Needham-Schroeder e gli attacchi

Il protocollo Needham-Schroeder (1978) è stato uno dei primi tentativi formali di progettare un protocollo di autenticazione crittografica utilizzando una terza parte fidata (TTP). L'obiettivo era consentire a due parti, Alice e Bob, di autenticarsi reciprocamente e stabilire una chiave di sessione condivisa utilizzando un server di autenticazione fidato (AS), che condivide chiavi a lungo termine con ciascuna entità. Il protocollo precede l'infrastruttura a chiave pubblica, ma ha introdotto concetti, come i nonce per garantire la freschezza e la distribuzione delle chiavi tramite un server fidato, che rimangono centrali in protocolli moderni come Kerberos. La comprensione di NS e dei suoi punti deboli ha contribuito a plasmare l'intero campo dell'analisi dei protocolli.

Il protocollo NS a chiave simmetrica si articola in cinque passaggi. (1) Alice invia {A, B, Na} all'AS, richiedendo una chiave di sessione per comunicare con Bob. (2) L'AS risponde ad Alice con {Na, B, Kab, {Kab, A}_Kb}_Ka — una chiave di sessione Kab e un ticket per Bob, il tutto cifrato con la chiave a lungo termine Ka di Alice. (3) Alice inoltra a Bob il ticket {Kab, A}_Kb. (4) Bob decifra il ticket, estrae Kab e invia {Nb}_Kab ad Alice, come challenge. (5) Alice risponde con {Nb-1}_Kab, dimostrando di possedere Kab. Il nonce Nb impedisce il replay del passaggio 4. Questo protocollo è soggetto a un noto attacco di replay sfruttato da Denning e Sacco (1981).

Denning e Sacco (1981) hanno scoperto un difetto: la risposta dell'AS nel passaggio 2 non garantisce la freschezza, perché non contiene un timestamp o un nonce generato dal server. Un attaccante, Mallory, che in precedenza aveva intercettato una vecchia chiave di sessione Kab compromettendo una sessione passata, può riprodurre il vecchio ticket {Kab, A}_Kb in qualunque momento successivo. Bob, ricevendo quello che sembra un ticket legittimo proveniente da Alice, utilizza la chiave compromessa Kab per la sessione. La correzione proposta da Denning e Sacco consiste nell'aggiungere un timestamp alla risposta dell'AS e al ticket. Questa soluzione è stata adottata in Kerberos: i timestamp sono incorporati nei ticket per limitarne il periodo di validità.

Il protocollo NS a chiave pubblica, anch'esso del 1978, è stato progettato per l'autenticazione reciproca tra due parti mediante la crittografia a chiave pubblica. (1) Alice invia {Na, A}_PKb a Bob, con il nonce Na cifrato con la chiave pubblica di Bob. (2) Bob risponde con {Na, Nb}_PKa, entrambi i nonce cifrati con la chiave pubblica di Alice. (3) Alice risponde con {Nb}_PKb, restituendo il nonce di Bob cifrato con la sua chiave pubblica. Dopo questo scambio, entrambe le parti possiedono entrambi i nonce (Na, Nb) e possono derivare una chiave di sessione. Il protocollo è sembrato sicuro per 17 anni, fino all'attacco di Lowe del 1995.

Gavin Lowe (1995) ha scoperto un difetto critico utilizzando il model checker Failures in Compositional Reasoning (FDR). Mallory può impersonare Bob nei confronti di Alice inoltrando i messaggi a un Bob onesto. Passaggio 1: Alice invia {Na, A}_PKm a Mallory, pensando di parlare con Bob. Mallory inoltra {Na, A}_PKb a Bob. Passaggio 2: Bob risponde con {Na, Nb}_PKa, che Mallory decifra e ricifra per Alice: {Na, Nb}_PKa. Alice decifra il messaggio ed estrae Nb. Passaggio 3: Alice invia {Nb}_PKm, pensando che il messaggio sia diretto a Bob. Mallory lo decifra e inoltra {Nb}_PKb a Bob. Bob crede di aver completato un'autenticazione reciproca con Alice, ma Alice si sta in realtà autenticando con Mallory. La correzione consiste nel fatto che, al passaggio 2, Bob deve includere la propria identità: {Na, Nb, B}_PKa.

La correzione di Lowe al protocollo NSPK è semplice, ma fondamentale: la risposta di Bob nel passaggio 2 deve includere l'identità B di Bob, diventando {Na, Nb, B}_PKa. Ora, quando Alice riceve la risposta, verifica che l'identità B inclusa corrisponda alla parte con cui intendeva comunicare. Mallory non può sostituire la propria risposta: per costruire un valore valido {Na, Nb, M}_PKa che superi il controllo di Alice, avrebbe bisogno della chiave privata di Alice. Questa idea è nota come Needham-Abadi Principle: i messaggi di autenticazione devono associare esplicitamente l'identità del mittente, senza affidarsi soltanto al contesto per identificarlo.

La scoperta del difetto di NSPK da parte di Lowe è stata agevolata dal model checker FDR (Failures-Divergences Refinement), che esplora esaustivamente tutte le possibili esecuzioni del protocollo, compresi gli interventi dell'avversario. Ciò ha favorito lo sviluppo di strumenti per l'analisi formale dei protocolli: Proverif, basato sul calcolo pi applicato, può dimostrare o confutare proprietà di autenticazione e segretezza in sessioni infinite. Tamarin Prover usa la riscrittura di multinsiemi e supporta protocolli complessi come TLS 1.3 e Signal. AVISPA e Scyther sono altri strumenti. I moderni progetti di protocolli, tra cui TLS 1.3, Signal e Noise, vengono sottoposti a verifica formale prima della distribuzione: un'eredità diretta dell'episodio NS/Lowe.

Gli attacchi a NS hanno chiarito la distinzione tra gli obiettivi dell'autenticazione. Autenticazione dell'entità: dimostrare che una parte è attualmente attiva e partecipa al protocollo; la freschezza è importante. Autenticazione dell'origine dei dati: dimostrare che un messaggio specifico è stato creato da una parte specifica; ciò potrebbe non implicare che la parte sia ancora attiva. L'attacco di Lowe compromette l'autenticazione dell'entità: Alice crede di autenticarsi con Bob, ma in realtà si sta autenticando con Mallory, che inoltra i messaggi a Bob. Le specifiche dei protocolli moderni dichiarano gli obiettivi in modo preciso: "Alice è autenticata presso Bob in qualità di iniziatrice di questa sessione." Obiettivi vaghi portano a specifiche ambigue, che superano la revisione informale ma falliscono l'analisi formale.

Un'altra classe di attacchi correlati a NS è l'attacco di riflessione: Mallory ripropone ad Alice i messaggi che Alice stessa ha inviato. Se il protocollo è simmetrico, cioè entrambe le parti usano la stessa chiave e lo stesso formato dei messaggi, Alice potrebbe accettare la propria sfida come risposta valida di Bob. Una difesa consiste nell'usare direzioni di chiave diverse, con chiavi separate di cifratura e decifratura per ciascuna direzione, oppure nell'includere indicatori di ruolo nei messaggi, ad esempio inserendo "I am initiator" nel messaggio cifrato. I protocolli moderni come TLS includono stringhe di etichette specifiche per il ruolo nelle chiavi derivate con HKDF, usando "c e traffic" per il client e "s hs traffic" per il server, così da impedire la riflessione.

Gli attacchi di interleaving combinano messaggi provenienti da più sessioni di protocollo concorrenti per falsificare l'autenticazione. Se Alice esegue due sessioni simultanee, Mallory può mescolare i messaggi di entrambe per creare una sessione combinata coerente, ma non valida, che autentica Mallory. La difesa consiste nel vincolo della sessione: ogni messaggio deve essere legato crittograficamente al contesto della propria sessione, ad esempio includendo un identificatore di sessione o usando una chiave univoca per ogni sessione. TLS impedisce l'interleaving tramite il messaggio Finished, che contiene un MAC sull'intero transcript della sessione corrente. Qualsiasi messaggio intercalato modifica il transcript e invalida il valore Finished.

I protocolli Needham-Schroeder hanno influenzato direttamente la progettazione di Kerberos, con i timestamp per impedire i replay, ripresi dalla correzione di Denning-Sacco; di TLS, il cui MAC del transcript nel messaggio Finished impedisce interleaving e riflessione; del Signal Protocol, con il vincolo della sessione ottenuto tramite lo stato del ratchet; e del Noise Protocol Framework, con l'associazione dell'identità nei pattern di handshake. Gli attacchi a NS hanno dimostrato che le argomentazioni informali sulla sicurezza non sono sufficienti: ogni protocollo deve essere analizzato contro un avversario attivo che controlla la rete e può riprodurre, riordinare e modificare i messaggi. Questo modello di avversario, noto come Dolev-Yao, è oggi lo standard nella verifica formale dei protocolli.

Il protocollo simmetrico Needham-Schroeder (1978) introdusse la distribuzione delle chiavi di sessione basata su una TTP. L'attacco di Denning-Sacco (1981) individuò una vulnerabilità ai replay, corretta introducendo i timestamp in Kerberos. Il protocollo NSPK a chiave pubblica subì un attacco MITM individuato da Lowe (1995) tramite model checking, corretto includendo l'identità del mittente nei messaggi. Questi attacchi hanno stabilito che la verifica formale, con strumenti come Proverif e Tamarin, è essenziale per la progettazione dei protocolli. Le lezioni principali sono: i messaggi devono associare l'identità del mittente, le sessioni devono essere isolate l'una dall'altra, gli attacchi di riflessione si prevengono con la derivazione direzionale delle chiavi e gli attacchi di interleaving si prevengono con MAC sui transcript.