author | paulson |
Tue, 08 Sep 1998 15:17:11 +0200 | |
changeset 5434 | 9b4bed3f394c |
parent 5053 | 75d20f367e94 |
child 11185 | 1b737b4c2108 |
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*) |
|
33 |
SesKeyLife_LB "2 <= SesKeyLife" |
|
34 |
||
35 |
(*The authenticator only for one journey*) |
|
36 |
AutLife_LB "1 <= AutLife" |
|
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 |
||
49 |
Nil "[]: kerberos_ban" |
|
50 |
||
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
51 |
Fake "[| evs: kerberos_ban; X: synth (analz (spies evs)) |] |
5053 | 52 |
==> Says Spy B X # evs : kerberos_ban" |
53 |
||
54 |
||
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
55 |
Kb1 "[| evs1: kerberos_ban |] |
5053 | 56 |
==> Says A Server {|Agent A, Agent B|} # evs1 |
57 |
: kerberos_ban" |
|
58 |
||
59 |
||
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
60 |
Kb2 "[| evs2: kerberos_ban; Key KAB ~: used evs2; |
5053 | 61 |
Says A' Server {|Agent A, Agent B|} : set evs2 |] |
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|})|}) |
|
66 |
# evs2 : kerberos_ban" |
|
67 |
||
68 |
||
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
69 |
Kb3 "[| evs3: kerberos_ban; |
5053 | 70 |
Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
71 |
: set evs3; |
|
72 |
Says A Server {|Agent A, Agent B|} : set evs3; |
|
73 |
~ Expired Ts evs3 |] |
|
74 |
==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} |
|
75 |
# evs3 : kerberos_ban" |
|
76 |
||
77 |
||
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
78 |
Kb4 "[| evs4: 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 |
83 |
: kerberos_ban" |
|
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*) |
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
86 |
Oops "[| evso: kerberos_ban; |
5053 | 87 |
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
88 |
: set evso; |
|
89 |
Expired Ts evso |] |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5053
diff
changeset
|
90 |
==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban" |
5053 | 91 |
|
92 |
||
93 |
end |