Quelle README_Guard.thy Sprache: Isabelle

theory README_Guard imports Main
begin

section \<open>Protocol-Independent Secrecy Results\<close>

text \<open>
  \<^item> date: April 2002
  \<^item> author: Frederic Blanqui
  \<^item> 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
  \<^url>\<open>https://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf\<close>: \<^emph>\<open>The Inductive
  approach to verifying cryptographic protocols\<close> (J. Computer Security 6,
  pages 85-128, 1998).

  This directory contains a number of files:

    \<^item> \<^file>\<open>Extensions.thy\<close> contains extensions of Larry Paulson's files with
      many useful lemmas.

    \<^item> \<^file>\<open>Analz.thy\<close> contains an important theorem about the decomposition of
    analz between pparts (pairs) and kparts (messages that are not pairs).

    \<^item> \<^file>\<open>Guard.thy\<close> contains the protocol-independent secrecy theorem for
      nonces.

    \<^item> \<^file>\<open>GuardK.thy\<close> is the same for keys.

    \<^item> \<^file>\<open>Guard_Public.thy\<close> extends \<^file>\<open>Guard.thy\<close> and \<^file>\<open>GuardK.thy\<close> for
    public-key protocols.

    \<^item> \<^file>\<open>Guard_Shared.thy\<close> extends \<^file>\<open>Guard.thy\<close> and \<^file>\<open>GuardK.thy\<close> for
    symmetric-key protocols.

    \<^item> \<^file>\<open>List_Msg.thy\<close> contains definitions on lists (inside messages).

    \<^item> \<^file>\<open>P1.thy\<close> 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).

    \<^item> \<^file>\<open>P2.thy\<close> is the same for the protocol P2

    \<^item> \<^file>\<open>Guard_NS_Public.thy\<close> is for Needham-Schroeder-Lowe

    \<^item> \<^file>\<open>Guard_OtwayRees.thy\<close> is for Otway-Rees

    \<^item> \<^file>\<open>Guard_Yahalom.thy\<close> is for Yahalom

    \<^item> \<^file>\<open>Proto.thy\<close> 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.
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.