Model checking per l’analisi di un algoritmo di autenticazione a chiave pubblica

BB → A

{|N2. , N |}apk(A)A B

Quando l'iniziatore riceve questo messaggio, lo decripta. Poiché il messaggio contiene il nonce N, che l'iniziatore ha generato di recente e inviato criptato al risponditore, l'iniziatore conclude che il messaggio è stato effettivamente inviato di recente dal risponditore.

A → B

{|NB|}3. apk(B)

L'ultimo messaggio viene inviato in modo che il rispondente possa verificare le sue ipotesi. Egli spiega che il messaggio è recente, poiché N è recente. Inoltre, solo l'iniziatore e il rispondente conoscono N e il rispondente non ha inviato il messaggio. Quindi il messaggio deve provenire dall'iniziatore. Infine, l'iniziatore avrà ricevuto N come parte del messaggio del rispondente che conteneva anche N, quindi non avrebbe risposto a meno che N non fosse stato inviato di recente dall'iniziatore.

Sebbene questo argomento di correttezza informale possa sembrare convincente,

esso soffredel seguente attacco:(i i a)indica l'avversario e indica l'avversario che impersona l'agenteaa → i : {|a, N1. |} apk(i)aa i,L'agente avvia il protocollo nel ruolo di iniziatore, con l'obiettivo di comunicare con egenera un nuovo nonce N .a→ b : {|a,N2. i |}apk(b)a ai a a b,L'avversario utilizza il nonce di per impersonare e avvia un'istanza del protocollo conche svolge il ruolo di risponditore.b → a : {|N3. ,N |}apk(a)a bb a, arisponde correttamente ad generando nel frattempo il proprio nonce N . Dato che vede ilbi, i.nonce che ha inviato a presume che il messaggio provenga daa → i : {|N4. |}apk(i)ba i,risponde a seguendo le regole del ruolo di iniziatore del protocollo.ia → b : {|N5. |} apk(b)bi b b. bcripta nuovamente N con la chiave pubblica di e invia il risultato a Poiché si aspettaba, a aquesta risposta da conclude che condivide N e N con e da solo.a bb a, a bPoiché pensa di comunicare con e

né né si discostano dal protocollo e le loro chiavi non sono note all'avversario, si aspetta che N e N siano noti solo ad e a lui stesso. È chiaro che l'ipotesi di è violata dall'attacco. Ci sono due cose da notare su questo attacco. In primo luogo, non è intuitivo: osservando bene, si vede che l'argomentazione sulla sicurezza si basa sull'ipotesi che gli agenti non rivelino i segreti e che questa ipotesi sia violata da quando a b. inoltra il nonce di a Infatti, Needham e Schroeder fanno esplicitamente questa ipotesi nelloro articolo. In secondo luogo, l'attacco non dipende da alcuna falla nelle primitive crittografiche utilizzate e richiede solo un modello di avversario molto semplice. Le uniche operazioni sui dati che l'avversario impiega sono la concatenazione e la suddivisione dei messaggi, nonché la crittografia e la decriptazione. 7.2 Model Checking per i protocolli di sicurezza I protocolli di sicurezza

Sono un'altra area promettente per l'applicazione delle tecniche di Model Checking. La crescente quantità di informazioni riservate (come le transazioni monetarie) inviate su collegamenti di comunicazione insicuri (come Internet) richiede protocolli di crittografia sempre più sofisticati. Come i progetti hardware, questi protocolli possono avere sottili bug che sono difficili da trovare.

L'analisi formale dei protocolli di sicurezza è un ottimo esempio in cui il Model Checking viene applicato con successo. Sebbene i protocolli di sicurezza siano tipicamente di piccole dimensioni, l'analisi manuale è difficile, poiché un protocollo deve funzionare anche quando sono presenti un numero arbitrario di esecuzioni.

Sono state sviluppate tecniche di Model Checking specializzate che affrontano sia problemi di esecuzioni infinite, sia modelli di avversari prolifici e altamente non deterministici.

Queste tecniche sono state implementate in strumenti.

Di Model Checking che ora sono in grado di adattarsi a protocolli di dimensioni realistiche e possono essere utilizzati per aiutare la progettazione e la standardizzazione dei protocolli.

Il risultato è un modello in grado di catturare un'ampia classe di potenziali problemi di protocollo. Un modello di questo tipo, che è allo stesso tempo semplice e sufficientemente espressivo per catturare un'ampia classe di difetti di sicurezza non intuitivi, si presta bene al Model Checking. Non sorprende quindi che l'analisi dei protocolli rispetto a tali modelli sia stata una delle principali applicazioni del Model Checking nella sicurezza.

In pratica, si utilizza il Model Checker per trovare tutti i modi possibili in cui un avversario può interagire con un protocollo utilizzando combinazioni arbitrarie di intercettazione, reindirizzamento e le altre operazioni di base a sua disposizione.

Il model checking dei protocolli crittografici non è solo di interesse intellettuale.

Può fare molto per semplificare lo sviluppo e l'adozione degli standard di sicurezza. Nuovi protocolli crittografici vengono costantemente inventati con l'introduzione di nuovi paradigmi di comunicazione. Poiché un protocollo deve essere ampiamente utilizzato prima di essere utile, i nuovi protocolli vengono solitamente introdotti attraverso un processo di standardizzazione. Questo processo può essere lungo e controverso e gli standard possono essere difficili da modificare una volta in vigore. L'analisi formale può contribuire ad accelerare la standardizzazione, individuando tempestivamente i problemi e fornendo prove di sicurezza se non vengono riscontrati difetti. Inoltre, può anche aiutare a prevenire la standardizzazione di protocolli difettosi. Infine, il Model Checking ha il vantaggio che i controesempi che trova rappresentano attacchi reali al protocollo. Questo permette di capire quali sono le vulnerabilità di un protocollo e come mitigarle.

8. Promela nel Model Checking del protocollo

Una falla in un protocollo crittografico può diventare un vero e proprio problema di sicurezza. Anche un protocollo apparentemente piccolo può produrre in realtà un gran numero di comportamenti avversi possibili.

Questo capitolo tratta la rappresentazione dei modelli di protocollo nel linguaggio Promela: la scelta di questo strumento è dovuta alle sue efficaci tecniche di minimizzazione automatica e alla sua ampia diffusione nel campo della verifica.

Stephan Merz studiò il protocollo e le azioni di un potenziale attaccante in Promela, il linguaggio del model checker Spin. Si può quindi usare Spin per dimostrare che il protocollo può essere sovvertito.

Il modello del protocollo prevede alcune ipotesi semplificative:

• Ci sono tre attori: Bob, Alice e I, l'intruso (Intruder) che comunicano attraverso una rete comune.
• Ogni agente possiede una coppia di chiavi (non corrotta) e

costituisce un nonce.- Gli Agenti Alice e Bob sono rispettivamente l'iniziatore e il risponditore, che cercano di stabilire un segreto comune, rappresentato dalla loro coppia di nonces.- L'obiettivo del protocollo è cercare di convincere l'altro della loro presenza e identità.- L'intruso può partecipare alle esecuzioni del protocollo come qualsiasi altro agente, ma può anche falsificare i messaggi, utilizzando le informazioni intercettate dal traffico di rete.Tuttavia, anche l'intruso non può violare l'algoritmo crittografico, cioè non può decifrare i messaggi criptati con una chiave diversa dalla sua.Merz definisce innanzitutto alcuni tipi per facilitare la lettura delle specifiche:I messaggi sono costituiti da una chiave (la chiave pubblica del destinatario) e da due parti di dati.La decrittazione può essere modellata come un pattern-matching sulla voce della chiave:channel)La rete su cui avviene la

comunicazione. In Promela, la comunicazione sincrona è rappresentata da un canale con dimensione del buffer 0. Ciò significa che il trasmettitore deve aspettare quando il ricevitore non è pronto e viceversa. Il messaggio in transito è rappresentato come una "tripla" composta da un tag di identificazione #msg, il ricevitore e il corpo del messaggio crittografato. Il campo del destinatario identifica il destinatario previsto, anche se un Intruso può intercettare qualsiasi messaggio inviato in rete. Alice è ora modellata come un processo. In Promela, una delle possibili diverse istruzioni eseguibili (non deterministiche) viene presa nell'istruzione. Nel processo per Alice, Alice sceglie quindi Bob o l'intruso come partner di comunicazione nell'istruzione. Inizialmente, un attore (o B o I) viene scelto in modo non deterministico per la successiva comunicazione.

esecuzione(il token :: introduce le diverse alternative di selezione non deterministica), e la sua chiave pubblica viene cercata.

Alice invia quindi il primo messaggio all'interlocutore scelto e attende la risposta.

Verifica che il corpo del messaggio sia criptato con la sua chiave e che contenga il nonce inviato nel primo messaggio. (Promela consente di inserire condizioni booleane come dichiarazioni; una dichiarazione di questo tipo si blocca se la condizione risulta falsa).

Se la risposta ha la sua chiave e contiene il suo numero casuale come prima parte, Alice legge il segreto del suo partner. Quindi invia la sua risposta. Se il processo arriva a questo punto, lo stato di Alice è OK.

Bob è sviluppato in modo del tutto analogo. L'intruso cerca ora di decifrare e inoltrare i messaggi che riceve o, se non è in grado di decifrarli, di inoltrarli come li ha ricevuti.

L'intruso non segue un protocollo fisso (serve il Model Checker Spin per trovare l'attacco).

E vengono elencate semplicemente le diverse azioni che può eseguire.

La seconda alternativa rappresenta l'agente I che invia un messaggio. Ci sono due sottocasi: o riprodurre un messaggio precedentemente intercettato o costruire un nuovo messaggio dalle informazioni apprese finora.

Naturalmente, la maggior parte delle combinazioni risultanti possono essere immediatamente riconosciute come inappropriate dagli agenti onesti. Il nostro modello contiene quindi molti deadlocks, che ignoriamo durante la seguente analisi.

8.1 La verifica con SPIN

Per la verifica, è necessario esprimere la proprietà verificata come una formula LTL: Siano statusA, statusB i flag che indicano se l'esecuzione ha avuto successo rispetto