|
1 (* Title: HOL/Auth/ZhouGollmann |
|
2 ID: $Id$ |
|
3 Author: Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab |
|
4 Copyright 2003 University of Cambridge |
|
5 |
|
6 The protocol of |
|
7 Jianying Zhou and Dieter Gollmann, |
|
8 A Fair Non-Repudiation Protocol, |
|
9 Security and Privacy 1996 (Oakland) |
|
10 55-61 |
|
11 *) |
|
12 |
|
13 theory ZhouGollmann = Public: |
|
14 |
|
15 syntax |
|
16 TTP :: agent |
|
17 |
|
18 translations |
|
19 "TTP" == "Server" |
|
20 |
|
21 syntax |
|
22 f_sub :: nat |
|
23 f_nro :: nat |
|
24 f_nrr :: nat |
|
25 f_con :: nat |
|
26 |
|
27 translations |
|
28 "f_sub" == "5" |
|
29 "f_nro" == "2" |
|
30 "f_nrr" == "3" |
|
31 "f_con" == "4" |
|
32 |
|
33 |
|
34 constdefs |
|
35 broken :: "agent set" |
|
36 --{*the compromised honest agents; TTP is included as it's not allowed to |
|
37 use the protocol*} |
|
38 "broken == insert TTP (bad - {Spy})" |
|
39 |
|
40 declare broken_def [simp] |
|
41 |
|
42 consts zg :: "event list set" |
|
43 |
|
44 inductive zg |
|
45 intros |
|
46 |
|
47 Nil: "[] \<in> zg" |
|
48 |
|
49 Fake: "[| evsf \<in> zg; X \<in> synth (analz (spies evsf)) |] |
|
50 ==> Says Spy B X # evsf \<in> zg" |
|
51 |
|
52 Reception: "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |] |
|
53 ==> Gets B X # evsr \<in> zg" |
|
54 |
|
55 (*L is fresh for honest agents. |
|
56 We don't require K to be fresh because we don't bother to prove secrecy! |
|
57 We just assume that the protocol's objective is to deliver K fairly, |
|
58 rather than to keep M secret.*) |
|
59 ZG1: "[| evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m); |
|
60 K \<in> symKeys; |
|
61 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|] |
|
62 ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg" |
|
63 |
|
64 (*B must check that NRO is A's signature to learn the sender's name*) |
|
65 ZG2: "[| evs2 \<in> zg; |
|
66 Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2; |
|
67 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; |
|
68 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|] |
|
69 ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2 \<in> zg" |
|
70 |
|
71 (*K is symmetric must be repeated IF there's spy*) |
|
72 (*A must check that NRR is B's signature to learn the sender's name*) |
|
73 (*without spy, the matching label would be enough*) |
|
74 ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys; |
|
75 Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3; |
|
76 Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3; |
|
77 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; |
|
78 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|] |
|
79 ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} |
|
80 # evs3 \<in> zg" |
|
81 |
|
82 (*TTP checks that sub_K is A's signature to learn who issued K, then |
|
83 gives credentials to A and B. The Notes event models the availability of |
|
84 the credentials, but the act of fetching them is not modelled.*) |
|
85 (*Also said TTP_prepare_ftp*) |
|
86 ZG4: "[| evs4 \<in> zg; K \<in> symKeys; |
|
87 Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} |
|
88 \<in> set evs4; |
|
89 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
90 con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B, |
|
91 Nonce L, Key K|}|] |
|
92 ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|} |
|
93 # evs4 \<in> zg" |
|
94 |
|
95 |
|
96 declare Says_imp_knows_Spy [THEN analz.Inj, dest] |
|
97 declare Fake_parts_insert_in_Un [dest] |
|
98 declare analz_into_parts [dest] |
|
99 |
|
100 declare symKey_neq_priEK [simp] |
|
101 declare symKey_neq_priEK [THEN not_sym, simp] |
|
102 |
|
103 |
|
104 subsection {*Basic Lemmas*} |
|
105 |
|
106 lemma Gets_imp_Says: |
|
107 "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs" |
|
108 apply (erule rev_mp) |
|
109 apply (erule zg.induct, auto) |
|
110 done |
|
111 |
|
112 lemma Gets_imp_knows_Spy: |
|
113 "[| Gets B X \<in> set evs; evs \<in> zg |] ==> X \<in> spies evs" |
|
114 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
115 |
|
116 |
|
117 text{*Lets us replace proofs about @{term "used evs"} by simpler proofs |
|
118 about @{term "parts (spies evs)"}.*} |
|
119 lemma Crypt_used_imp_spies: |
|
120 "[| Crypt K X \<in> used evs; K \<noteq> priK TTP; evs \<in> zg |] |
|
121 ==> Crypt K X \<in> parts (spies evs)" |
|
122 apply (erule rev_mp) |
|
123 apply (erule zg.induct) |
|
124 apply (simp_all add: parts_insert_knows_A) |
|
125 done |
|
126 |
|
127 lemma Notes_TTP_imp_Gets: |
|
128 "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |} |
|
129 \<in> set evs; |
|
130 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
131 evs \<in> zg|] |
|
132 ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs" |
|
133 apply (erule rev_mp) |
|
134 apply (erule zg.induct, auto) |
|
135 done |
|
136 |
|
137 text{*For reasoning about C, which is encrypted in message ZG2*} |
|
138 lemma ZG2_msg_in_parts_spies: |
|
139 "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|] |
|
140 ==> C \<in> parts (spies evs)" |
|
141 by (blast dest: Gets_imp_Says) |
|
142 |
|
143 (*classical regularity lemma on priK*) |
|
144 lemma Spy_see_priK [simp]: |
|
145 "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)" |
|
146 apply (erule zg.induct) |
|
147 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) |
|
148 done |
|
149 |
|
150 text{*So that blast can use it too*} |
|
151 declare Spy_see_priK [THEN [2] rev_iffD1, dest!] |
|
152 |
|
153 lemma Spy_analz_priK [simp]: |
|
154 "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)" |
|
155 by auto |
|
156 |
|
157 |
|
158 subsection{*About NRO*} |
|
159 |
|
160 text{*Below we prove that if @{term NRO} exists then @{term A} definitely |
|
161 sent it, provided @{term A} is not broken. *} |
|
162 |
|
163 text{*Strong conclusion for a good agent*} |
|
164 lemma NRO_authenticity_good: |
|
165 "[| NRO \<in> parts (spies evs); |
|
166 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; |
|
167 A \<notin> bad; evs \<in> zg |] |
|
168 ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs" |
|
169 apply clarify |
|
170 apply (erule rev_mp) |
|
171 apply (erule zg.induct) |
|
172 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) |
|
173 done |
|
174 |
|
175 text{*A compromised agent: we can't be sure whether A or the Spy sends the |
|
176 message or of the precise form of the message*} |
|
177 lemma NRO_authenticity_bad: |
|
178 "[| NRO \<in> parts (spies evs); |
|
179 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; |
|
180 A \<in> bad; evs \<in> zg |] |
|
181 ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}" |
|
182 apply clarify |
|
183 apply (erule rev_mp) |
|
184 apply (erule zg.induct) |
|
185 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
186 txt{*ZG3*} |
|
187 prefer 4 apply blast |
|
188 txt{*ZG2*} |
|
189 prefer 3 apply blast |
|
190 txt{*Fake*} |
|
191 apply (simp add: parts_insert_knows_A, blast) |
|
192 txt{*ZG1*} |
|
193 apply (auto intro!: exI) |
|
194 done |
|
195 |
|
196 theorem NRO_authenticity: |
|
197 "[| NRO \<in> used evs; |
|
198 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; |
|
199 A \<notin> broken; evs \<in> zg |] |
|
200 ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}" |
|
201 apply auto |
|
202 apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good) |
|
203 apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad) |
|
204 done |
|
205 |
|
206 |
|
207 subsection{*About NRR*} |
|
208 |
|
209 text{*Below we prove that if @{term NRR} exists then @{term B} definitely |
|
210 sent it, provided @{term B} is not broken.*} |
|
211 |
|
212 text{*Strong conclusion for a good agent*} |
|
213 lemma NRR_authenticity_good: |
|
214 "[| NRR \<in> parts (spies evs); |
|
215 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; |
|
216 B \<notin> bad; evs \<in> zg |] |
|
217 ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs" |
|
218 apply clarify |
|
219 apply (erule rev_mp) |
|
220 apply (erule zg.induct) |
|
221 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) |
|
222 done |
|
223 |
|
224 lemma NRR_authenticity_bad: |
|
225 "[| NRR \<in> parts (spies evs); |
|
226 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; |
|
227 B \<in> bad; evs \<in> zg |] |
|
228 ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}" |
|
229 apply clarify |
|
230 apply (erule rev_mp) |
|
231 apply (erule zg.induct) |
|
232 apply (frule_tac [5] ZG2_msg_in_parts_spies) |
|
233 apply (simp_all del: bex_simps) |
|
234 txt{*ZG3*} |
|
235 prefer 4 apply blast |
|
236 txt{*Fake*} |
|
237 apply (simp add: parts_insert_knows_A, blast) |
|
238 txt{*ZG1*} |
|
239 apply (auto simp del: bex_simps) |
|
240 txt{*ZG2*} |
|
241 apply (force intro!: exI) |
|
242 done |
|
243 |
|
244 theorem NRR_authenticity: |
|
245 "[| NRR \<in> used evs; |
|
246 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; |
|
247 B \<notin> broken; evs \<in> zg |] |
|
248 ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}" |
|
249 apply auto |
|
250 apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good) |
|
251 apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad) |
|
252 done |
|
253 |
|
254 |
|
255 subsection{*Proofs About @{term sub_K}*} |
|
256 |
|
257 text{*Below we prove that if @{term sub_K} exists then @{term A} definitely |
|
258 sent it, provided @{term A} is not broken. *} |
|
259 |
|
260 text{*Strong conclusion for a good agent*} |
|
261 lemma sub_K_authenticity_good: |
|
262 "[| sub_K \<in> parts (spies evs); |
|
263 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
264 A \<notin> bad; evs \<in> zg |] |
|
265 ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs" |
|
266 apply (erule rev_mp) |
|
267 apply (erule zg.induct) |
|
268 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
269 txt{*Fake*} |
|
270 apply (blast dest!: Fake_parts_sing_imp_Un) |
|
271 done |
|
272 |
|
273 text{*A compromised agent: we can't be sure whether A or the Spy sends the |
|
274 message or of the precise form of the message*} |
|
275 lemma sub_K_authenticity_bad: |
|
276 "[| sub_K \<in> parts (spies evs); |
|
277 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
278 A \<in> bad; evs \<in> zg |] |
|
279 ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}" |
|
280 apply clarify |
|
281 apply (erule rev_mp) |
|
282 apply (erule zg.induct) |
|
283 apply (frule_tac [5] ZG2_msg_in_parts_spies) |
|
284 apply (simp_all del: bex_simps) |
|
285 txt{*Fake*} |
|
286 apply (simp add: parts_insert_knows_A, blast) |
|
287 txt{*ZG1*} |
|
288 apply (auto simp del: bex_simps) |
|
289 txt{*ZG3*} |
|
290 apply (force intro!: exI) |
|
291 done |
|
292 |
|
293 theorem sub_K_authenticity: |
|
294 "[| sub_K \<in> used evs; |
|
295 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
296 A \<notin> broken; evs \<in> zg |] |
|
297 ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}" |
|
298 apply auto |
|
299 apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good) |
|
300 apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad) |
|
301 done |
|
302 |
|
303 |
|
304 subsection{*Proofs About @{term con_K}*} |
|
305 |
|
306 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it, |
|
307 and therefore @{term A} and @{term B}) can get it too. Moreover, we know |
|
308 that @{term A} sent @{term sub_K}*} |
|
309 |
|
310 lemma con_K_authenticity: |
|
311 "[|con_K \<in> used evs; |
|
312 con_K = Crypt (priK TTP) |
|
313 {|Number f_con, Agent A, Agent B, Nonce L, Key K|}; |
|
314 evs \<in> zg |] |
|
315 ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|} |
|
316 \<in> set evs" |
|
317 apply clarify |
|
318 apply (erule rev_mp) |
|
319 apply (erule zg.induct) |
|
320 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
321 txt{*Fake*} |
|
322 apply (blast dest!: Fake_parts_sing_imp_Un) |
|
323 txt{*ZG2*} |
|
324 apply (blast dest: parts_cut) |
|
325 done |
|
326 |
|
327 text{*If @{term TTP} holds @{term con_K} then @{term A} sent |
|
328 @{term sub_K}. We assume that @{term A} is not broken. Nothing needs to |
|
329 be assumed about the form of @{term con_K}!*} |
|
330 lemma Notes_TTP_imp_Says_A: |
|
331 "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|} |
|
332 \<in> set evs; |
|
333 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
334 A \<notin> broken; evs \<in> zg|] |
|
335 ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}" |
|
336 by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity) |
|
337 |
|
338 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*} |
|
339 theorem B_sub_K_authenticity: |
|
340 "[|con_K \<in> used evs; |
|
341 con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B, |
|
342 Nonce L, Key K|}; |
|
343 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
344 A \<notin> broken; B \<noteq> TTP; evs \<in> zg|] |
|
345 ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}" |
|
346 by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A) |
|
347 |
|
348 |
|
349 subsection{*Proving fairness*} |
|
350 |
|
351 text{*Cannot prove that, if @{term B} has NRO, then @{term A} has her NRR. |
|
352 It would appear that @{term B} has a small advantage, though it is |
|
353 useless to win disputes: @{term B} needs to present @{term con_K} as well.*} |
|
354 |
|
355 text{*Strange: unicity of the label protects @{term A}?*} |
|
356 lemma A_unicity: |
|
357 "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|}; |
|
358 NRO \<in> parts (spies evs); |
|
359 Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|} |
|
360 \<in> set evs; |
|
361 A \<notin> bad; evs \<in> zg |] |
|
362 ==> M'=M" |
|
363 apply clarify |
|
364 apply (erule rev_mp) |
|
365 apply (erule rev_mp) |
|
366 apply (erule zg.induct) |
|
367 apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) |
|
368 txt{*ZG1: freshness*} |
|
369 apply (blast dest: parts.Body) |
|
370 done |
|
371 |
|
372 |
|
373 text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds |
|
374 NRR. Relies on unicity of labels.*} |
|
375 lemma sub_K_implies_NRR: |
|
376 "[| sub_K \<in> parts (spies evs); |
|
377 NRO \<in> parts (spies evs); |
|
378 sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}; |
|
379 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|}; |
|
380 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|}; |
|
381 A \<notin> bad; evs \<in> zg |] |
|
382 ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs" |
|
383 apply clarify |
|
384 apply (erule rev_mp) |
|
385 apply (erule rev_mp) |
|
386 apply (erule zg.induct) |
|
387 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
388 txt{*Fake*} |
|
389 apply blast |
|
390 txt{*ZG1: freshness*} |
|
391 apply (blast dest: parts.Body) |
|
392 txt{*ZG3*} |
|
393 apply (blast dest: A_unicity [OF refl]) |
|
394 done |
|
395 |
|
396 |
|
397 lemma Crypt_used_imp_L_used: |
|
398 "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |] |
|
399 ==> L \<in> used evs" |
|
400 apply (erule rev_mp) |
|
401 apply (erule zg.induct, auto) |
|
402 txt{*Fake*} |
|
403 apply (blast dest!: Fake_parts_sing_imp_Un) |
|
404 txt{*ZG2: freshness*} |
|
405 apply (blast dest: parts.Body) |
|
406 done |
|
407 |
|
408 |
|
409 text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, |
|
410 then @{term A} holds NRR. @{term A} must be uncompromised, but there is no |
|
411 assumption about @{term B}.*} |
|
412 theorem A_fairness_NRO: |
|
413 "[|con_K \<in> used evs; |
|
414 NRO \<in> parts (spies evs); |
|
415 con_K = Crypt (priK TTP) |
|
416 {|Number f_con, Agent A, Agent B, Nonce L, Key K|}; |
|
417 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|}; |
|
418 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|}; |
|
419 A \<notin> bad; evs \<in> zg |] |
|
420 ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs" |
|
421 apply clarify |
|
422 apply (erule rev_mp) |
|
423 apply (erule rev_mp) |
|
424 apply (erule zg.induct) |
|
425 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
426 txt{*Fake*} |
|
427 apply (simp add: parts_insert_knows_A) |
|
428 apply (blast dest: Fake_parts_sing_imp_Un) |
|
429 txt{*ZG1*} |
|
430 apply (blast dest: Crypt_used_imp_L_used) |
|
431 txt{*ZG2*} |
|
432 apply (blast dest: parts_cut) |
|
433 txt{*ZG4*} |
|
434 apply (blast intro: sub_K_implies_NRR [OF _ _ refl] |
|
435 dest: Gets_imp_knows_Spy [THEN parts.Inj]) |
|
436 done |
|
437 |
|
438 text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO. |
|
439 @{term B} must be uncompromised, but there is no assumption about @{term |
|
440 A}. *} |
|
441 theorem B_fairness_NRR: |
|
442 "[|NRR \<in> used evs; |
|
443 NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}; |
|
444 NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}; |
|
445 B \<notin> bad; evs \<in> zg |] |
|
446 ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs" |
|
447 apply clarify |
|
448 apply (erule rev_mp) |
|
449 apply (erule zg.induct) |
|
450 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) |
|
451 txt{*Fake*} |
|
452 apply (blast dest!: Fake_parts_sing_imp_Un) |
|
453 txt{*ZG2*} |
|
454 apply (blast dest: parts_cut) |
|
455 done |
|
456 |
|
457 |
|
458 text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text |
|
459 con_K_authenticity}. Cannot conclude that also NRO is available to @{term B}, |
|
460 because if @{term A} were unfair, @{term A} could build message 3 without |
|
461 building message 1, which contains NRO. *} |
|
462 |
|
463 end |