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 add_path "Guard"; |
11 set timing; |
12 |
12 |
13 set timing; |
13 (* Conventional protocols: rely on |
|
14 conventional Message, Event and Public *) |
14 |
15 |
15 (*Shared-key protocols*) |
16 (*Shared-key protocols*) |
16 time_use_thy "NS_Shared"; |
17 time_use_thy "NS_Shared"; |
17 time_use_thy "Kerberos_BAN"; |
18 time_use_thy "Kerberos_BAN"; |
|
19 time_use_thy "Kerberos_BAN_Gets"; |
18 time_use_thy "KerberosIV"; |
20 time_use_thy "KerberosIV"; |
|
21 time_use_thy "KerberosIV_Gets"; |
|
22 time_use_thy "KerberosV"; |
19 time_use_thy "OtwayRees"; |
23 time_use_thy "OtwayRees"; |
20 time_use_thy "OtwayRees_AN"; |
24 time_use_thy "OtwayRees_AN"; |
21 time_use_thy "OtwayRees_Bad"; |
25 time_use_thy "OtwayRees_Bad"; |
|
26 time_use_thy "OtwayReesBella"; |
22 time_use_thy "WooLam"; |
27 time_use_thy "WooLam"; |
23 time_use_thy "Recur"; |
28 time_use_thy "Recur"; |
24 time_use_thy "Yahalom"; |
29 time_use_thy "Yahalom"; |
25 time_use_thy "Yahalom2"; |
30 time_use_thy "Yahalom2"; |
26 time_use_thy "Yahalom_Bad"; |
31 time_use_thy "Yahalom_Bad"; |
30 time_use_thy "NS_Public_Bad"; |
35 time_use_thy "NS_Public_Bad"; |
31 time_use_thy "NS_Public"; |
36 time_use_thy "NS_Public"; |
32 time_use_thy "TLS"; |
37 time_use_thy "TLS"; |
33 time_use_thy "CertifiedEmail"; |
38 time_use_thy "CertifiedEmail"; |
34 |
39 |
|
40 (*Smartcard protocols: rely on conventional Message and on new |
|
41 EventSC and Smartcard *) |
|
42 |
|
43 with_path "Smartcard" time_use_thy "ShoupRubin"; |
|
44 with_path "Smartcard" time_use_thy "ShoupRubinBella"; |
|
45 |
35 (*Blanqui's "guard" concept: protocol-independent secrecy*) |
46 (*Blanqui's "guard" concept: protocol-independent secrecy*) |
36 time_use_thy "P1"; |
47 with_path "Guard" (app time_use_thy) |
37 time_use_thy "P2"; |
48 ["P1", "P2", "Guard_NS_Public", "Guard_OtwayRees", "Guard_Yahalom", "Proto"]; |
38 time_use_thy "Guard_NS_Public"; |
|
39 time_use_thy "Guard_OtwayRees"; |
|
40 time_use_thy "Guard_Yahalom"; |
|
41 time_use_thy "Proto"; |
|