# Theory README_Guard

theory README_Guard imports Main
begin
section ‹Protocol-Independent Secrecy Results›
text ‹
▪ date: April 2002
▪ author: Frederic Blanqui
▪ email: blanqui@lri.fr
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
🌐‹https://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf›: ∗‹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.thy› contains an important theorem about the decomposition of
analz between pparts (pairs) and kparts (messages that are not pairs).
▪ 🗏‹Guard.thy› contains the protocol-independent secrecy theorem for
nonces.
▪ 🗏‹GuardK.thy› is the same for keys.
▪ 🗏‹Guard_Public.thy› extends 🗏‹Guard.thy› and 🗏‹GuardK.thy› for
public-key protocols.
▪ 🗏‹Guard_Shared.thy› extends 🗏‹Guard.thy› and 🗏‹GuardK.thy› for
symmetric-key protocols.
▪ 🗏‹List_Msg.thy› contains definitions on lists (inside messages).
▪ 🗏‹P1.thy› 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.thy› is the same for the protocol P2
▪ 🗏‹Guard_NS_Public.thy› is for Needham-Schroeder-Lowe
▪ 🗏‹Guard_OtwayRees.thy› is for Otway-Rees
▪ 🗏‹Guard_Yahalom.thy› is for Yahalom
▪ 🗏‹Proto.thy› 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.
›
end