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.
Modeling a certified email protocol using I/O Automata / C. Blundo, S. Cimato, R. De Prisco, A.L. Ferrara. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 99:(2004), pp. 339-359. ((Intervento presentato al convegno MEFISTO Project tenutosi a Pisa nel 2003 [10.1016/j.entcs.2004.02.015].
Modeling a certified email protocol using I/O Automata
S. Cimato;
2004
Abstract
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
1-s2.0-S157106610405073X-main.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
338.22 kB
Formato
Adobe PDF
|
338.22 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
