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