| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Auth/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle README.thySprache: 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
¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26