1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 2 3<HTML> 4 5<HEAD> 6 <meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> 7 <TITLE>HOL/Auth/README</TITLE> 8</HEAD> 9 10<BODY> 11 12<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1> 13 14<P>Cryptographic protocols are of major importance, especially with the 15growing use of the Internet. This directory demonstrates the ``inductive 16method'' of protocol verification, which is described in <A 17HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various 18papers</A>. The operational semantics of protocol participants is defined 19inductively. 20 21<P>This directory contains proofs concerning 22 23<UL> 24<LI>three versions of the Otway-Rees protocol 25 26<LI>the Needham-Schroeder shared-key protocol 27 28<LI>the Needham-Schroeder public-key protocol (original and with Lowe's 29modification) 30 31<LI>two versions of Kerberos: the simplified form published in the BAN paper 32 and also the full protocol (Kerberos IV) 33 34<LI>three versions of the Yahalom protocol, including a bad one that 35 illustrates the purpose of the Oops rule 36 37<LI>a novel recursive authentication protocol 38 39<LI>the Internet protocol TLS 40 41<LI>The certified e-mail protocol of Abadi et al. 42</UL> 43 44<P>Frederic Blanqui has contributed a theory of guardedness, which is 45demonstrated by proofs of some roving agent protocols. 46 47<ADDRESS> 48<A 49HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>, 50<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> 51</ADDRESS> 52</BODY> 53</HTML> 54