1(*  Title:      HOL/Auth/OtwayReesBella.thy
2    Author:     Giampaolo Bella, Catania University
3*)
4
5section\<open>Bella's version of the Otway-Rees protocol\<close>
6
7
8theory OtwayReesBella imports Public begin
9
10text\<open>Bella's modifications to a version of the Otway-Rees protocol taken from
11the BAN paper only concern message 7. The updated protocol makes the goal of
12key distribution of the session key available to A. Investigating the
13principle of Goal Availability undermines the BAN claim about the original
14protocol, that "this protocol does not make use of Kab as an encryption key,
15so neither principal can know whether the key is known to the other". The
16updated protocol makes no use of the session key to encrypt but informs A that
17B knows it.\<close>
18
19inductive_set orb :: "event list set"
20 where
21
22  Nil:  "[]\<in> orb"
23
24| Fake: "\<lbrakk>evsa\<in> orb;  X\<in> synth (analz (knows Spy evsa))\<rbrakk>
25         \<Longrightarrow> Says Spy B X  # evsa \<in> orb"
26
27| Reception: "\<lbrakk>evsr\<in> orb;  Says A B X \<in> set evsr\<rbrakk>
28              \<Longrightarrow> Gets B X # evsr \<in> orb"
29
30| OR1:  "\<lbrakk>evs1\<in> orb;  Nonce NA \<notin> used evs1\<rbrakk>
31         \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, 
32                   Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
33               # evs1 \<in> orb"
34
35| OR2:  "\<lbrakk>evs2\<in> orb;  Nonce NB \<notin> used evs2;
36           Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk>
37        \<Longrightarrow> Says B Server 
38                \<lbrace>Nonce M, Agent A, Agent B, X, 
39           Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
40               # evs2 \<in> orb"
41
42| OR3:  "\<lbrakk>evs3\<in> orb;  Key KAB \<notin> used evs3;
43          Gets Server 
44             \<lbrace>Nonce M, Agent A, Agent B, 
45               Crypt (shrK A) \<lbrace>Nonce NA, Nonce M, Agent A, Agent B\<rbrace>, 
46               Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
47          \<in> set evs3\<rbrakk>
48        \<Longrightarrow> Says Server B \<lbrace>Nonce M,
49                    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
50                                      Nonce NB, Key KAB\<rbrace>\<rbrace>
51               # evs3 \<in> orb"
52
53  (*B can only check that the message he is bouncing is a ciphertext*)
54  (*Sending M back is omitted*)   
55| OR4:  "\<lbrakk>evs4\<in> orb; B \<noteq> Server; \<forall> p q. X \<noteq> \<lbrace>p, q\<rbrace>; 
56          Says B Server \<lbrace>Nonce M, Agent A, Agent B, X', 
57                Crypt (shrK B) \<lbrace>Nonce NB, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
58            \<in> set evs4;
59          Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce NB, Key KAB\<rbrace>\<rbrace>
60            \<in> set evs4\<rbrakk>
61        \<Longrightarrow> Says B A \<lbrace>Nonce M, X\<rbrace> # evs4 \<in> orb"
62
63
64| Oops: "\<lbrakk>evso\<in> orb;  
65           Says Server B \<lbrace>Nonce M,
66                    Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
67                                      Nonce NB, Key KAB\<rbrace>\<rbrace> 
68             \<in> set evso\<rbrakk>
69 \<Longrightarrow> Notes Spy \<lbrace>Agent A, Agent B, Nonce NA, Nonce NB, Key KAB\<rbrace> # evso 
70     \<in> orb"
71
72
73
74declare knows_Spy_partsEs [elim]
75declare analz_into_parts [dest]
76declare Fake_parts_insert_in_Un  [dest]
77
78
79text\<open>Fragile proof, with backtracking in the possibility call.\<close>
80lemma possibility_thm: "\<lbrakk>A \<noteq> Server; B \<noteq> Server; Key K \<notin> used[]\<rbrakk>    
81      \<Longrightarrow>   \<exists> evs \<in> orb.           
82     Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
83apply (intro exI bexI)
84apply (rule_tac [2] orb.Nil
85                    [THEN orb.OR1, THEN orb.Reception,
86                     THEN orb.OR2, THEN orb.Reception,
87                     THEN orb.OR3, THEN orb.Reception, THEN orb.OR4]) 
88apply (possibility, simp add: used_Cons)  
89done
90
91
92lemma Gets_imp_Says :
93     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
94apply (erule rev_mp)
95apply (erule orb.induct)
96apply auto
97done
98
99lemma Gets_imp_knows_Spy: 
100     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
101by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
102
103declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
104
105lemma Gets_imp_knows:
106     "\<lbrakk>Gets B X \<in> set evs; evs \<in> orb\<rbrakk>  \<Longrightarrow> X \<in> knows B evs"
107by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)
108
109lemma OR2_analz_knows_Spy: 
110   "\<lbrakk>Gets B \<lbrace>Nonce M, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> orb\<rbrakk>   
111    \<Longrightarrow> X \<in> analz (knows Spy evs)"
112by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
113
114lemma OR4_parts_knows_Spy: 
115   "\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key Kab\<rbrace>\<rbrace>  \<in> set evs; 
116      evs \<in> orb\<rbrakk>   \<Longrightarrow> X \<in> parts (knows Spy evs)"
117by blast
118
119lemma Oops_parts_knows_Spy: 
120    "Says Server B \<lbrace>Nonce M, Crypt K' \<lbrace>X, Nonce Nb, K\<rbrace>\<rbrace> \<in> set evs  
121     \<Longrightarrow> K \<in> parts (knows Spy evs)"
122by blast
123
124lemmas OR2_parts_knows_Spy =
125    OR2_analz_knows_Spy [THEN analz_into_parts]
126
127ML
128\<open>
129fun parts_explicit_tac ctxt i =
130    forward_tac ctxt [@{thm Oops_parts_knows_Spy}] (i+7) THEN
131    forward_tac ctxt [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
132    forward_tac ctxt [@{thm OR2_parts_knows_Spy}]  (i+4)
133\<close>
134 
135method_setup parts_explicit = \<open>
136    Scan.succeed (SIMPLE_METHOD' o parts_explicit_tac)\<close>
137  "to explicitly state that some message components belong to parts knows Spy"
138
139
140lemma Spy_see_shrK [simp]: 
141    "evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
142by (erule orb.induct, parts_explicit, simp_all, blast+)
143
144lemma Spy_analz_shrK [simp]: 
145"evs \<in> orb \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
146by auto
147
148lemma Spy_see_shrK_D [dest!]:
149     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
150by (blast dest: Spy_see_shrK)
151
152lemma new_keys_not_used [simp]:
153   "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> orb\<rbrakk>  \<Longrightarrow> K \<notin> keysFor (parts (knows Spy evs))"
154apply (erule rev_mp)
155apply (erule orb.induct, parts_explicit, simp_all)
156apply (force dest!: keysFor_parts_insert)
157apply (blast+)
158done
159
160
161
162subsection\<open>Proofs involving analz\<close>
163
164text\<open>Describes the form of K and NA when the Server sends this message.  Also
165  for Oops case.\<close>
166lemma Says_Server_message_form: 
167"\<lbrakk>Says Server B  \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
168     evs \<in> orb\<rbrakk>                                            
169 \<Longrightarrow> K \<notin> range shrK \<and> (\<exists> A Na. X=(Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
170by (erule rev_mp, erule orb.induct, simp_all)
171
172lemma Says_Server_imp_Gets: 
173 "\<lbrakk>Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
174                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;
175    evs \<in> orb\<rbrakk>
176  \<Longrightarrow>  Gets Server \<lbrace>Nonce M, Agent A, Agent B, 
177                   Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>, 
178               Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace>
179         \<in> set evs"
180by (erule rev_mp, erule orb.induct, simp_all)
181
182
183lemma A_trusts_OR1: 
184"\<lbrakk>Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs);  
185    A \<notin> bad; evs \<in> orb\<rbrakk>                   
186 \<Longrightarrow> Says A B \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs"
187apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
188apply (blast)
189done
190
191
192lemma B_trusts_OR2:
193 "\<lbrakk>Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>  
194      \<in> parts (knows Spy evs);  B \<notin> bad; evs \<in> orb\<rbrakk>                   
195  \<Longrightarrow> (\<exists> X. Says B Server \<lbrace>Nonce M, Agent A, Agent B, X,  
196              Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> 
197          \<in> set evs)"
198apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
199apply (blast+)
200done
201
202
203lemma B_trusts_OR3: 
204"\<lbrakk>Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace> \<in> parts (knows Spy evs);  
205   B \<notin> bad; evs \<in> orb\<rbrakk>                   
206\<Longrightarrow> \<exists> M. Says Server B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> 
207         \<in> set evs"
208apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
209apply (blast+)
210done
211
212lemma Gets_Server_message_form: 
213"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs;  
214    evs \<in> orb\<rbrakk>                                              
215 \<Longrightarrow> (K \<notin> range shrK \<and> (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>)))    
216             | X \<in> analz (knows Spy evs)"
217by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
218          Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)
219
220lemma unique_Na: "\<lbrakk>Says A B  \<lbrace>Nonce M, Agent A, Agent B, Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
221         Says A B' \<lbrace>Nonce M', Agent A, Agent B', Crypt (shrK A) \<lbrace>Nonce Na, Nonce M', Agent A, Agent B'\<rbrace>\<rbrace> \<in> set evs;  
222    A \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow> B=B' \<and> M=M'"
223by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
224
225lemma unique_Nb: "\<lbrakk>Says B Server \<lbrace>Nonce M, Agent A, Agent B, X, Crypt (shrK B) \<lbrace>Nonce Nb, Nonce M, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs;   
226         Says B Server \<lbrace>Nonce M', Agent A', Agent B, X', Crypt (shrK B) \<lbrace>Nonce Nb,Nonce M', Nonce M', Agent A', Agent B\<rbrace>\<rbrace> \<in> set evs;   
227    B \<notin> bad; evs \<in> orb\<rbrakk> \<Longrightarrow>   M=M' \<and> A=A' \<and> X=X'"
228by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)
229
230lemma analz_image_freshCryptK_lemma:
231"(Crypt K X \<in> analz (Key`nE \<union> H)) \<longrightarrow> (Crypt K X \<in> analz H) \<Longrightarrow>  
232        (Crypt K X \<in> analz (Key`nE \<union> H)) = (Crypt K X \<in> analz H)"
233by (blast intro: analz_mono [THEN [2] rev_subsetD])
234
235ML
236\<open>
237structure OtwayReesBella =
238struct
239
240val analz_image_freshK_ss =
241  simpset_of
242   (\<^context> delsimps [image_insert, image_Un]
243      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
244      addsimps @{thms analz_image_freshK_simps})
245
246end
247\<close>
248
249method_setup analz_freshCryptK = \<open>
250    Scan.succeed (fn ctxt =>
251     (SIMPLE_METHOD
252      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
253          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}),
254          ALLGOALS (asm_simp_tac
255            (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))])))\<close>
256  "for proving useful rewrite rule"
257
258
259method_setup disentangle = \<open>
260    Scan.succeed
261     (fn ctxt => SIMPLE_METHOD
262      (REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE, disjE] 
263                   ORELSE' hyp_subst_tac ctxt)))\<close>
264  "for eliminating conjunctions, disjunctions and the like"
265
266
267
268lemma analz_image_freshCryptK [rule_format]: 
269"evs \<in> orb \<Longrightarrow>                              
270     Key K \<notin> analz (knows Spy evs) \<longrightarrow>  
271       (\<forall> KK. KK \<subseteq> - (range shrK) \<longrightarrow>                  
272             (Crypt K X \<in> analz (Key`KK \<union> (knows Spy evs))) =   
273             (Crypt K X \<in> analz (knows Spy evs)))"
274apply (erule orb.induct)
275apply (analz_mono_contra)
276apply (frule_tac [7] Gets_Server_message_form)
277apply (frule_tac [9] Says_Server_message_form)
278apply disentangle
279apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
280prefer 8 apply clarify
281apply (analz_freshCryptK, spy_analz, fastforce)
282done
283
284
285
286lemma analz_insert_freshCryptK: 
287"\<lbrakk>evs \<in> orb;  Key K \<notin> analz (knows Spy evs);  
288         Seskey \<notin> range shrK\<rbrakk> \<Longrightarrow>   
289         (Crypt K X \<in> analz (insert (Key Seskey) (knows Spy evs))) =  
290         (Crypt K X \<in> analz (knows Spy evs))"
291by (simp only: analz_image_freshCryptK analz_image_freshK_simps)
292
293
294lemma analz_hard: 
295"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
296             Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
297   Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace> \<in> analz (knows Spy evs);  
298   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>                   
299 \<Longrightarrow>  Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs"
300apply (erule rev_mp)
301apply (erule rev_mp)
302apply (erule orb.induct)
303apply (frule_tac [7] Gets_Server_message_form)
304apply (frule_tac [9] Says_Server_message_form)
305apply disentangle
306txt\<open>letting the simplifier solve OR2\<close>
307apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
308apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
309apply (spy_analz)
310txt\<open>OR1\<close>
311apply blast
312txt\<open>Oops\<close>
313prefer 4 apply (blast dest: analz_insert_freshCryptK)
314txt\<open>OR4 - ii\<close>
315prefer 3 apply (blast)
316txt\<open>OR3\<close>
317(*adding Gets_imp_ and Says_imp_ for efficiency*)
318apply (blast dest: 
319       A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
320txt\<open>OR4 - i\<close>
321apply clarify
322apply (simp add: pushes split_ifs)
323apply (case_tac "Aaa\<in>bad")
324apply (blast dest: analz_insert_freshCryptK)
325apply clarify
326apply simp
327apply (case_tac "Ba\<in>bad")
328apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
329apply (simp (no_asm_simp))
330apply clarify
331apply (frule Gets_imp_knows_Spy 
332             [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
333       assumption, assumption, assumption, erule exE)
334apply (frule Says_Server_imp_Gets 
335            [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
336            THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
337       assumption, assumption, assumption, assumption)
338apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
339done
340
341
342lemma Gets_Server_message_form': 
343"\<lbrakk>Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>X, Nonce Nb, Key K\<rbrace>\<rbrace>  \<in> set evs;  
344   B \<notin> bad; evs \<in> orb\<rbrakk>                              
345  \<Longrightarrow> K \<notin> range shrK \<and> (\<exists> A Na. X = (Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>))"
346by (blast dest!: B_trusts_OR3 Says_Server_message_form)
347
348
349lemma OR4_imp_Gets: 
350"\<lbrakk>Says B A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;   
351   B \<notin> bad; evs \<in> orb\<rbrakk>  
352 \<Longrightarrow> (\<exists> Nb. Gets B \<lbrace>Nonce M, Crypt (shrK B) \<lbrace>Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>,
353                                             Nonce Nb, Key K\<rbrace>\<rbrace> \<in> set evs)"
354apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
355prefer 3 apply (blast dest: Gets_Server_message_form')
356apply blast+
357done
358
359
360lemma A_keydist_to_B: 
361"\<lbrakk>Says A B \<lbrace>Nonce M, Agent A, Agent B,  
362            Crypt (shrK A) \<lbrace>Nonce Na, Nonce M, Agent A, Agent B\<rbrace>\<rbrace> \<in>set evs; 
363   Gets A \<lbrace>Nonce M, Crypt (shrK A) \<lbrace>Nonce Na, Key K\<rbrace>\<rbrace> \<in> set evs;    
364   A \<notin> bad; B \<notin> bad; evs \<in> orb\<rbrakk>  
365  \<Longrightarrow> Key K \<in> analz (knows B evs)"
366apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
367apply (drule analz_hard, assumption, assumption, assumption, assumption)
368apply (drule OR4_imp_Gets, assumption, assumption)
369apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
370done
371
372
373text\<open>Other properties as for the original protocol\<close>
374
375
376end
377