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 |
|
15 growing use of the Internet. This directory demonstrates the ``inductive |
|
16 method'' of protocol verification, which is described in <A |
|
17 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various |
|
18 papers</A>. The operational semantics of protocol participants is defined |
|
19 inductively. |
|
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 |
|
29 modification) |
|
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 |
|
45 demonstrated by proofs of some roving agent protocols. |
|
46 |
|
47 <ADDRESS> |
|
48 <A |
|
49 HREF="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> |
|