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