author | wenzelm |
Mon, 16 Mar 2009 18:24:30 +0100 | |
changeset 30549 | d2d7874648bd |
parent 28098 | c92850d2d16c |
child 32632 | 8ae912371831 |
permissions | -rw-r--r-- |
24106 | 1 |
(* Title: HOL/Auth/ROOT.ML |
1944 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
1971 | 6 |
Root file for protocol proofs. |
1944 | 7 |
*) |
8 |
||
24106 | 9 |
use_thys [ |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
10 |
|
18886 | 11 |
(* Conventional protocols: rely on |
12 |
conventional Message, Event and Public *) |
|
1944 | 13 |
|
2325 | 14 |
(*Shared-key protocols*) |
24106 | 15 |
"NS_Shared", |
16 |
"Kerberos_BAN", |
|
17 |
"Kerberos_BAN_Gets", |
|
18 |
"KerberosIV", |
|
19 |
"KerberosIV_Gets", |
|
20 |
"KerberosV", |
|
21 |
"OtwayRees", |
|
22 |
"OtwayRees_AN", |
|
23 |
"OtwayRees_Bad", |
|
24 |
"OtwayReesBella", |
|
25 |
"WooLam", |
|
26 |
"Recur", |
|
27 |
"Yahalom", |
|
28 |
"Yahalom2", |
|
29 |
"Yahalom_Bad", |
|
30 |
"ZhouGollmann", |
|
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
31 |
|
2325 | 32 |
(*Public-key protocols*) |
24106 | 33 |
"NS_Public_Bad", |
34 |
"NS_Public", |
|
35 |
"TLS", |
|
36 |
"CertifiedEmail", |
|
13508 | 37 |
|
18886 | 38 |
(*Smartcard protocols: rely on conventional Message and on new |
39 |
EventSC and Smartcard *) |
|
40 |
||
24106 | 41 |
"Smartcard/ShoupRubin", |
42 |
"Smartcard/ShoupRubinBella", |
|
18886 | 43 |
|
13508 | 44 |
(*Blanqui's "guard" concept: protocol-independent secrecy*) |
24106 | 45 |
"Guard/P1", |
46 |
"Guard/P2", |
|
47 |
"Guard/Guard_NS_Public", |
|
48 |
"Guard/Guard_OtwayRees", |
|
49 |
"Guard/Guard_Yahalom", |
|
50 |
"Guard/Proto" |
|
51 |
]; |