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