Mixnets e EasyCrypt: dimostrazioni crittografiche assistite da calcolatore

Negli ultimi anni l'avanzamento della ricerca in campo crittografico ha portato alla necessità di utilizzare strumenti software per la verifica delle prove formali. EasyCrypt è un tool, in fase di sviluppo, ideato per dimostrazioni basate su sequenze di giochi. Nella presente tesi viene presentato un caso di studio riguardante l'applicabilità di EasyCrypt alle mixing networks (abbr. mixnets). è presente un'esaustiva rassegna delle mixnets proposte in letteratura ed è descritta la teoria alla base delle dimostrazioni critografiche basate su sequenze di giochi. EasyCrypt viene analizzato nei suoi fondamenti teorici nonché nelle applicazioni pratiche, con riferimento particolare agli esperimenti svolti per la dimostrazione di proprietà di sicurezza delle mixnets.