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

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet am 2026-06-10) ¤

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 und die Messung sind noch experimentell.