Sui Tipi Sessione, le Scelte Probabilistiche e il Tempo Polinomiale

I protocolli crittografici sono progettati per garantire comunicazioni protette su canali eventualmente controllati da utenti malintenzionati. Considerando le dimensioni crescenti delle reti di comunicazione e la loro dipendenza dai protocolli crittografici, risulta necessario un elevato livello di sicurezza in questi ultimi. Nel modello computazionale della crittografia moderna, le proprietà di sicurezza vengono definite in modo rigoroso e la verifica dei protocolli rispetto a tali proprietà viene effettuata mediante prove matematiche. In tale scenario si colloca il seguente progetto di tesi. L'obiettivo di questa tesi riguarda lo sviluppo di algebre di processo che siano in grado di rappresentare i protocolli crittografici nel senso del modello computazionale. L'algebra di processo indagata necessita di una nozione di scelta probabilistica e di vincoli di complessità computazionale per gli avversari. A tale fine, è stato definito un sistema di tipi sessione in grado di verificare la sicurezza dei protocolli. I problemi di scalabilità dei modelli relativi alla verifica automatica dei protocolli definiti secondo l'approccio computazionale sottolineano la rilevanza scientifica di questo elaborato. La radice di tali limitazioni risiede nella contemporanea presenza di non determinismo e scelte probabilistiche. Il sistema sviluppato nel presente progetto risulta essere, da una parte, sufficientemente permissivo da consentire la rappresentazione dei protocolli standard e delle prove per riduzione e, dall'altra, il più possibile restrittivo da impedire il non determinismo e i fenomeni di deadlock, in genere non presenti nel modello computazionale. Inoltre, gode di importanti proprietà quali Subject Reduction e limitazione polinomiale della complessità computazionale dei processi.