author | wenzelm |
Mon, 16 Mar 2009 18:24:30 +0100 | |
changeset 30549 | d2d7874648bd |
parent 25134 | 3d4953e88449 |
child 32406 | 9ea59bd1397a |
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 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
header{*The Kerberos Protocol, BAN Version*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
8 |
|
16417 | 9 |
theory Kerberos_BAN imports Public begin |
5053 | 10 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
text{*From page 251 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
Proc. Royal Soc. 426 |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
14 |
|
18886 | 15 |
Confidentiality (secrecy) and authentication properties are also |
16 |
given in a termporal version: strong guarantees in a little abstracted |
|
17 |
- but very realistic - model. |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
18 |
*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
19 |
|
18886 | 20 |
(* Temporal model of accidents: session keys can be leaked |
21 |
ONLY when they have expired *) |
|
5053 | 22 |
|
23 |
consts |
|
24 |
||
25 |
(*Duration of the session key*) |
|
18886 | 26 |
sesKlife :: nat |
5053 | 27 |
|
28 |
(*Duration of the authenticator*) |
|
18886 | 29 |
authlife :: nat |
5053 | 30 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
31 |
text{*The ticket should remain fresh for two journeys on the network at least*} |
18886 | 32 |
specification (sesKlife) |
33 |
sesKlife_LB [iff]: "2 \<le> sesKlife" |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
34 |
by blast |
5053 | 35 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
36 |
text{*The authenticator only for one journey*} |
18886 | 37 |
specification (authlife) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
38 |
authlife_LB [iff]: "authlife \<noteq> 0" |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
39 |
by blast |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
40 |
|
20768 | 41 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
42 |
CT :: "event list=>nat" where |
20768 | 43 |
"CT == length " |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
44 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
45 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
46 |
expiredK :: "[nat, event list] => bool" where |
20768 | 47 |
"expiredK T evs == sesKlife + T < CT evs" |
18886 | 48 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
49 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
50 |
expiredA :: "[nat, event list] => bool" where |
20768 | 51 |
"expiredA T evs == authlife + T < CT evs" |
18886 | 52 |
|
53 |
||
54 |
constdefs |
|
5053 | 55 |
|
18886 | 56 |
(* A is the true creator of X if she has sent X and X never appeared on |
57 |
the trace before this event. Recall that traces grow from head. *) |
|
58 |
Issues :: "[agent, agent, msg, event list] => bool" |
|
59 |
("_ Issues _ with _ on _") |
|
60 |
"A Issues B with X on evs == |
|
61 |
\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} & |
|
62 |
X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs)))" |
|
5053 | 63 |
|
18886 | 64 |
(* Yields the subtrace of a given trace from its beginning to a given event *) |
65 |
before :: "[event, event list] => event list" ("before _ on _") |
|
66 |
"before ev on evs == takeWhile (% z. z ~= ev) (rev evs)" |
|
67 |
||
68 |
(* States than an event really appears only once on a trace *) |
|
69 |
Unique :: "[event, event list] => bool" ("Unique _ on _") |
|
70 |
"Unique ev on evs == |
|
71 |
ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))" |
|
72 |
||
73 |
||
23746 | 74 |
inductive_set bankerberos :: "event list set" |
75 |
where |
|
13926 | 76 |
|
18886 | 77 |
Nil: "[] \<in> bankerberos" |
13926 | 78 |
|
23746 | 79 |
| Fake: "\<lbrakk> evsf \<in> bankerberos; X \<in> synth (analz (spies evsf)) \<rbrakk> |
18886 | 80 |
\<Longrightarrow> Says Spy B X # evsf \<in> bankerberos" |
13926 | 81 |
|
82 |
||
23746 | 83 |
| BK1: "\<lbrakk> evs1 \<in> bankerberos \<rbrakk> |
18886 | 84 |
\<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 |
85 |
\<in> bankerberos" |
|
86 |
||
87 |
||
23746 | 88 |
| BK2: "\<lbrakk> evs2 \<in> bankerberos; Key K \<notin> used evs2; K \<in> symKeys; |
18886 | 89 |
Says A' Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
90 |
\<Longrightarrow> Says Server A |
|
13926 | 91 |
(Crypt (shrK A) |
18886 | 92 |
\<lbrace>Number (CT evs2), Agent B, Key K, |
93 |
(Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) |
|
94 |
# evs2 \<in> bankerberos" |
|
13926 | 95 |
|
96 |
||
23746 | 97 |
| BK3: "\<lbrakk> evs3 \<in> bankerberos; |
18886 | 98 |
Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
13926 | 99 |
\<in> set evs3; |
18886 | 100 |
Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
101 |
\<not> expiredK Tk evs3 \<rbrakk> |
|
102 |
\<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> |
|
103 |
# evs3 \<in> bankerberos" |
|
13926 | 104 |
|
105 |
||
23746 | 106 |
| BK4: "\<lbrakk> evs4 \<in> bankerberos; |
18886 | 107 |
Says A' B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), |
108 |
(Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4; |
|
109 |
\<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> |
|
110 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 |
|
111 |
\<in> bankerberos" |
|
5053 | 112 |
|
13926 | 113 |
(*Old session keys may become compromised*) |
23746 | 114 |
| Oops: "\<lbrakk> evso \<in> bankerberos; |
18886 | 115 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
13926 | 116 |
\<in> set evso; |
18886 | 117 |
expiredK Tk evso \<rbrakk> |
118 |
\<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerberos" |
|
13926 | 119 |
|
120 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
121 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
122 |
declare parts.Body [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
123 |
declare analz_into_parts [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
124 |
declare Fake_parts_insert_in_Un [dest] |
13926 | 125 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
126 |
text{*A "possibility property": there are traces that reach the end.*} |
18886 | 127 |
lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk> |
128 |
\<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerberos. |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
129 |
Says B A (Crypt K (Number Timestamp)) |
13926 | 130 |
\<in> set evs" |
18886 | 131 |
apply (cut_tac sesKlife_LB) |
13926 | 132 |
apply (intro exI bexI) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
133 |
apply (rule_tac [2] |
18886 | 134 |
bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2, |
135 |
THEN bankerberos.BK3, THEN bankerberos.BK4]) |
|
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
136 |
apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
13926 | 137 |
done |
138 |
||
18886 | 139 |
subsection{*Lemmas for reasoning about predicate "Issues"*} |
13926 | 140 |
|
18886 | 141 |
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
142 |
apply (induct_tac "evs") |
|
143 |
apply (induct_tac [2] "a", auto) |
|
144 |
done |
|
145 |
||
146 |
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
|
147 |
apply (induct_tac "evs") |
|
148 |
apply (induct_tac [2] "a", auto) |
|
149 |
done |
|
150 |
||
151 |
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
|
152 |
(if A:bad then insert X (spies evs) else spies evs)" |
|
153 |
apply (induct_tac "evs") |
|
154 |
apply (induct_tac [2] "a", auto) |
|
155 |
done |
|
156 |
||
157 |
lemma spies_evs_rev: "spies evs = spies (rev evs)" |
|
158 |
apply (induct_tac "evs") |
|
159 |
apply (induct_tac [2] "a") |
|
160 |
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
|
161 |
done |
|
162 |
||
163 |
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
|
164 |
||
165 |
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
|
166 |
apply (induct_tac "evs") |
|
167 |
apply (induct_tac [2] "a", auto) |
|
168 |
txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
|
169 |
done |
|
170 |
||
171 |
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
|
172 |
||
173 |
||
174 |
text{*Lemmas for reasoning about predicate "before"*} |
|
175 |
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"; |
|
176 |
apply (induct_tac "evs") |
|
177 |
apply simp |
|
178 |
apply (induct_tac "a") |
|
179 |
apply auto |
|
180 |
done |
|
13926 | 181 |
|
18886 | 182 |
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"; |
183 |
apply (induct_tac "evs") |
|
184 |
apply simp |
|
185 |
apply (induct_tac "a") |
|
186 |
apply auto |
|
187 |
done |
|
188 |
||
189 |
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"; |
|
190 |
apply (induct_tac "evs") |
|
191 |
apply simp |
|
192 |
apply (induct_tac "a") |
|
193 |
apply auto |
|
194 |
done |
|
195 |
||
196 |
lemma used_evs_rev: "used evs = used (rev evs)" |
|
197 |
apply (induct_tac "evs") |
|
198 |
apply simp |
|
199 |
apply (induct_tac "a") |
|
200 |
apply (simp add: used_Says_rev) |
|
201 |
apply (simp add: used_Gets_rev) |
|
202 |
apply (simp add: used_Notes_rev) |
|
203 |
done |
|
204 |
||
205 |
lemma used_takeWhile_used [rule_format]: |
|
206 |
"x : used (takeWhile P X) --> x : used X" |
|
207 |
apply (induct_tac "X") |
|
208 |
apply simp |
|
209 |
apply (induct_tac "a") |
|
210 |
apply (simp_all add: used_Nil) |
|
211 |
apply (blast dest!: initState_into_used)+ |
|
212 |
done |
|
213 |
||
214 |
lemma set_evs_rev: "set evs = set (rev evs)" |
|
215 |
apply auto |
|
216 |
done |
|
217 |
||
218 |
lemma takeWhile_void [rule_format]: |
|
219 |
"x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs" |
|
220 |
apply auto |
|
221 |
done |
|
222 |
||
223 |
(**** Inductive proofs about bankerberos ****) |
|
224 |
||
225 |
text{*Forwarding Lemma for reasoning about the encrypted portion of message BK3*} |
|
226 |
lemma BK3_msg_in_parts_spies: |
|
227 |
"Says S A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs |
|
228 |
\<Longrightarrow> X \<in> parts (spies evs)" |
|
229 |
apply blast |
|
230 |
done |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
231 |
|
13926 | 232 |
lemma Oops_parts_spies: |
18886 | 233 |
"Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs |
234 |
\<Longrightarrow> K \<in> parts (spies evs)" |
|
235 |
apply blast |
|
236 |
done |
|
13926 | 237 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
238 |
text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
13926 | 239 |
lemma Spy_see_shrK [simp]: |
18886 | 240 |
"evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
241 |
apply (erule bankerberos.induct) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
242 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 243 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast+) |
13926 | 244 |
done |
5053 | 245 |
|
246 |
||
13926 | 247 |
lemma Spy_analz_shrK [simp]: |
18886 | 248 |
"evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
249 |
apply auto |
|
250 |
done |
|
13926 | 251 |
|
252 |
lemma Spy_see_shrK_D [dest!]: |
|
18886 | 253 |
"\<lbrakk> Key (shrK A) \<in> parts (spies evs); |
254 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A:bad" |
|
255 |
apply (blast dest: Spy_see_shrK) |
|
256 |
done |
|
13926 | 257 |
|
258 |
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
|
259 |
||
260 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
261 |
text{*Nobody can have used non-existent keys!*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
262 |
lemma new_keys_not_used [simp]: |
18886 | 263 |
"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerberos\<rbrakk> |
264 |
\<Longrightarrow> K \<notin> keysFor (parts (spies evs))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
265 |
apply (erule rev_mp) |
18886 | 266 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
267 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 268 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
269 |
txt{*Fake*} |
13926 | 270 |
apply (force dest!: keysFor_parts_insert) |
18886 | 271 |
txt{*BK2, BK3, BK4*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
272 |
apply (force dest!: analz_shrK_Decrypt)+ |
13926 | 273 |
done |
274 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
275 |
subsection{* Lemmas concerning the form of items passed in messages *} |
13926 | 276 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
277 |
text{*Describes the form of K, X and K' when the Server sends this message.*} |
13926 | 278 |
lemma Says_Server_message_form: |
18886 | 279 |
"\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
280 |
\<in> set evs; evs \<in> bankerberos \<rbrakk> |
|
281 |
\<Longrightarrow> K' = shrK A & K \<notin> range shrK & |
|
282 |
Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) & |
|
283 |
Key K \<notin> used(before |
|
284 |
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
285 |
on evs) & |
|
286 |
Tk = CT(before |
|
287 |
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
288 |
on evs)" |
|
289 |
apply (unfold before_def) |
|
13926 | 290 |
apply (erule rev_mp) |
18886 | 291 |
apply (erule bankerberos.induct, simp_all) |
292 |
txt{*We need this simplification only for Message 2*} |
|
293 |
apply (simp (no_asm) add: takeWhile_tail) |
|
294 |
apply auto |
|
295 |
txt{*Two subcases of Message 2. Subcase: used before*} |
|
296 |
apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD] |
|
297 |
used_takeWhile_used) |
|
298 |
txt{*subcase: CT before*} |
|
299 |
apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void]) |
|
13926 | 300 |
done |
5053 | 301 |
|
302 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
303 |
text{*If the encrypted message appears then it originated with the Server |
13926 | 304 |
PROVIDED that A is NOT compromised! |
18886 | 305 |
This allows A to verify freshness of the session key. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
306 |
*} |
18886 | 307 |
lemma Kab_authentic: |
308 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
309 |
\<in> parts (spies evs); |
18886 | 310 |
A \<notin> bad; evs \<in> bankerberos \<rbrakk> |
311 |
\<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
13926 | 312 |
\<in> set evs" |
313 |
apply (erule rev_mp) |
|
18886 | 314 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
315 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 316 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast) |
13926 | 317 |
done |
318 |
||
319 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
320 |
text{*If the TICKET appears then it originated with the Server*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
321 |
text{*FRESHNESS OF THE SESSION KEY to B*} |
18886 | 322 |
lemma ticket_authentic: |
323 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
324 |
B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
325 |
\<Longrightarrow> Says Server A |
|
326 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
327 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
13926 | 328 |
\<in> set evs" |
329 |
apply (erule rev_mp) |
|
18886 | 330 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
331 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 332 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast) |
13926 | 333 |
done |
334 |
||
335 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
336 |
text{*EITHER describes the form of X when the following message is sent, |
13926 | 337 |
OR reduces it to the Fake case. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
338 |
Use @{text Says_Server_message_form} if applicable.*} |
13926 | 339 |
lemma Says_S_message_form: |
18886 | 340 |
"\<lbrakk> Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
341 |
\<in> set evs; |
18886 | 342 |
evs \<in> bankerberos \<rbrakk> |
343 |
\<Longrightarrow> (K \<notin> range shrK & X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>)) |
|
13926 | 344 |
| X \<in> analz (spies evs)" |
345 |
apply (case_tac "A \<in> bad") |
|
346 |
apply (force dest!: Says_imp_spies [THEN analz.Inj]) |
|
347 |
apply (frule Says_imp_spies [THEN parts.Inj]) |
|
18886 | 348 |
apply (blast dest!: Kab_authentic Says_Server_message_form) |
13926 | 349 |
done |
350 |
||
5053 | 351 |
|
352 |
||
13926 | 353 |
(**** |
354 |
The following is to prove theorems of the form |
|
355 |
||
18886 | 356 |
Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow> |
13926 | 357 |
Key K \<in> analz (spies evs) |
358 |
||
359 |
A more general formula must be proved inductively. |
|
360 |
||
361 |
****) |
|
362 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
363 |
text{* Session keys are not used to encrypt other session keys *} |
13926 | 364 |
lemma analz_image_freshK [rule_format (no_asm)]: |
18886 | 365 |
"evs \<in> bankerberos \<Longrightarrow> |
366 |
\<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
367 |
(Key K \<in> analz (Key`KK Un (spies evs))) = |
13926 | 368 |
(K \<in> KK | Key K \<in> analz (spies evs))" |
18886 | 369 |
apply (erule bankerberos.induct) |
13926 | 370 |
apply (drule_tac [7] Says_Server_message_form) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
371 |
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) |
13926 | 372 |
done |
373 |
||
374 |
||
375 |
lemma analz_insert_freshK: |
|
18886 | 376 |
"\<lbrakk> evs \<in> bankerberos; KAB \<notin> range shrK \<rbrakk> \<Longrightarrow> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
377 |
(Key K \<in> analz (insert (Key KAB) (spies evs))) = |
13926 | 378 |
(K = KAB | Key K \<in> analz (spies evs))" |
18886 | 379 |
apply (simp only: analz_image_freshK analz_image_freshK_simps) |
380 |
done |
|
13926 | 381 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
382 |
text{* The session key K uniquely identifies the message *} |
13926 | 383 |
lemma unique_session_keys: |
18886 | 384 |
"\<lbrakk> Says Server A |
385 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
386 |
Says Server A' |
18886 | 387 |
(Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; |
388 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A=A' & Tk=Tk' & B=B' & X = X'" |
|
13926 | 389 |
apply (erule rev_mp) |
390 |
apply (erule rev_mp) |
|
18886 | 391 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
392 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 393 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all) |
394 |
txt{*BK2: it can't be a new key*} |
|
395 |
apply blast |
|
396 |
done |
|
397 |
||
398 |
lemma Server_Unique: |
|
399 |
"\<lbrakk> Says Server A |
|
400 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
401 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> |
|
402 |
Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
403 |
on evs" |
|
404 |
apply (erule rev_mp, erule bankerberos.induct, simp_all add: Unique_def) |
|
13926 | 405 |
apply blast |
406 |
done |
|
407 |
||
408 |
||
18886 | 409 |
subsection{*Non-temporal guarantees, explicitly relying on non-occurrence of |
410 |
oops events - refined below by temporal guarantees*} |
|
411 |
||
412 |
text{*Non temporal treatment of confidentiality*} |
|
413 |
||
414 |
text{* Lemma: the session key sent in msg BK2 would be lost by oops |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
415 |
if the spy could see it! *} |
18886 | 416 |
lemma lemma_conf [rule_format (no_asm)]: |
417 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
418 |
\<Longrightarrow> Says Server A |
|
419 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
420 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
421 |
\<in> set evs \<longrightarrow> |
|
422 |
Key K \<in> analz (spies evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs" |
|
423 |
apply (erule bankerberos.induct) |
|
424 |
apply (frule_tac [7] Says_Server_message_form) |
|
425 |
apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
|
426 |
apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes) |
|
427 |
txt{*Fake*} |
|
428 |
apply spy_analz |
|
429 |
txt{*BK2*} |
|
430 |
apply (blast intro: parts_insertI) |
|
431 |
txt{*BK3*} |
|
432 |
apply (case_tac "Aa \<in> bad") |
|
433 |
prefer 2 apply (blast dest: Kab_authentic unique_session_keys) |
|
434 |
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz) |
|
435 |
txt{*Oops*} |
|
436 |
apply (blast dest: unique_session_keys) |
|
437 |
done |
|
438 |
||
439 |
||
440 |
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
|
441 |
as long as they have not expired.*} |
|
442 |
lemma Confidentiality_S: |
|
443 |
"\<lbrakk> Says Server A |
|
444 |
(Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
445 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
446 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
447 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
448 |
apply (frule Says_Server_message_form, assumption) |
|
449 |
apply (blast intro: lemma_conf) |
|
450 |
done |
|
451 |
||
452 |
text{*Confidentiality for Alice*} |
|
453 |
lemma Confidentiality_A: |
|
454 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
455 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
456 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
457 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
458 |
apply (blast dest!: Kab_authentic Confidentiality_S) |
|
459 |
done |
|
460 |
||
461 |
text{*Confidentiality for Bob*} |
|
462 |
lemma Confidentiality_B: |
|
463 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
464 |
\<in> parts (spies evs); |
|
465 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
466 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
467 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
468 |
apply (blast dest!: ticket_authentic Confidentiality_S) |
|
469 |
done |
|
470 |
||
471 |
text{*Non temporal treatment of authentication*} |
|
13926 | 472 |
|
18886 | 473 |
text{*Lemmas @{text lemma_A} and @{text lemma_B} in fact are common to both temporal and non-temporal treatments*} |
474 |
lemma lemma_A [rule_format]: |
|
475 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
476 |
\<Longrightarrow> |
|
477 |
Key K \<notin> analz (spies evs) \<longrightarrow> |
|
478 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
479 |
\<in> set evs \<longrightarrow> |
|
480 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
481 |
Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> |
|
482 |
\<in> set evs" |
|
483 |
apply (erule bankerberos.induct) |
|
484 |
apply (frule_tac [7] Oops_parts_spies) |
|
485 |
apply (frule_tac [5] Says_S_message_form) |
|
486 |
apply (frule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra) |
|
487 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
488 |
txt{*Fake*} |
|
489 |
apply blast |
|
490 |
txt{*BK2*} |
|
491 |
apply (force dest: Crypt_imp_invKey_keysFor) |
|
492 |
txt{*BK3*} |
|
493 |
apply (blast dest: Kab_authentic unique_session_keys) |
|
494 |
done |
|
495 |
lemma lemma_B [rule_format]: |
|
496 |
"\<lbrakk> B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
497 |
\<Longrightarrow> Key K \<notin> analz (spies evs) \<longrightarrow> |
|
498 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
499 |
\<in> set evs \<longrightarrow> |
|
500 |
Crypt K (Number Ta) \<in> parts (spies evs) \<longrightarrow> |
|
501 |
Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
502 |
apply (erule bankerberos.induct) |
|
503 |
apply (frule_tac [7] Oops_parts_spies) |
|
504 |
apply (frule_tac [5] Says_S_message_form) |
|
505 |
apply (drule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra) |
|
506 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
507 |
txt{*Fake*} |
|
508 |
apply blast |
|
509 |
txt{*BK2*} |
|
510 |
apply (force dest: Crypt_imp_invKey_keysFor) |
|
511 |
txt{*BK4*} |
|
512 |
apply (blast dest: ticket_authentic unique_session_keys |
|
513 |
Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) |
|
514 |
done |
|
515 |
||
516 |
||
517 |
text{*The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
|
518 |
||
519 |
||
520 |
text{*Authentication of A to B*} |
|
521 |
lemma B_authenticates_A_r: |
|
522 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
523 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
524 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
525 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
526 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
527 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
528 |
apply (blast dest!: ticket_authentic |
|
529 |
intro!: lemma_A |
|
530 |
elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
531 |
done |
|
532 |
||
533 |
||
534 |
text{*Authentication of B to A*} |
|
535 |
lemma A_authenticates_B_r: |
|
536 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
537 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
538 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
539 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
540 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
541 |
apply (blast dest!: Kab_authentic |
|
542 |
intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
543 |
done |
|
544 |
||
545 |
lemma B_authenticates_A: |
|
546 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
547 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
548 |
Key K \<notin> analz (spies evs); |
|
549 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
550 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
551 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
552 |
apply (blast dest!: ticket_authentic intro!: lemma_A) |
|
553 |
done |
|
554 |
||
555 |
lemma A_authenticates_B: |
|
556 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
557 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
558 |
Key K \<notin> analz (spies evs); |
|
559 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
560 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
561 |
apply (blast dest!: Kab_authentic intro!: lemma_B) |
|
562 |
done |
|
563 |
||
564 |
subsection{*Temporal guarantees, relying on a temporal check that insures that |
|
565 |
no oops event occurred. These are available in the sense of goal availability*} |
|
566 |
||
567 |
||
568 |
text{*Temporal treatment of confidentiality*} |
|
569 |
||
570 |
text{* Lemma: the session key sent in msg BK2 would be EXPIRED |
|
571 |
if the spy could see it! *} |
|
572 |
lemma lemma_conf_temporal [rule_format (no_asm)]: |
|
573 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
574 |
\<Longrightarrow> Says Server A |
|
575 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
576 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
577 |
\<in> set evs \<longrightarrow> |
|
578 |
Key K \<in> analz (spies evs) \<longrightarrow> expiredK Tk evs" |
|
579 |
apply (erule bankerberos.induct) |
|
13926 | 580 |
apply (frule_tac [7] Says_Server_message_form) |
581 |
apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
|
582 |
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
|
583 |
txt{*Fake*} |
|
584 |
apply spy_analz |
|
18886 | 585 |
txt{*BK2*} |
13926 | 586 |
apply (blast intro: parts_insertI less_SucI) |
18886 | 587 |
txt{*BK3*} |
13926 | 588 |
apply (case_tac "Aa \<in> bad") |
18886 | 589 |
prefer 2 apply (blast dest: Kab_authentic unique_session_keys) |
13926 | 590 |
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) |
18886 | 591 |
txt{*Oops: PROOF FAILS if unsafe intro below*} |
13926 | 592 |
apply (blast dest: unique_session_keys intro!: less_SucI) |
593 |
done |
|
5053 | 594 |
|
595 |
||
18886 | 596 |
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
597 |
as long as they have not expired.*} |
18886 | 598 |
lemma Confidentiality_S_temporal: |
599 |
"\<lbrakk> Says Server A |
|
600 |
(Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
601 |
\<not> expiredK T evs; |
|
602 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
603 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
13926 | 604 |
apply (frule Says_Server_message_form, assumption) |
18886 | 605 |
apply (blast intro: lemma_conf_temporal) |
13926 | 606 |
done |
607 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
608 |
text{*Confidentiality for Alice*} |
18886 | 609 |
lemma Confidentiality_A_temporal: |
610 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
611 |
\<not> expiredK T evs; |
|
612 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
613 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
614 |
apply (blast dest!: Kab_authentic Confidentiality_S_temporal) |
|
615 |
done |
|
13926 | 616 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
617 |
text{*Confidentiality for Bob*} |
18886 | 618 |
lemma Confidentiality_B_temporal: |
619 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
620 |
\<in> parts (spies evs); |
18886 | 621 |
\<not> expiredK Tk evs; |
622 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
623 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
624 |
apply (blast dest!: ticket_authentic Confidentiality_S_temporal) |
|
625 |
done |
|
626 |
||
627 |
text{*Temporal treatment of authentication*} |
|
628 |
||
629 |
text{*Authentication of A to B*} |
|
630 |
lemma B_authenticates_A_temporal: |
|
631 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
632 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
633 |
\<in> parts (spies evs); |
|
634 |
\<not> expiredK Tk evs; |
|
635 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
636 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
637 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
638 |
apply (blast dest!: ticket_authentic |
|
639 |
intro!: lemma_A |
|
640 |
elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
641 |
done |
|
642 |
||
643 |
text{*Authentication of B to A*} |
|
644 |
lemma A_authenticates_B_temporal: |
|
645 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
646 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
647 |
\<in> parts (spies evs); |
|
648 |
\<not> expiredK Tk evs; |
|
649 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
650 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
651 |
apply (blast dest!: Kab_authentic |
|
652 |
intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
653 |
done |
|
654 |
||
655 |
subsection{*Treatment of the key distribution goal using trace inspection. All |
|
656 |
guarantees are in non-temporal form, hence non available, though their temporal |
|
657 |
form is trivial to derive. These guarantees also convey a stronger form of |
|
658 |
authentication - non-injective agreement on the session key*} |
|
13926 | 659 |
|
5053 | 660 |
|
18886 | 661 |
lemma B_Issues_A: |
662 |
"\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs; |
|
663 |
Key K \<notin> analz (spies evs); |
|
664 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
665 |
\<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs" |
|
666 |
apply (simp (no_asm) add: Issues_def) |
|
667 |
apply (rule exI) |
|
668 |
apply (rule conjI, assumption) |
|
669 |
apply (simp (no_asm)) |
|
670 |
apply (erule rev_mp) |
|
671 |
apply (erule rev_mp) |
|
672 |
apply (erule bankerberos.induct, analz_mono_contra) |
|
673 |
apply (simp_all (no_asm_simp)) |
|
674 |
txt{*fake*} |
|
13926 | 675 |
apply blast |
18886 | 676 |
txt{*K4 obviously is the non-trivial case*} |
677 |
apply (simp add: takeWhile_tail) |
|
678 |
apply (blast dest: ticket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: A_authenticates_B_temporal) |
|
679 |
done |
|
680 |
||
681 |
lemma A_authenticates_and_keydist_to_B: |
|
682 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
683 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
684 |
Key K \<notin> analz (spies evs); |
|
685 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
686 |
\<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs" |
|
687 |
apply (blast dest!: A_authenticates_B B_Issues_A) |
|
13926 | 688 |
done |
689 |
||
690 |
||
18886 | 691 |
lemma A_Issues_B: |
692 |
"\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> |
|
693 |
\<in> set evs; |
|
694 |
Key K \<notin> analz (spies evs); |
|
695 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
696 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs" |
|
697 |
apply (simp (no_asm) add: Issues_def) |
|
698 |
apply (rule exI) |
|
699 |
apply (rule conjI, assumption) |
|
700 |
apply (simp (no_asm)) |
|
701 |
apply (erule rev_mp) |
|
702 |
apply (erule rev_mp) |
|
703 |
apply (erule bankerberos.induct, analz_mono_contra) |
|
704 |
apply (simp_all (no_asm_simp)) |
|
705 |
txt{*fake*} |
|
13926 | 706 |
apply blast |
18886 | 707 |
txt{*K3 is the non trivial case*} |
708 |
apply (simp add: takeWhile_tail) |
|
709 |
apply auto (*Technically unnecessary, merely clarifies the subgoal as it is presemted in the book*) |
|
710 |
apply (blast dest: Kab_authentic Says_Server_message_form parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] |
|
711 |
intro!: B_authenticates_A) |
|
13926 | 712 |
done |
713 |
||
18886 | 714 |
|
715 |
lemma B_authenticates_and_keydist_to_A: |
|
716 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
717 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
718 |
Key K \<notin> analz (spies evs); |
|
719 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
720 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs" |
|
721 |
apply (blast dest: B_authenticates_A A_Issues_B) |
|
722 |
done |
|
723 |
||
724 |
||
725 |
||
5053 | 726 |
|
727 |
end |