| author | nipkow |
| Fri, 06 Nov 2009 19:22:32 +0100 | |
| changeset 33492 | 4168294a9f96 |
| parent 32632 | 8ae912371831 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
| 32632 | 1 |
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| 1944 | 2 |
Copyright 1996 University of Cambridge |
3 |
*) |
|
4 |
||
| 32632 | 5 |
header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
|
| 1944 | 6 |
|
| 32632 | 7 |
theory Auth_Shared |
8 |
imports |
|
9 |
"NS_Shared" |
|
10 |
"Kerberos_BAN" |
|
11 |
"Kerberos_BAN_Gets" |
|
12 |
"KerberosIV" |
|
13 |
"KerberosIV_Gets" |
|
14 |
"KerberosV" |
|
15 |
"OtwayRees" |
|
16 |
"OtwayRees_AN" |
|
17 |
"OtwayRees_Bad" |
|
18 |
"OtwayReesBella" |
|
19 |
"WooLam" |
|
20 |
"Recur" |
|
21 |
"Yahalom" |
|
22 |
"Yahalom2" |
|
23 |
"Yahalom_Bad" |
|
24 |
"ZhouGollmann" |
|
25 |
begin |
|
|
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
26 |
|
| 32632 | 27 |
end |