Protocol-Independent Secrecy Results
date: april 2002
author: Frederic Blanqui
email: blanqui@lri.fr
webpage:
The current development is built above the HOL (Higher-Order Logic)
Isabelle theory and the formalization of protocols introduced by Larry Paulson. More details are
in his paper
The Inductive approach
to verifying cryptographic protocols (J. Computer Security 6, pages
85-128, 1998).
This directory contains a number of files:
- Extensions.thy contains extensions of Larry Paulson's files with many useful
lemmas.
- Analz contains an important theorem about the decomposition of analz
between pparts (pairs) and kparts (messages that are not pairs).
- Guard contains the protocol-independent secrecy theorem for nonces.
- GuardK is the same for keys.
- Guard_Public extends Guard and GuardK for public-key protocols.
- Guard_Shared extends Guard and GuardK for symmetric-key protocols.
- List_Msg contains definitions on lists (inside messages).
- P1 contains the definition of the protocol P1 and the proof of its
properties (strong forward integrity, insertion resilience, truncation
resilience, data confidentiality and non-repudiability)
- P2 is the same for the protocol P2
- NS_Public is for Needham-Schroeder-Lowe
- OtwayRees is for Otway-Rees
- Yahalom is for Yahalom
- Proto contains a more precise formalization of protocols with rules
and a protocol-independent theorem for proving guardness from a preservation
property. It also contains the proofs for Needham-Schroeder as an example.
Last modified 20 August 2002
Frederic Blanqui,
blanqui@lri.fr