Proving security protocols correct
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 370-381
- https://doi.org/10.1109/lics.1999.782632
Abstract
Security protocols use cryptography to set up private communication channels on an insecure network. Many protocols contain flaws, and because security goals are seldom specified in detail, we cannot be certain what constitutes a flaw. Thanks to recent work by a number of researchers, security protocols can now be analyzed formally. The paper outlines the problem area, emphasizing the notion of freshness. It describes how a protocol can be specified using operational semantics and properties proved by rule induction, with machine support from the proof tool Isabelle. The main example compares two versions of the Yahalom protocol. Unless the model of the environment is sufficiently detailed, it cannot distinguish the correct protocol from a flawed version. The paper attempts to draw some general lessons on the use of formalisms. Compared with model checking, the inductive method performs a finer analysis, but the cost of using it is greater.Keywords
This publication has 14 references indexed in Scilit:
- Logic and over-simplificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Proving security protocols with model checkers by data independence techniquesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a completeness result for model checking of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Casper: a compiler for the analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Automated analysis of cryptographic protocols using MurφPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An attack on a recursive authentication protocol A cautionary taleInformation Processing Letters, 1998
- Kerberos Version IV: Inductive analysis of the secrecy goalsPublished by Springer Nature ,1998
- Security properties and CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1996
- Prudent engineering practice for cryptographic protocolsIEEE Transactions on Software Engineering, 1996
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989