Analisi statica dello Spi-calcolo

In questo lavoro ci proponiamo quindi di analizzare i protocolli di comunicazione, utilizzando lo Spi-calcolo come modello per poterli rappresentare. Lo Spi-calcolo estende un particolare modello per la connessione dei sistemi interattivi (il Ï€-calcolo) al quale vengono aggiunte le operazioni comuni nei protocolli di sicurezza. Vi sono molti dialetti dello Spi-calcolo, noi considereremo quello proposto in [3] che utilizza una semantica di tipo “late” [26]