Theory README_Guard

theory README_Guard imports Main

section ‹Protocol-Independent Secrecy Results›

text  date: April 2002
   author: Frederic Blanqui

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

     🗏‹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.