Modeling A Certified Email Protocol using I/O Automata
Carlo Blundo, Stelvio Cimato, Roberto De Prisco, Anna Lisa Ferrara · Electronic Notes in Theoretical Computer Science · 2004
Describing and reasoning about asynchronous distributed systems is often a difficult and error prone task.In this paper we experiment the Input/Output Automata framework as a tool to describe and reason about cryptographic protocols running in an asynchronous distributed system.We examine a simple certified email protocol [5], give its formalization using the IOA model, and prove that some security properties are satisfied during the execution of the protocol.