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