I/O Automaton Models and Proofs for Shared-Key Communication Systems
| Author(s) : | Nancy Lynch, |
| Publisher : | N/A |
| Publication Date : | 1999 |
| ISSN : | N/A |
| Abstract : | The combination of two security protocols, a simple shared-key communication protocol and the Di e-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. 0 1, |