author | paulson |
Mon, 06 Aug 2001 15:46:20 +0200 | |
changeset 11465 | 45d156ede468 |
parent 11185 | 1b737b4c2108 |
child 11701 | 3d51fbf81c17 |
permissions | -rw-r--r-- |
5053 | 1 |
(* Title: HOL/Auth/Kerberos_BAN |
2 |
ID: $Id$ |
|
3 |
Author: Giampaolo Bella, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
The Kerberos protocol, BAN version. |
|
7 |
||
8 |
From page 251 of |
|
9 |
Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 |
Proc. Royal Soc. 426 (1989) |
|
11 |
*) |
|
12 |
||
13 |
Kerberos_BAN = Shared + |
|
14 |
||
15 |
(* Temporal modelization: session keys can be leaked |
|
16 |
ONLY when they have expired *) |
|
17 |
||
18 |
syntax |
|
19 |
CT :: event list=>nat |
|
20 |
Expired :: [nat, event list] => bool |
|
21 |
RecentAuth :: [nat, event list] => bool |
|
22 |
||
23 |
consts |
|
24 |
||
25 |
(*Duration of the session key*) |
|
26 |
SesKeyLife :: nat |
|
27 |
||
28 |
(*Duration of the authenticator*) |
|
29 |
AutLife :: nat |
|
30 |
||
31 |
rules |
|
32 |
(*The ticket should remain fresh for two journeys on the network at least*) |
|
11465 | 33 |
SesKeyLife_LB "#2 <= SesKeyLife" |
5053 | 34 |
|
35 |
(*The authenticator only for one journey*) |
|
11465 | 36 |
AutLife_LB "1' <= AutLife" |
5053 | 37 |
|
38 |
translations |
|
39 |
"CT" == "length" |
|
40 |
||
41 |
"Expired T evs" == "SesKeyLife + T < CT evs" |
|
42 |
||
43 |
"RecentAuth T evs" == "CT evs <= AutLife + T" |
|
44 |
||
45 |
consts kerberos_ban :: event list set |
|
46 |
inductive "kerberos_ban" |
|
47 |
intrs |
|
48 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
49 |
Nil "[] \\<in> kerberos_ban" |
5053 | 50 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
51 |
Fake "[| evsf \\<in> kerberos_ban; X \\<in> synth (analz (spies evsf)) |] |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
52 |
==> Says Spy B X # evsf \\<in> kerberos_ban" |
5053 | 53 |
|
54 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
55 |
Kb1 "[| evs1 \\<in> kerberos_ban |] |
5053 | 56 |
==> Says A Server {|Agent A, Agent B|} # evs1 |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
57 |
\\<in> kerberos_ban" |
5053 | 58 |
|
59 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
60 |
Kb2 "[| evs2 \\<in> kerberos_ban; Key KAB \\<notin> used evs2; |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
61 |
Says A' Server {|Agent A, Agent B|} \\<in> set evs2 |] |
5053 | 62 |
==> Says Server A |
63 |
(Crypt (shrK A) |
|
64 |
{|Number (CT evs2), Agent B, Key KAB, |
|
65 |
(Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
66 |
# evs2 \\<in> kerberos_ban" |
5053 | 67 |
|
68 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
69 |
Kb3 "[| evs3 \\<in> kerberos_ban; |
5053 | 70 |
Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
71 |
\\<in> set evs3; |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
72 |
Says A Server {|Agent A, Agent B|} \\<in> set evs3; |
5053 | 73 |
~ Expired Ts evs3 |] |
74 |
==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
75 |
# evs3 \\<in> kerberos_ban" |
5053 | 76 |
|
77 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
78 |
Kb4 "[| evs4 \\<in> kerberos_ban; |
5053 | 79 |
Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), |
80 |
(Crypt K {|Agent A, Number Ta|}) |}: set evs4; |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
81 |
~ Expired Ts evs4; RecentAuth Ta evs4 |] |
5053 | 82 |
==> Says B A (Crypt K (Number Ta)) # evs4 |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
83 |
\\<in> kerberos_ban" |
5053 | 84 |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
85 |
(*Old session keys may become compromised*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
86 |
Oops "[| evso \\<in> kerberos_ban; |
5053 | 87 |
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
88 |
\\<in> set evso; |
5053 | 89 |
Expired Ts evso |] |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
5434
diff
changeset
|
90 |
==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban" |
5053 | 91 |
|
92 |
||
93 |
end |