New package for constructing realizers for introduction and elimination
rules of inductive predicates.
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
<P>Cryptographic protocols are of major importance, especially with the
growing use of the Internet. This directory demonstrates a new proof method,
which is described in <A
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
papers</A>. The operational semantics of protocol participants is defined
inductively.
<P>This directory contains proofs concerning
<UL>
<LI>three versions of the Otway-Rees protocol
<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
<LI>two versions of Kerberos: the simplified form published in the BAN paper
and also the full protocol (Kerberos IV)
<LI>three versions of the Yahalom protocol, including a bad one that
illustrates the purpose of the Oops rule
<LI>a novel recursive authentication protocol
<LI>the Internet protocol TLS
</UL>
<HR>
<P>Last modified 20 August 2002
<ADDRESS>
<A
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>