Un approccio simbolico all'analisi di protocolli di sicurezza

Capitolo 1 Introduzione Lo scopo di questa tesi è quella di deteminare metodi che possano semplificare l’analisi compiuta su un protocollo crittografico. Un protocollo è un’insieme di regole che devono essere seguite affinchè due, o più partecipanti al protocollo, possano scambiarsi informazioni di qualunque natura; spesso si parla di protocolli crittografici riferendosi a quei protocolli per i quali vengono adottate particolari tecniche, dette crittografiche, per codificare i dati scambiati. Un attacco ad un protocollo è una violazione, da parte di un estraneo, delle regole che definiscono il protocollo stesso; individuare tali violazioni, significa simulare tutti i possibili comportamenti del sistema per determinare quali di questi conducono ad un comportamento erroneo del protocollo. 1.1 Scenario In questi ultimi anni si è intensificato l’utilizzo di internet e sistemi distribuiti, non solo in ambiti esclusivi come l’università e le grandi aziende, ma anche nella sfera priva- ta. Al crescere del volume e dell’importanza dei dati immagazzinati nei computer ed accessibili dall’esterno, la preoccupazione di garantire privacy e sicurezza è divenuta sempre maggiore. I sistemi di comunicazione sono divenuti complessi e dinamici per far fronte alle molteplici esigenze: la riservatezza è certamente importante ma anche l’integrità dei dati risulta, spesso, una caratteristica irrinunciabile. Se un nuovo utente si unisce ad un sistema, questo deve essere in grado di identificarlo per poi modificare il proprio comportamento e adattarsi alle nuove circostanze. Ciò non è facile, particolarmente 7