Quelle  README_Guard.thy   Sprache: Isabelle

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