Proving properties of security protocols by induction
- 22 November 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Informal justifications of security protocols involve arguing backwards that various events are impossible. Inductive definitions can make such arguments rigorous. The resulting proofs are complicated, but can be generated reasonably quickly using the proof tool Isabelle/HOL. There is no restriction to finite-state systems and the approach is not based on belief logics. Protocols are inductively defined as sets of traces, which may involve many interleaved protocol runs. Protocol descriptions model accidental key losses as well as attacks. The model spy can send spoof messages made up of components decrypted from previous traffic.Several key distribution protocols have been studied, including Needham-Schroeder, Yahalom and Otway-Rees. The method applies to both symmetric-key and public-key protocols. A new attack has been discovered in a variant of Otway-Rees (already broken by Mao and Boyd). Assertions concerning secrecy and authenticity have been proved.Keywords
This publication has 10 references indexed in Scilit:
- Towards formal analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Some new attacks upon security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A HOL extension of GNY for automatically analyzing cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- What do we mean by entity authentication?Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Prudent engineering practice for cryptographic protocolsIEEE Transactions on Software Engineering, 1996
- On the security of recent protocolsInformation Processing Letters, 1995
- Why cryptosystems failCommunications of the ACM, 1994
- Three systems for cryptographic protocol analysisJournal of Cryptology, 1994
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989
- An Introduction to Inductive DefinitionsPublished by Elsevier ,1977