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