Verifica di protocolli di sicurezza crittografici

Capitolo 1 Introduzione L’avvento e l’espansione della rete mondiale Internet ha aperto un ventaglio infinito di possibilita` per l’uso dei calcolatori elettronici:dalla consultazione e gestione di archivi remoti alla programmazione distribuita, dalle video- conferenze al commercio elettronico. Tali impieghi possono essere riassunti con un unico scopo della rete : permettere la comunicazione tra due o piu` calcolatori lontani. Come nelle reti interne(LAN) le interazioni tra calcolatori vengono re- golate da protocolli. Ogni protocollo e` specifico per un tipo di interazione. Abbiamo ad esempio protocolli per la posta elettronica, protocolli per il trasferimento dati, protocolli per la consultazione di documenti, e cos`i via. In generale un protocollo di rete consiste in un insieme di passi che due o piu` calcolatori devono effettuare per portare a termine una transazione. I protocolli sono costituiti da un insieme di messaggi che gli agenti coin- volti si scambiamo mediante la rete, e da una serie di passi che regolano il comportamento di tali agenti. Tuttavia, nel momento in cui avvenga una interazione tra insieme di agenti, uno o piu` degli agenti coinvolti, per fini fraudolenti, potrebbero non eseguire correttamente il protocollo che regola tale tipo di interazione. Un evento di questo tipo viene definito attacco. Nel migliore dei casi gli agenti onesti si rendono conto di questo e l’interazione termina. Nel caso peggiore, l’esecuzione del protocollo viene completata e gli agenti maliziosi raggiun- gono i propri scopi. In questo caso si dice che l’attacco e` andato a buon fine. Per difendersi da tali attacchi sono nati i protocolli di sicurezza. Nella prima parte di questo documento verranno innanzitutto descritte e analiz- zate le piu` comuni problematiche di sicurezza, e alcune soluzioni presentate per rispondere a tali problematiche. Verranno descritti dei metodi formali 4