I/O automaton models and proofs for shared-key communication systems
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 2 (10636900) , 14-29
- https://doi.org/10.1109/csfw.1999.779759
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
This publication has 9 references indexed in Scilit:
- Secure implementation of channel abstractionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The inductive approach to verifying cryptographic protocolsJournal of Computer Security, 1998
- Protection in programming-language translationsPublished by Springer Nature ,1998
- Implementing sequentially consistent shared objects using broadcast and point-to-point communicationJournal of the ACM, 1998
- Specifying and using a partitionable group communication servicePublished by Association for Computing Machinery (ACM) ,1997
- On the Borowsky-Gafni simulation algorithmPublished by Association for Computing Machinery (ACM) ,1996
- Time Bounds for Real-Time Process Control in the Presence of Timing UncertaintyInformation and Computation, 1994
- Authentication and authenticated key exchangesDesigns, Codes and Cryptography, 1992
- New directions in cryptographyIEEE Transactions on Information Theory, 1976