author | paulson |
Tue, 08 Sep 1998 15:17:11 +0200 | |
changeset 5434 | 9b4bed3f394c |
parent 5421 | 01fc8d6a40f2 |
child 5479 | 5a5dfb0f0d7d |
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) |
|
5064 | 11 |
|
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset
|
12 |
Confidentiality (secrecy) and authentication properties rely on |
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset
|
13 |
temporal checks: strong guarantees in a little abstracted - but |
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset
|
14 |
very realistic - model (see .thy). |
5053 | 15 |
|
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5114
diff
changeset
|
16 |
Tidied by lcp. |
5053 | 17 |
*) |
18 |
||
19 |
AddEs spies_partsEs; |
|
20 |
AddDs [impOfSubs analz_subset_parts]; |
|
21 |
AddDs [impOfSubs Fake_parts_insert]; |
|
22 |
||
5064 | 23 |
AddIffs [SesKeyLife_LB, AutLife_LB]; |
5053 | 24 |
|
25 |
||
26 |
(*A "possibility property": there are traces that reach the end.*) |
|
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset
|
27 |
Goal "EX Timestamp K. EX evs: kerberos_ban. \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
28 |
\ Says B A (Crypt K (Number Timestamp)) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
29 |
\ : set evs"; |
5352 | 30 |
by (cut_facts_tac [SesKeyLife_LB] 1); |
5053 | 31 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
32 |
by (rtac (kerberos_ban.Nil RS kerberos_ban.Kb1 RS kerberos_ban.Kb2 RS |
|
33 |
kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2); |
|
34 |
by possibility_tac; |
|
5352 | 35 |
by (ALLGOALS Asm_simp_tac); |
36 |
by (ALLGOALS trans_tac); |
|
5053 | 37 |
result(); |
38 |
||
39 |
||
40 |
||
41 |
(**** Inductive proofs about kerberos_ban ****) |
|
42 |
||
43 |
(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
44 |
Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
45 |
\ ==> X : parts (spies evs)"; |
5053 | 46 |
by (Blast_tac 1); |
47 |
qed "Kb3_msg_in_parts_spies"; |
|
48 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
49 |
Goal "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
50 |
\ ==> K : parts (spies evs)"; |
5053 | 51 |
by (Blast_tac 1); |
52 |
qed "Oops_parts_spies"; |
|
53 |
||
54 |
(*For proving the easier theorems about X ~: parts (spies evs).*) |
|
55 |
fun parts_induct_tac i = |
|
56 |
etac kerberos_ban.induct i THEN |
|
57 |
forward_tac [Oops_parts_spies] (i+6) THEN |
|
58 |
forward_tac [Kb3_msg_in_parts_spies] (i+4) THEN |
|
59 |
prove_simple_subgoals_tac i; |
|
60 |
||
61 |
||
62 |
(*Spy never sees another agent's shared key! (unless it's bad at start)*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
63 |
Goal "evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
5053 | 64 |
by (parts_induct_tac 1); |
65 |
by (ALLGOALS Blast_tac); |
|
66 |
qed "Spy_see_shrK"; |
|
67 |
Addsimps [Spy_see_shrK]; |
|
68 |
||
69 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
70 |
Goal "evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
5053 | 71 |
by Auto_tac; |
72 |
qed "Spy_analz_shrK"; |
|
73 |
Addsimps [Spy_analz_shrK]; |
|
74 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
75 |
Goal "[| Key (shrK A) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
76 |
\ evs : kerberos_ban |] ==> A:bad"; |
5053 | 77 |
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); |
78 |
qed "Spy_see_shrK_D"; |
|
79 |
||
80 |
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
|
81 |
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
|
82 |
||
83 |
||
84 |
(*Nobody can have used non-existent keys!*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
85 |
Goal "evs : kerberos_ban ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
86 |
\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
5053 | 87 |
by (parts_induct_tac 1); |
88 |
(*Fake*) |
|
89 |
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
|
90 |
(*Kb2, Kb3, Kb4*) |
|
91 |
by (ALLGOALS Blast_tac); |
|
92 |
qed_spec_mp "new_keys_not_used"; |
|
93 |
||
94 |
bind_thm ("new_keys_not_analzd", |
|
95 |
[analz_subset_parts RS keysFor_mono, |
|
96 |
new_keys_not_used] MRS contra_subsetD); |
|
97 |
||
98 |
Addsimps [new_keys_not_used, new_keys_not_analzd]; |
|
99 |
||
100 |
||
101 |
(** Lemmas concerning the form of items passed in messages **) |
|
102 |
||
103 |
(*Describes the form of K, X and K' when the Server sends this message.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
104 |
Goal "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
105 |
\ : set evs; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
106 |
\ ==> K ~: range shrK & \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
107 |
\ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
108 |
\ K' = shrK A"; |
5053 | 109 |
by (etac rev_mp 1); |
110 |
by (etac kerberos_ban.induct 1); |
|
111 |
by Auto_tac; |
|
112 |
qed "Says_Server_message_form"; |
|
113 |
||
114 |
||
115 |
(*If the encrypted message appears then it originated with the Server |
|
116 |
PROVIDED that A is NOT compromised! |
|
117 |
||
118 |
This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
|
119 |
*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
120 |
Goal "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
121 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
122 |
\ A ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
123 |
\ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
124 |
\ : set evs"; |
5053 | 125 |
by (etac rev_mp 1); |
126 |
by (parts_induct_tac 1); |
|
127 |
by (Blast_tac 1); |
|
128 |
qed "A_trusts_K_by_Kb2"; |
|
129 |
||
130 |
||
131 |
(*If the TICKET appears then it originated with the Server*) |
|
132 |
(*FRESHNESS OF THE SESSION KEY to B*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
133 |
Goal "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
134 |
\ B ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
135 |
\ ==> Says Server A \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
136 |
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
137 |
\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
138 |
\ : set evs"; |
5053 | 139 |
by (etac rev_mp 1); |
140 |
by (parts_induct_tac 1); |
|
141 |
by (Blast_tac 1); |
|
142 |
qed "B_trusts_K_by_Kb3"; |
|
143 |
||
144 |
||
145 |
(*EITHER describes the form of X when the following message is sent, |
|
146 |
OR reduces it to the Fake case. |
|
147 |
Use Says_Server_message_form if applicable.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
148 |
Goal "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
149 |
\ : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
150 |
\ evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
151 |
\==> (K ~: range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
152 |
\ | X : analz (spies evs)"; |
5053 | 153 |
by (case_tac "A : bad" 1); |
154 |
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] |
|
155 |
addss (simpset())) 1); |
|
156 |
by (forward_tac [Says_imp_spies RS parts.Inj] 1); |
|
157 |
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, |
|
158 |
Says_Server_message_form]) 1); |
|
159 |
qed "Says_S_message_form"; |
|
160 |
||
161 |
||
162 |
(*For proofs involving analz.*) |
|
163 |
val analz_spies_tac = |
|
164 |
forward_tac [Says_Server_message_form] 7 THEN |
|
165 |
forward_tac [Says_S_message_form] 5 THEN |
|
166 |
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); |
|
167 |
||
168 |
||
169 |
(**** |
|
170 |
The following is to prove theorems of the form |
|
171 |
||
172 |
Key K : analz (insert (Key KAB) (spies evs)) ==> |
|
173 |
Key K : analz (spies evs) |
|
174 |
||
175 |
A more general formula must be proved inductively. |
|
176 |
||
177 |
****) |
|
178 |
||
179 |
||
180 |
(** Session keys are not used to encrypt other session keys **) |
|
181 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
182 |
Goal "evs : kerberos_ban ==> \ |
5053 | 183 |
\ ALL K KK. KK <= Compl (range shrK) --> \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
184 |
\ (Key K : analz (Key``KK Un (spies evs))) = \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
185 |
\ (K : KK | Key K : analz (spies evs))"; |
5053 | 186 |
by (etac kerberos_ban.induct 1); |
187 |
by analz_spies_tac; |
|
188 |
by (REPEAT_FIRST (resolve_tac [allI, impI])); |
|
189 |
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
|
190 |
(*Takes 5 secs*) |
|
191 |
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
|
192 |
(*Fake*) |
|
193 |
by (spy_analz_tac 1); |
|
194 |
qed_spec_mp "analz_image_freshK"; |
|
195 |
||
196 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
197 |
Goal "[| evs : kerberos_ban; KAB ~: range shrK |] ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
198 |
\ Key K : analz (insert (Key KAB) (spies evs)) = \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
199 |
\ (K = KAB | Key K : analz (spies evs))"; |
5053 | 200 |
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
201 |
qed "analz_insert_freshK"; |
|
202 |
||
203 |
||
204 |
(** The session key K uniquely identifies the message **) |
|
205 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
206 |
Goal "evs : kerberos_ban ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
207 |
\ EX A' Ts' B' X'. ALL A Ts B X. \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
208 |
\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
209 |
\ : set evs \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
210 |
\ --> A=A' & Ts=Ts' & B=B' & X=X'"; |
5053 | 211 |
by (etac kerberos_ban.induct 1); |
212 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
|
213 |
by Safe_tac; |
|
214 |
(*Kb2: it can't be a new key*) |
|
215 |
by (expand_case_tac "K = ?y" 1); |
|
216 |
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); |
|
217 |
by (blast_tac (claset() delrules [conjI]) 1); |
|
218 |
val lemma = result(); |
|
219 |
||
220 |
(*In messages of this form, the session key uniquely identifies the rest*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
221 |
Goal "[| Says Server A \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
222 |
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
223 |
\ Says Server A' \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
224 |
\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
225 |
\ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"; |
5053 | 226 |
by (prove_unique_tac lemma 1); |
227 |
qed "unique_session_keys"; |
|
228 |
||
229 |
||
230 |
(** Lemma: the session key sent in msg Kb2 would be EXPIRED |
|
231 |
if the spy could see it! |
|
232 |
**) |
|
233 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
234 |
Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
235 |
\ ==> Says Server A \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
236 |
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
237 |
\ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
238 |
\ : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
239 |
\ Key K : analz (spies evs) --> Expired Ts evs"; |
5053 | 240 |
by (etac kerberos_ban.induct 1); |
241 |
by analz_spies_tac; |
|
242 |
by (ALLGOALS |
|
5064 | 243 |
(asm_simp_tac (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] |
244 |
@ pushes)))); |
|
5053 | 245 |
(*Oops*) |
246 |
by (blast_tac (claset() addDs [unique_session_keys] addIs [less_SucI]) 4); |
|
247 |
(*Kb2*) |
|
5064 | 248 |
by (blast_tac (claset() addIs [parts_insertI, less_SucI]) 2); |
5053 | 249 |
(*Fake*) |
250 |
by (spy_analz_tac 1); |
|
251 |
(**LEVEL 6 **) |
|
5064 | 252 |
(*Kb3*) |
5053 | 253 |
by (case_tac "Aa : bad" 1); |
5064 | 254 |
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 2); |
255 |
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj, |
|
256 |
Crypt_Spy_analz_bad, analz.Fst, analz.Snd] |
|
5053 | 257 |
addIs [less_SucI]) 1); |
258 |
val lemma = result() RS mp RS mp RSN(1,rev_notE); |
|
259 |
||
260 |
||
261 |
(** CONFIDENTIALITY for the SERVER: |
|
262 |
Spy does not see the keys sent in msg Kb2 |
|
263 |
as long as they have NOT EXPIRED |
|
264 |
**) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
265 |
Goal "[| Says Server A \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
266 |
\ (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
267 |
\ ~ Expired T evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
268 |
\ A ~: bad; B ~: bad; evs : kerberos_ban \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
269 |
\ |] ==> Key K ~: analz (spies evs)"; |
5053 | 270 |
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
5064 | 271 |
by (Clarify_tac 1); (*prevents PROOF FAILED*) |
5053 | 272 |
by (blast_tac (claset() addSEs [lemma]) 1); |
273 |
qed "Confidentiality_S"; |
|
274 |
||
275 |
(**** THE COUNTERPART OF CONFIDENTIALITY |
|
276 |
[|...; Expired Ts evs; ...|] ==> Key K : analz (spies evs) |
|
277 |
WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
|
278 |
||
279 |
||
280 |
(** CONFIDENTIALITY for ALICE: **) |
|
281 |
(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
282 |
Goal "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
283 |
\ ~ Expired T evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
284 |
\ A ~: bad; B ~: bad; evs : kerberos_ban \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
285 |
\ |] ==> Key K ~: analz (spies evs)"; |
5064 | 286 |
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2, Confidentiality_S]) 1); |
5053 | 287 |
qed "Confidentiality_A"; |
288 |
||
289 |
||
290 |
(** CONFIDENTIALITY for BOB: **) |
|
291 |
(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
292 |
Goal "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
293 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
294 |
\ ~ Expired Tk evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
295 |
\ A ~: bad; B ~: bad; evs : kerberos_ban \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
296 |
\ |] ==> Key K ~: analz (spies evs)"; |
5053 | 297 |
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3, |
298 |
Confidentiality_S]) 1); |
|
299 |
qed "Confidentiality_B"; |
|
300 |
||
301 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
302 |
Goal "[| B ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
303 |
\ ==> Key K ~: analz (spies evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
304 |
\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
305 |
\ : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
306 |
\ Crypt K (Number Ta) : parts (spies evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
307 |
\ Says B A (Crypt K (Number Ta)) : set evs"; |
5053 | 308 |
by (etac kerberos_ban.induct 1); |
309 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
310 |
by (dtac Kb3_msg_in_parts_spies 5); |
|
311 |
by (forward_tac [Oops_parts_spies] 7); |
|
5064 | 312 |
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); |
5053 | 313 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
5064 | 314 |
(**LEVEL 6**) |
5053 | 315 |
by (Blast_tac 1); |
5064 | 316 |
by (Clarify_tac 1); |
5053 | 317 |
(* |
318 |
Subgoal 1: contradiction from the assumptions |
|
319 |
Key K ~: used evs2 and Crypt K (Number Ta) : parts (spies evs2) |
|
320 |
*) |
|
321 |
by (dtac Crypt_imp_invKey_keysFor 1); |
|
322 |
by (Asm_full_simp_tac 1); |
|
5064 | 323 |
(* the two tactics above detect the contradiction*) |
5053 | 324 |
by (case_tac "Ba : bad" 1); (*splits up the subgoal by the stated case*) |
325 |
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS parts.Fst RS |
|
326 |
B_trusts_K_by_Kb3, |
|
327 |
unique_session_keys]) 2); |
|
328 |
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS analz.Fst RS |
|
329 |
Crypt_Spy_analz_bad]) 1); |
|
330 |
val lemma_B = result(); |
|
331 |
||
332 |
||
333 |
(*AUTHENTICATION OF B TO A*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
334 |
Goal "[| Crypt K (Number Ta) : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
335 |
\ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
336 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
337 |
\ ~ Expired Ts evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
338 |
\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
339 |
\ ==> Says B A (Crypt K (Number Ta)) : set evs"; |
5053 | 340 |
by (blast_tac (claset() addSDs [A_trusts_K_by_Kb2] |
341 |
addSIs [lemma_B RS mp RS mp RS mp] |
|
342 |
addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
343 |
qed "Authentication_B"; |
|
344 |
||
345 |
||
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
346 |
Goal "[| A ~: bad; B ~: bad; evs : kerberos_ban |] ==> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
347 |
\ Key K ~: analz (spies evs) --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
348 |
\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
349 |
\ : set evs --> \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
350 |
\ Crypt K {|Agent A, Number Ta|} : parts (spies evs) -->\ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
351 |
\ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
352 |
\ : set evs"; |
5053 | 353 |
by (etac kerberos_ban.induct 1); |
354 |
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); |
|
355 |
by (forward_tac [Kb3_msg_in_parts_spies] 5); |
|
356 |
by (forward_tac [Oops_parts_spies] 7); |
|
5064 | 357 |
by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); |
5053 | 358 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
5064 | 359 |
(**LEVEL 6**) |
5053 | 360 |
by (Blast_tac 1); |
5064 | 361 |
by (Clarify_tac 1); |
5053 | 362 |
by (dtac Crypt_imp_invKey_keysFor 1); |
363 |
by (Asm_full_simp_tac 1); |
|
5064 | 364 |
by (blast_tac (claset() addDs [A_trusts_K_by_Kb2, unique_session_keys]) 1); |
5053 | 365 |
val lemma_A = result(); |
366 |
||
367 |
||
368 |
(*AUTHENTICATION OF A TO B*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
369 |
Goal "[| Crypt K {|Agent A, Number Ta|} : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
370 |
\ Crypt (shrK B) {|Number Ts, Agent A, Key K|} \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
371 |
\ : parts (spies evs); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
372 |
\ ~ Expired Ts evs; \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
373 |
\ A ~: bad; B ~: bad; evs : kerberos_ban |] \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
374 |
\ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
375 |
\ Crypt K {|Agent A, Number Ta|}|} : set evs"; |
5053 | 376 |
by (blast_tac (claset() addSDs [B_trusts_K_by_Kb3] |
377 |
addSIs [lemma_A RS mp RS mp RS mp] |
|
378 |
addSEs [Confidentiality_S RSN (2,rev_notE)]) 1); |
|
379 |
qed "Authentication_A"; |