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