src/HOL/Auth/README.html
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 6452 6a1b393ccdc0
child 13508 890d736b93a5
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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>Auth--The 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
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
     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 Otway-Rees protocol
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    14
4594
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    15
<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    16
6452
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents: 6400
diff changeset
    17
<LI>two versions of Kerberos: the simplified form published in the BAN paper
6a1b393ccdc0 addition of Kerberos IV example
paulson
parents: 6400
diff changeset
    18
	and also the full protocol (Kerberos IV)
6400
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    19
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    20
<LI>three versions of the Yahalom protocol, including a bad one that 
1f495d4d922b added new theory Yahalom_Bad
paulson
parents: 4594
diff changeset
    21
	illustrates the purpose of the Oops rule
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    22
4594
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    23
<LI>a novel recursive authentication protocol 
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    24
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    25
<LI>the Internet protocol TLS
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    26
</UL>
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    27
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    28
<HR>
4594
f8d4387b40d9 fixed WWW links
paulson
parents: 3119
diff changeset
    29
<P>Last modified 30 Jan 1998
3119
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    30
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    31
<ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    32
<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
    33
</ADDRESS>
bb2ee88aa43f Description of the Auth directory: security protocols proofs
paulson
parents:
diff changeset
    34
</BODY></HTML>