Quelle  README_Guard.thy

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›
  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