author | wenzelm |
Wed, 14 Sep 2005 23:14:57 +0200 | |
changeset 17394 | a8c9ed3f9818 |
parent 14716 | 1846cc85ada1 |
child 18886 | 9f27383426db |
permissions | -rw-r--r-- |
1944 | 1 |
(* Title: HOL/Auth/ROOT |
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 |
||
14716 | 9 |
no_document use_thy "NatPair"; |
10 |
||
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
11 |
add_path "Guard"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
12 |
|
13550 | 13 |
set timing; |
1944 | 14 |
|
2325 | 15 |
(*Shared-key protocols*) |
2530 | 16 |
time_use_thy "NS_Shared"; |
5053 | 17 |
time_use_thy "Kerberos_BAN"; |
6452 | 18 |
time_use_thy "KerberosIV"; |
2530 | 19 |
time_use_thy "OtwayRees"; |
20 |
time_use_thy "OtwayRees_AN"; |
|
21 |
time_use_thy "OtwayRees_Bad"; |
|
22 |
time_use_thy "WooLam"; |
|
23 |
time_use_thy "Recur"; |
|
24 |
time_use_thy "Yahalom"; |
|
25 |
time_use_thy "Yahalom2"; |
|
6400 | 26 |
time_use_thy "Yahalom_Bad"; |
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
27 |
time_use_thy "ZhouGollmann"; |
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
28 |
|
2325 | 29 |
(*Public-key protocols*) |
2530 | 30 |
time_use_thy "NS_Public_Bad"; |
31 |
time_use_thy "NS_Public"; |
|
3475 | 32 |
time_use_thy "TLS"; |
13922 | 33 |
time_use_thy "CertifiedEmail"; |
13508 | 34 |
|
35 |
(*Blanqui's "guard" concept: protocol-independent secrecy*) |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
36 |
time_use_thy "P1"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
37 |
time_use_thy "P2"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
38 |
time_use_thy "Guard_NS_Public"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
39 |
time_use_thy "Guard_OtwayRees"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
40 |
time_use_thy "Guard_Yahalom"; |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
14716
diff
changeset
|
41 |
time_use_thy "Proto"; |