author  paulson 
Thu, 18 Mar 1999 10:41:33 +0100  
changeset 6400  1f495d4d922b 
parent 4594  f8d4387b40d9 
child 6452  6a1b393ccdc0 
permissions  rwrr 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

1 
<! $Id$ > 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

2 
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

3 

bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

4 
<H2>AuthThe Inductive Approach to Verifying Security Protocols</H2> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

5 

bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

6 
<P>Cryptographic protocols are of major importance, especially with the 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

7 
growing use of the Internet. This directory demonstrates a <A 
4594  8 
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

9 
proof method</A>. The operational semantics of protocol participants is 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

10 
defined inductively. The directory contains proofs concerning 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

11 

bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

12 
<UL> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

13 
<LI>three versions of the OtwayRees protocol 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

14 

4594  15 
<LI>the NeedhamSchroeder protocol (publickey and sharedkey versions) 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

16 

6400  17 
<LI>the Kerberos protocol (the simplified form published in the BAN paper) 
18 

19 
<LI>three versions of the Yahalom protocol, including a bad one that 

20 
illustrates the purpose of the Oops rule 

3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

21 

4594  22 
<LI>a novel recursive authentication protocol 
23 

24 
<LI>the Internet protocol TLS 

3119
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 

bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

27 
<HR> 
4594  28 
<P>Last modified 30 Jan 1998 
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

29 

bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

30 
<ADDRESS> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

31 
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

32 
</ADDRESS> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

33 
</BODY></HTML> 