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
