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
