<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML>
<HEAD>
<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
<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 the ``inductive
method'' of protocol verification, 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 shared-key protocol
<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
modification)
<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
<LI>The certified e-mail protocol of Abadi et al.
</UL>
<P>Frederic Blanqui has contributed a theory of guardedness, which is
demonstrated by proofs of some roving agent protocols.
<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>