Title :
I/O automaton models and proofs for shared-key communication systems
Author_Institution :
MIT Lab., Cambridge, MA, USA
Abstract :
The combination of two security protocols, a simple shared-key communication protocol and the Diffie-Hellman key distribution protocol, is modeled formally and proved correct. The modeling is based on the I/O automaton model for distributed algorithms, and the proofs are based on invariant assertions, simulation relations, and compositional reasoning. Arguments about the cryptosystems are handled separately from arguments about the protocols
Keywords :
automata theory; cryptography; distributed algorithms; protocols; simulation; Diffie-Hellman key distribution protocol; I/O automaton models; compositional reasoning; cryptosystems; distributed algorithms; invariant assertions; proofs; security protocols; shared-key communication systems; simulation relations; Automata; Computer science; Cryptography; Distributed algorithms; Distributed computing; Laboratories; Protocols; Reactive power; Read only memory; Security;
Conference_Titel :
Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE
Conference_Location :
Mordano
Print_ISBN :
0-7695-0201-6
DOI :
10.1109/CSFW.1999.779759
