1 (* Title: HOL/Auth/ROOT |
1 (* Title: HOL/Auth/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Root file for protocol proofs. |
6 Root file for protocol proofs. |
7 *) |
7 *) |
8 |
8 |
9 no_document use_thy "NatPair"; |
9 no_document use_thy "NatPair"; |
10 |
10 |
11 set timing; |
11 use_thys [ |
12 |
12 |
13 (* Conventional protocols: rely on |
13 (* Conventional protocols: rely on |
14 conventional Message, Event and Public *) |
14 conventional Message, Event and Public *) |
15 |
15 |
16 (*Shared-key protocols*) |
16 (*Shared-key protocols*) |
17 time_use_thy "NS_Shared"; |
17 "NS_Shared", |
18 time_use_thy "Kerberos_BAN"; |
18 "Kerberos_BAN", |
19 time_use_thy "Kerberos_BAN_Gets"; |
19 "Kerberos_BAN_Gets", |
20 time_use_thy "KerberosIV"; |
20 "KerberosIV", |
21 time_use_thy "KerberosIV_Gets"; |
21 "KerberosIV_Gets", |
22 time_use_thy "KerberosV"; |
22 "KerberosV", |
23 time_use_thy "OtwayRees"; |
23 "OtwayRees", |
24 time_use_thy "OtwayRees_AN"; |
24 "OtwayRees_AN", |
25 time_use_thy "OtwayRees_Bad"; |
25 "OtwayRees_Bad", |
26 time_use_thy "OtwayReesBella"; |
26 "OtwayReesBella", |
27 time_use_thy "WooLam"; |
27 "WooLam", |
28 time_use_thy "Recur"; |
28 "Recur", |
29 time_use_thy "Yahalom"; |
29 "Yahalom", |
30 time_use_thy "Yahalom2"; |
30 "Yahalom2", |
31 time_use_thy "Yahalom_Bad"; |
31 "Yahalom_Bad", |
32 time_use_thy "ZhouGollmann"; |
32 "ZhouGollmann", |
33 |
33 |
34 (*Public-key protocols*) |
34 (*Public-key protocols*) |
35 time_use_thy "NS_Public_Bad"; |
35 "NS_Public_Bad", |
36 time_use_thy "NS_Public"; |
36 "NS_Public", |
37 time_use_thy "TLS"; |
37 "TLS", |
38 time_use_thy "CertifiedEmail"; |
38 "CertifiedEmail", |
39 |
39 |
40 (*Smartcard protocols: rely on conventional Message and on new |
40 (*Smartcard protocols: rely on conventional Message and on new |
41 EventSC and Smartcard *) |
41 EventSC and Smartcard *) |
42 |
42 |
43 with_path "Smartcard" time_use_thy "ShoupRubin"; |
43 "Smartcard/ShoupRubin", |
44 with_path "Smartcard" time_use_thy "ShoupRubinBella"; |
44 "Smartcard/ShoupRubinBella", |
45 |
45 |
46 (*Blanqui's "guard" concept: protocol-independent secrecy*) |
46 (*Blanqui's "guard" concept: protocol-independent secrecy*) |
47 with_path "Guard" (app time_use_thy) |
47 "Guard/P1", |
48 ["P1", "P2", "Guard_NS_Public", "Guard_OtwayRees", "Guard_Yahalom", "Proto"]; |
48 "Guard/P2", |
|
49 "Guard/Guard_NS_Public", |
|
50 "Guard/Guard_OtwayRees", |
|
51 "Guard/Guard_Yahalom", |
|
52 "Guard/Proto" |
|
53 ]; |