Modeling A Certified Email Protocol using I/O Automata | Zendy

Carlo Blundo | Zendy; Stelvio Cimato | Zendy; Roberto De Prisco | Zendy; Anna Lisa Ferrara | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Modeling A Certified Email Protocol using I/O Automata

Author(s) -

Carlo Blundo,

Stelvio Cimato,

Roberto De Prisco,

Anna Lisa Ferrara

Publication year - 2004

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.02.015

Subject(s) - computer science , asynchronous communication , protocol (science) , cryptographic protocol , automaton , certification , theoretical computer science , simple (philosophy) , cryptography , task (project management) , distributed computing , model checking , programming language , algorithm , computer network , medicine , philosophy , alternative medicine , management , epistemology , pathology , political science , law , economics

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research