Verified security protocol modeling and implementation with AnBx

AnBx è un'estensione della notazione Alice & Bob per la descrizione di protocolli, ed è utilizzato come linguaggio di specifica per la modellazione puramente dichiarativa dei protocolli distribuiti. AnBx è costituito da un insieme di astrazioni sui dati e sui modi di comunicazione che forniscono il supporto di base per le proprietà di sicurezza ad alto livello, schermando i dettagli della infrastruttura crittografica sottostante. AnBx, essendo implementato sul tool di verifica OFMC, è utilizzabile non solo per specifica e la progettazione ma anche per l'analisi della sicurezza dei protocolli distribuiti. Inoltre il framework consente la generazione automatica del codice Java di protocolli descritti in AnBx, mantenendo separate la logica del protocollo dalla logica dell'applicazione. L'efficacia del nostro approccio è mostrata nella specifica ed nell'analisi di due protocolli di pagamento elettronico usati nel mondo reale, realizzando proprietà di sicurezza più forti e più scalabili rispetto a quelle delle versioni originali. Nella seconda parte della tesi analizziamo in maniera formale il sistema di comunicazione veicolare sicura (SeVeCom) utilizzando il framework AIF, che è basato su una nuova tecnica di set-abstraction. Nel corso del lavoro abbiamo trovato due nuovi attacchi, e verificato che sotto ragionevoli ipotesi il sistema è sicuro.