Quelle README.thy

Sprache: Isabelle

theory README imports Main
begin

section ‹Auth--The Inductive Approach to Verifying Security Protocols›

text ‹
Cryptographic protocols are of major importance, especially with the growing
use of the Internet. This directory demonstrates the ``inductive method'' of
protocol verification, which is described in papers:
🪙‹http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html›. The operational
semantics of protocol participants is defined inductively.

This directory contains proofs concerning:

▪ three versions of the Otway-Rees protocol

▪ the Needham-Schroeder shared-key protocol

▪ the Needham-Schroeder public-key protocol (original and with Lowe's
modification)

▪ two versions of Kerberos: the simplified form published in the BAN paper
and also the full protocol (Kerberos IV)

▪ three versions of the Yahalom protocol, including a bad one that
illustrates the purpose of the Oops rule

▪ a novel recursive authentication protocol

▪ the Internet protocol TLS

▪ The certified e-mail protocol of Abadi et al.

Frederic Blanqui has contributed a theory of guardedness, which is
demonstrated by proofs of some roving agent protocols.
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 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.