Correction of protocol; addition of Reveal message; proofs of
authorpaulson
Mon Sep 23 18:21:31 1996 +0200 (1996-09-23)
changeset 20145be4c8ca7b25
parent 2013 4b7a432fb3ed
child 2015 d4a8fd8a8065
Correction of protocol; addition of Reveal message; proofs of
correctness in its presence
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 23 18:20:43 1996 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 23 18:21:31 1996 +0200
     1.3 @@ -5,30 +5,42 @@
     1.4  
     1.5  Inductive relation "otway" for the Otway-Rees protocol.
     1.6  
     1.7 +Version that encrypts Nonce NB
     1.8 +
     1.9  From page 244 of
    1.10    Burrows, Abadi and Needham.  A Logic of Authentication.
    1.11    Proc. Royal Soc. 426 (1989)
    1.12  *)
    1.13  
    1.14 +
    1.15 +(*MAY DELETE**)
    1.16 +Delsimps [parts_insert_sees];
    1.17 +AddIffs [le_refl];
    1.18 +val disj_cong = 
    1.19 +  let val th = prove_goal HOL.thy 
    1.20 +                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
    1.21 +		(fn _=> [fast_tac HOL_cs 1])
    1.22 +  in  standard (impI RSN (2, th RS mp RS mp))  end;
    1.23 +
    1.24 +
    1.25  open OtwayRees;
    1.26  
    1.27  proof_timing:=true;
    1.28  HOL_quantifiers := false;
    1.29  
    1.30  
    1.31 -(** Weak liveness: there are traces that reach the end **)
    1.32 -
    1.33 +(*Weak liveness: there are traces that reach the end*)
    1.34  goal thy 
    1.35   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.36 -\        ==> EX K. EX evs: otway.          \
    1.37 -\               Says A B (Crypt (Agent A) K) : set_of_list evs";
    1.38 +\        ==> EX K. EX NA. EX evs: otway.          \
    1.39 +\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    1.40 +\                 : set_of_list evs";
    1.41  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.42 -br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4 RS 
    1.43 -    otway.OR5) 2;
    1.44 +br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    1.45  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.46  by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.47  by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.48 -qed "weak_liveness";
    1.49 +result();
    1.50  
    1.51  
    1.52  (**** Inductive proofs about otway ****)
    1.53 @@ -51,13 +63,6 @@
    1.54  Addsimps [not_Says_to_self];
    1.55  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.56  
    1.57 -goal thy "!!evs. evs : otway ==> Notes A X ~: set_of_list evs";
    1.58 -be otway.induct 1;
    1.59 -by (Auto_tac());
    1.60 -qed "not_Notes";
    1.61 -Addsimps [not_Notes];
    1.62 -AddSEs   [not_Notes RSN (2, rev_notE)];
    1.63 -
    1.64  
    1.65  (** For reasoning about the encrypted portion of messages **)
    1.66  
    1.67 @@ -75,26 +80,28 @@
    1.68  \                K : parts (sees Enemy evs)";
    1.69  by (fast_tac (!claset addSEs partsEs
    1.70  	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.71 -qed "OR5_parts_sees_Enemy";
    1.72 +qed "Reveal_parts_sees_Enemy";
    1.73  
    1.74  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.75    argument as for the Fake case.  This is possible for most, but not all,
    1.76    proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.77    messages originate from the Enemy. *)
    1.78  
    1.79 -val OR2_OR4_tac = 
    1.80 -    dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    1.81 -    dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    1.82 +val parts_Fake_tac = 
    1.83 +    forward_tac [OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 4 THEN
    1.84 +    forward_tac [OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 6 THEN
    1.85 +    forward_tac [Reveal_parts_sees_Enemy] 7;
    1.86  
    1.87  
    1.88 -(*** Shared keys are not betrayed ***)
    1.89 +(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    1.90 +    sends messages containing X! **)
    1.91  
    1.92  (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.93  goal thy 
    1.94   "!!evs. [| evs : otway;  A ~: bad |]    \
    1.95  \        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.96  be otway.induct 1;
    1.97 -by OR2_OR4_tac;
    1.98 +by parts_Fake_tac;
    1.99  by (Auto_tac());
   1.100  (*Deals with Fake message*)
   1.101  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.102 @@ -131,13 +138,12 @@
   1.103    This has to be proved anew for each protocol description,
   1.104    but should go by similar reasoning every time.  Hardest case is the
   1.105    standard Fake rule.  
   1.106 -      The length comparison, and Union over C, are essential for the 
   1.107 -  induction! *)
   1.108 +      The Union over C is essential for the induction! *)
   1.109  goal thy "!!evs. evs : otway ==> \
   1.110  \                length evs <= length evs' --> \
   1.111  \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.112  be otway.induct 1;
   1.113 -by OR2_OR4_tac;
   1.114 +by parts_Fake_tac;
   1.115  (*auto_tac does not work here, as it performs safe_tac first*)
   1.116  by (ALLGOALS Asm_simp_tac);
   1.117  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.118 @@ -161,19 +167,58 @@
   1.119  \           evs : otway                 \
   1.120  \        |] ==> length evt < length evs";
   1.121  br ccontr 1;
   1.122 +bd leI 1;
   1.123  by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.124 -	              addIs [impOfSubs parts_mono, leI]) 1);
   1.125 +                      addIs  [impOfSubs parts_mono]) 1);
   1.126  qed "Says_imp_old_keys";
   1.127  
   1.128  
   1.129 +(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   1.130 +
   1.131 +goal thy "!!evs. evs : otway ==> \
   1.132 +\                length evs <= length evt --> \
   1.133 +\                          Nonce (newN evt) ~: (UN C. parts (sees C evs))";
   1.134 +be otway.induct 1;
   1.135 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.136 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ parts_insert2]
   1.137 +                                     addcongs [disj_cong])));
   1.138 +by (REPEAT_FIRST (fast_tac (!claset 
   1.139 +			      addSEs partsEs
   1.140 +			      addSDs  [Says_imp_sees_Enemy RS parts.Inj]
   1.141 +			      addDs  [impOfSubs analz_subset_parts,
   1.142 +				      impOfSubs parts_insert_subset_Un,
   1.143 +				      Suc_leD]
   1.144 +			      addss (!simpset))));
   1.145 +val lemma = result();
   1.146 +
   1.147 +(*Variant needed for the main theorem below*)
   1.148 +goal thy 
   1.149 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.150 +\        ==> Nonce (newN evs') ~: parts (sees C evs)";
   1.151 +by (fast_tac (!claset addDs [lemma]) 1);
   1.152 +qed "new_nonces_not_seen";
   1.153 +Addsimps [new_nonces_not_seen];
   1.154 +
   1.155 +(*Another variant: old messages must contain old nonces!*)
   1.156 +goal thy 
   1.157 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.158 +\           Nonce (newN evt) : parts {X};    \
   1.159 +\           evs : otway                 \
   1.160 +\        |] ==> length evt < length evs";
   1.161 +br ccontr 1;
   1.162 +bd leI 1;
   1.163 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   1.164 +	              addIs  [impOfSubs parts_mono]) 1);
   1.165 +qed "Says_imp_old_nonces";
   1.166 +
   1.167 +
   1.168  (*Nobody can have USED keys that will be generated in the future.
   1.169    ...very like new_keys_not_seen*)
   1.170  goal thy "!!evs. evs : otway ==> \
   1.171  \                length evs <= length evs' --> \
   1.172  \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.173  be otway.induct 1;
   1.174 -by OR2_OR4_tac;
   1.175 -bd OR5_parts_sees_Enemy 7;
   1.176 +by parts_Fake_tac;
   1.177  by (ALLGOALS Asm_simp_tac);
   1.178  (*OR1 and OR3*)
   1.179  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   1.180 @@ -187,7 +232,7 @@
   1.181  	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.182  	       addss (!simpset)))
   1.183       [3,2,1]));
   1.184 -(*OR5: dummy message*)
   1.185 +(*Reveal: dummy message*)
   1.186  by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.187  		      addIs  [less_SucI, impOfSubs keysFor_mono]
   1.188  		      addss (!simpset addsimps [le_def])) 1);
   1.189 @@ -228,14 +273,14 @@
   1.190  \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.191  \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.192  be otway.induct 1;
   1.193 -by OR2_OR4_tac;
   1.194 +by parts_Fake_tac;
   1.195  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.196  (*Deals with Faked messages*)
   1.197  by (best_tac (!claset addSEs partsEs
   1.198  		      addDs [impOfSubs analz_subset_parts,
   1.199                               impOfSubs parts_insert_subset_Un]
   1.200                        addss (!simpset)) 2);
   1.201 -(*Base case and OR5*)
   1.202 +(*Base case and Reveal*)
   1.203  by (Auto_tac());
   1.204  result();
   1.205  
   1.206 @@ -273,6 +318,40 @@
   1.207  
   1.208  (** Session keys are not used to encrypt other session keys **)
   1.209  
   1.210 +(*Describes the form of Key K when the following message is sent.  The use of
   1.211 +  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.212 +  assumptions on A are needed to prevent its being a Faked message.  (Based
   1.213 +  on NS_Shared/Says_S_message_form) *)
   1.214 +goal thy
   1.215 + "!!evs. evs: otway ==>                                           \
   1.216 +\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   1.217 +\          A ~: bad -->                                           \
   1.218 +\        (EX evt:otway. K = newK evt)";
   1.219 +be otway.induct 1;
   1.220 +by parts_Fake_tac;
   1.221 +by (Auto_tac());
   1.222 +(*Deals with Fake message*)
   1.223 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.224 +			     impOfSubs Fake_parts_insert]) 1);
   1.225 +val lemma = result() RS mp;
   1.226 +
   1.227 +
   1.228 +(*EITHER describes the form of Key K when the following message is sent, 
   1.229 +  OR     reduces it to the Fake case.*)
   1.230 +goal thy 
   1.231 + "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   1.232 +\           evs : otway |]                      \
   1.233 +\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   1.234 +by (excluded_middle_tac "A : bad" 1);
   1.235 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   1.236 +	              addss (!simpset)) 2);
   1.237 +by (forward_tac [lemma] 1);
   1.238 +by (fast_tac (!claset addEs  partsEs
   1.239 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.240 +by (Fast_tac 1);
   1.241 +qed "Reveal_message_form";
   1.242 +
   1.243 +
   1.244  (*Lemma for the trivial direction of the if-and-only-if*)
   1.245  goal thy  
   1.246   "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   1.247 @@ -282,6 +361,7 @@
   1.248  val lemma = result();
   1.249  
   1.250  
   1.251 +(*The equality makes the induction hypothesis easier to apply*)
   1.252  goal thy  
   1.253   "!!evs. evs : otway ==> \
   1.254  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.255 @@ -289,18 +369,19 @@
   1.256  be otway.induct 1;
   1.257  bd OR2_analz_sees_Enemy 4;
   1.258  bd OR4_analz_sees_Enemy 6;
   1.259 -by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.260 -by (ALLGOALS (*Takes 35 secs*)
   1.261 +bd Reveal_message_form 7;
   1.262 +by (REPEAT_FIRST (ares_tac [allI, lemma]));
   1.263 +by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.264 +by (ALLGOALS (*Takes 28 secs*)
   1.265      (asm_simp_tac 
   1.266       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.267  			 @ pushes)
   1.268                 setloop split_tac [expand_if])));
   1.269 -(*OR4, OR2, Fake*) 
   1.270 -by (EVERY (map enemy_analz_tac [5,3,2]));
   1.271 -(*OR3*)
   1.272 -by (Fast_tac 2);
   1.273 -(*Base case*) 
   1.274 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.275 +(** LEVEL 7 **)
   1.276 +(*Reveal case 2, OR4, OR2, Fake*) 
   1.277 +by (EVERY (map enemy_analz_tac [7,5,3,2]));
   1.278 +(*Reveal case 1, OR3, Base*)
   1.279 +by (Auto_tac());
   1.280  qed_spec_mp "analz_image_newK";
   1.281  
   1.282  
   1.283 @@ -314,14 +395,235 @@
   1.284  qed "analz_insert_Key_newK";
   1.285  
   1.286  
   1.287 -(*Describes the form *and age* of K when the following message is sent*)
   1.288 +(** The Key K uniquely identifies the Server's  message. **)
   1.289 +
   1.290 +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.291 +
   1.292 +goal thy 
   1.293 + "!!evs. evs : otway ==>                      \
   1.294 +\      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.295 +\       Says Server B \
   1.296 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.297 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   1.298 +\       A=A' & B=B' & NA=NA' & NB=NB'";
   1.299 +be otway.induct 1;
   1.300 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.301 +by (Step_tac 1);
   1.302 +(*Remaining cases: OR3 and OR4*)
   1.303 +by (ex_strip_tac 2);
   1.304 +by (Fast_tac 2);
   1.305 +by (excluded_middle_tac "K = Key(newK evsa)" 1);
   1.306 +by (Asm_simp_tac 1);
   1.307 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   1.308 +(*...we assume X is a very new message, and handle this case by contradiction*)
   1.309 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.310 +	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.311 +	              addss (!simpset addsimps [parts_insertI])) 1);
   1.312 +val lemma = result();
   1.313 +
   1.314 +goal thy 
   1.315 + "!!evs. [| Says Server B                                          \
   1.316 +\              {|NA, Crypt {|NA, K|} (shrK A),                     \
   1.317 +\                    Crypt {|NB, K|} (shrK B)|}                    \
   1.318 +\            : set_of_list evs;                                    \ 
   1.319 +\           Says Server B'                                         \
   1.320 +\              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   1.321 +\                     Crypt {|NB', K|} (shrK B')|}                 \
   1.322 +\            : set_of_list evs;                                    \
   1.323 +\           evs : otway |]                                         \
   1.324 +\        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.325 +bd lemma 1;
   1.326 +by (REPEAT (etac exE 1));
   1.327 +(*Duplicate the assumption*)
   1.328 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.329 +by (fast_tac (!claset addSDs [spec]) 1);
   1.330 +qed "unique_session_keys";
   1.331 +
   1.332 +
   1.333 +
   1.334 +(**** Towards proving stronger authenticity properties ****)
   1.335 +
   1.336 +(*Only OR1 can have caused such a part of a message to appear.*)
   1.337 +goal thy 
   1.338 + "!!evs. [| A ~: bad;  evs : otway |]               \
   1.339 +\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   1.340 +\             : parts (sees Enemy evs) -->                  \
   1.341 +\            Says A B {|NA, Agent A, Agent B,               \
   1.342 +\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   1.343 +\             : set_of_list evs";
   1.344 +be otway.induct 1;
   1.345 +by parts_Fake_tac;
   1.346 +by (ALLGOALS Asm_simp_tac);
   1.347 +(*Fake*)
   1.348 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.349 +			      impOfSubs Fake_parts_insert]) 2);
   1.350 +by (Auto_tac());
   1.351 +qed_spec_mp "Crypt_imp_OR1";
   1.352 +
   1.353 +
   1.354 +(** The Nonce NA uniquely identifies A's  message. **)
   1.355 +
   1.356 +goal thy 
   1.357 + "!!evs. [| evs : otway; A ~: bad |]               \
   1.358 +\ ==> EX B'. ALL B.    \
   1.359 +\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs) --> \
   1.360 +\        B = B'";
   1.361 +be otway.induct 1;
   1.362 +by parts_Fake_tac;
   1.363 +by (ALLGOALS Asm_simp_tac);
   1.364 +(*Fake*)
   1.365 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.366 +			      impOfSubs Fake_parts_insert]) 2);
   1.367 +(*Base case*)
   1.368 +by (fast_tac (!claset addss (!simpset)) 1);
   1.369 +by (Step_tac 1);
   1.370 +(*OR1: creation of new Nonce*)
   1.371 +by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
   1.372 +by (Asm_simp_tac 1);
   1.373 +by (Fast_tac 1);
   1.374 +by (best_tac (!claset addSEs partsEs
   1.375 +	              addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   1.376 +val lemma = result();
   1.377 +
   1.378 +goal thy 
   1.379 + "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs); \ 
   1.380 +\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees Enemy evs); \ 
   1.381 +\          evs : otway;  A ~: bad |]                                         \
   1.382 +\        ==> B = C";
   1.383 +bd lemma 1;
   1.384 +ba 1;
   1.385 +by (etac exE 1);
   1.386 +(*Duplicate the assumption*)
   1.387 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.388 +by (fast_tac (!claset addSDs [spec]) 1);
   1.389 +qed "unique_OR1_nonce";
   1.390 +
   1.391 +
   1.392 +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   1.393 +
   1.394 +(*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   1.395 +  OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   1.396 +  over-simplified version of this protocol: see OtwayRees_Bad.*)
   1.397 +goal thy 
   1.398 + "!!evs. [| A ~: bad;  evs : otway |]                            \
   1.399 +\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
   1.400 +\             : parts (sees Enemy evs) -->                       \
   1.401 +\            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
   1.402 +\             ~: parts (sees Enemy evs)";
   1.403 +be otway.induct 1;
   1.404 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
   1.405 +(*It is hard to generate this proof in a reasonable amount of time*)
   1.406 +by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
   1.407 +                      addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.408 +by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
   1.409 +			    addSDs  [impOfSubs analz_subset_parts,
   1.410 +				     impOfSubs parts_insert_subset_Un]
   1.411 +			    addss  (!simpset))));
   1.412 +by (REPEAT_FIRST (fast_tac (!claset 
   1.413 +			      addSEs (partsEs@[nonce_not_seen_now])
   1.414 +                              addSDs  [impOfSubs analz_subset_parts,
   1.415 +                                      impOfSubs parts_insert_subset_Un]
   1.416 +                              addss (!simpset))));
   1.417 +qed_spec_mp"no_nonce_OR1_OR2";
   1.418 +
   1.419 +
   1.420 +
   1.421 +(*If the encrypted message appears, and A has used Nonce NA to start a run,
   1.422 +  then it originated with the Server!*)
   1.423 +goal thy 
   1.424 + "!!evs. [| A ~: bad;  evs : otway |]                                 \
   1.425 +\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   1.426 +\            Says A B {|Nonce NA, Agent A, Agent B,  \
   1.427 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   1.428 +\             : set_of_list evs --> \
   1.429 +\            (EX NB. Says Server B               \
   1.430 +\                 {|Nonce NA,               \
   1.431 +\                   Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.432 +\                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.433 +\                   : set_of_list evs)";
   1.434 +be otway.induct 1;
   1.435 +by parts_Fake_tac;
   1.436 +by (ALLGOALS Asm_simp_tac);
   1.437 +(*Fake*)
   1.438 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.439 +			      impOfSubs Fake_parts_insert]) 1);
   1.440 +(*OR1: it cannot be a new Nonce, contradiction.*)
   1.441 +by (fast_tac (!claset addSIs [parts_insertI]
   1.442 +		      addSEs partsEs
   1.443 +		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.444 +	              addss (!simpset)) 1);
   1.445 +(*OR3 and OR4*)  (** LEVEL 5 **)
   1.446 +(*OR4*)
   1.447 +by (REPEAT (Safe_step_tac 2));
   1.448 +by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   1.449 +by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.450 +		      addEs  partsEs
   1.451 +	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 2);
   1.452 +(*OR3*)  (** LEVEL 8 **)
   1.453 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.454 +by (step_tac (!claset delrules [disjCI, impCE]) 1);
   1.455 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]
   1.456 +                      addSEs [MPair_parts]
   1.457 +                      addEs  [unique_OR1_nonce]) 1);
   1.458 +by (fast_tac (!claset addSEs [MPair_parts]
   1.459 +                      addSDs [Says_imp_sees_Enemy RS parts.Inj]
   1.460 +                      addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   1.461 +	              delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   1.462 +qed_spec_mp "Crypt_imp_Server_msg";
   1.463 +
   1.464 +
   1.465 +(*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   1.466 +  then the key really did come from the Server!  CANNOT prove this of the
   1.467 +  bad form of this protocol, even though we can prove
   1.468 +  Enemy_not_see_encrypted_key*)
   1.469 +goal thy 
   1.470 + "!!evs. [| A ~: bad;  evs : otway |]                                    \
   1.471 +\        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
   1.472 +\             : set_of_list evs -->                                      \
   1.473 +\            Says A B {|Nonce NA, Agent A, Agent B,                      \
   1.474 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   1.475 +\             : set_of_list evs -->                                      \
   1.476 +\            (EX NB. Says Server B                                       \
   1.477 +\                     {|Nonce NA,                                        \
   1.478 +\                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.479 +\                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.480 +\                       : set_of_list evs)";
   1.481 +be otway.induct 1;
   1.482 +by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.483 +(*OR2*)
   1.484 +by (Fast_tac 3);
   1.485 +(*OR1: it cannot be a new Nonce, contradiction.*)
   1.486 +by (fast_tac (!claset addSIs [parts_insertI]
   1.487 +		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.488 +	              addss (!simpset)) 2);
   1.489 +(*Fake, OR4*) (** LEVEL 4 **)
   1.490 +by (step_tac (!claset delrules [impCE]) 1);
   1.491 +by (ALLGOALS Asm_simp_tac);
   1.492 +by (Fast_tac 4);
   1.493 +by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   1.494 +		      addEs  partsEs
   1.495 +	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 3);
   1.496 +(** LEVEL 8 **)
   1.497 +(*Still subcases of Fake and OR4*)
   1.498 +by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.499 +	              addDs  [impOfSubs analz_subset_parts]) 1);
   1.500 +by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   1.501 +	              addEs  partsEs
   1.502 +	              addDs  [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.503 +val lemma = result();
   1.504 +
   1.505 +val OR4_imp_Says_Server_A = 
   1.506 +    lemma RSN (2, rev_mp) RS mp |> standard;
   1.507 +
   1.508 +
   1.509 +
   1.510 +(*Describes the form of K and NA when the Server sends this message.*)
   1.511  goal thy 
   1.512   "!!evs. [| Says Server B \
   1.513  \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.514  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.515  \           evs : otway |]                                        \
   1.516 -\        ==> (EX evt:otway. K = Key(newK evt) & \
   1.517 -\                           length evt < length evs) &            \
   1.518 +\        ==> (EX evt:otway. K = Key(newK evt)) &                  \
   1.519  \            (EX i. NA = Nonce i)";
   1.520  be rev_mp 1;
   1.521  be otway.induct 1;
   1.522 @@ -329,31 +631,52 @@
   1.523  qed "Says_Server_message_form";
   1.524  
   1.525  
   1.526 -(*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*)
   1.527 +(** Crucial secrecy property: Enemy does not see the keys sent in msg OR3 **)
   1.528 +
   1.529  goal thy 
   1.530 - "!!evs. [| Says Server A \
   1.531 -\            {|NA, Crypt {|NA, K|} (shrK B),                      \
   1.532 -\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   1.533 -\           A ~: bad;  B ~: bad;  evs : otway |] ==>              \
   1.534 -\     K ~: analz (sees Enemy evs)";
   1.535 -be rev_mp 1;
   1.536 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]         \
   1.537 +\        ==> Says Server B                                             \
   1.538 +\              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   1.539 +\                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   1.540 +\            Says A Enemy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   1.541 +\            Key(newK evt) ~: analz (sees Enemy evs)";
   1.542  be otway.induct 1;
   1.543  bd OR2_analz_sees_Enemy 4;
   1.544  bd OR4_analz_sees_Enemy 6;
   1.545 -by (ALLGOALS Asm_simp_tac);
   1.546 -(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.547 -by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.548 -by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.549 -by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   1.550 +by (forward_tac [Reveal_message_form] 7);
   1.551 +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.552  by (ALLGOALS
   1.553      (asm_full_simp_tac 
   1.554       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.555  			  analz_insert_Key_newK] @ pushes)
   1.556                 setloop split_tac [expand_if])));
   1.557 -(*OR4, OR2, Fake*) 
   1.558 -by (EVERY (map enemy_analz_tac [4,2,1]));
   1.559 +(** LEVEL 6 **)
   1.560  (*OR3*)
   1.561 -by (fast_tac (!claset addSEs [less_irrefl]) 1);
   1.562 +by (fast_tac (!claset addSIs [parts_insertI]
   1.563 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.564 +	              addss (!simpset)) 3);
   1.565 +(*Reveal case 2, OR4, OR2, Fake*) 
   1.566 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' enemy_analz_tac));
   1.567 +(*Reveal case 1*) (** LEVEL 8 **)
   1.568 +by (excluded_middle_tac "Aa : bad" 1);
   1.569 +(*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
   1.570 +bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   1.571 +by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   1.572 +(*So now we have  Aa ~: bad *)
   1.573 +by (dresolve_tac [OR4_imp_Says_Server_A] 1);
   1.574 +by (REPEAT (assume_tac 1));
   1.575 +by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.576 +val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.577 +
   1.578 +goal thy 
   1.579 + "!!evs. [| Says Server B \
   1.580 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.581 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.582 +\           Says A Enemy {|NA, K|} ~: set_of_list evs;            \
   1.583 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.584 +\        ==> K ~: analz (sees Enemy evs)";
   1.585 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.586 +by (fast_tac (!claset addSEs [lemma]) 1);
   1.587  qed "Enemy_not_see_encrypted_key";
   1.588  
   1.589  
   1.590 @@ -380,8 +703,6 @@
   1.591  by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.592  qed "Crypt_parts_singleton";
   1.593  
   1.594 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.595 -
   1.596  (*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.597    C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.598  goal thy 
   1.599 @@ -407,7 +728,7 @@
   1.600  by (Asm_simp_tac 3);
   1.601  by (REPEAT (ares_tac [exI] 3));
   1.602  (*...we prove this case by contradiction: the key is too new!*)
   1.603 -by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.604 +by (fast_tac (!claset addIs [parts_insertI]
   1.605  		      addSEs partsEs
   1.606  		      addEs [Says_imp_old_keys RS less_irrefl]
   1.607  	              addss (!simpset)) 3);
   1.608 @@ -421,6 +742,5 @@
   1.609  (*Fake*) (** LEVEL 16 **)
   1.610  by (ex_strip_tac 1);
   1.611  by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.612 -qed "unique_session_keys";
   1.613 +qed "key_identifies_senders";
   1.614  
   1.615 -(*It seems strange but this theorem is NOT needed to prove the main result!*)
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Mon Sep 23 18:20:43 1996 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Mon Sep 23 18:21:31 1996 +0200
     2.3 @@ -5,6 +5,8 @@
     2.4  
     2.5  Inductive relation "otway" for the Otway-Rees protocol.
     2.6  
     2.7 +Version that encrypts Nonce NB
     2.8 +
     2.9  From page 244 of
    2.10    Burrows, Abadi and Needham.  A Logic of Authentication.
    2.11    Proc. Royal Soc. 426 (1989)
    2.12 @@ -25,10 +27,10 @@
    2.13            ==> Says Enemy B X  # evs : otway"
    2.14  
    2.15           (*Alice initiates a protocol run*)
    2.16 -    OR1  "[| evs: otway;  A ~= B |]
    2.17 +    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    2.18            ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    2.19 -                            Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    2.20 -                                  (shrK A) |} 
    2.21 +                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    2.22 +                               (shrK A) |} 
    2.23                   # evs : otway"
    2.24  
    2.25           (*Bob's response to Alice's message.  Bob doesn't know who 
    2.26 @@ -37,8 +39,9 @@
    2.27      OR2  "[| evs: otway;  B ~= Server;
    2.28               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.29            ==> Says B Server 
    2.30 -                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    2.31 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.32 +                  {|Nonce NA, Agent A, Agent B, X, 
    2.33 +                    Crypt {|Nonce NA, Nonce (newN evs), 
    2.34 +                            Agent A, Agent B|} (shrK B)|}
    2.35                   # evs : otway"
    2.36  
    2.37           (*The Server receives Bob's message and checks that the three NAs
    2.38 @@ -48,8 +51,7 @@
    2.39               Says B' Server 
    2.40                    {|Nonce NA, Agent A, Agent B, 
    2.41                      Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    2.42 -                    Nonce NB, 
    2.43 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.44 +                    Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|}
    2.45                 : set_of_list evs |]
    2.46            ==> Says Server B 
    2.47                    {|Nonce NA, 
    2.48 @@ -59,19 +61,23 @@
    2.49  
    2.50           (*Bob receives the Server's (?) message and compares the Nonces with
    2.51  	   those in the message he previously sent the Server.*)
    2.52 -    OR4  "[| evs: otway;  A ~= B;  
    2.53 +    OR4  "[| evs: otway;  A ~= B;  B ~= Server;
    2.54               Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.55                 : set_of_list evs;
    2.56 -             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    2.57 +             Says B Server {|Nonce NA, Agent A, Agent B, X', 
    2.58 +                             Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} 
    2.59 +                                   (shrK B)|}
    2.60                 : set_of_list evs |]
    2.61 -          ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    2.62 +          ==> Says B A {|Nonce NA, X|} # evs : otway"
    2.63  
    2.64 -         (*Alice checks her Nonce, then sends a dummy message to Bob,
    2.65 -           using the new session key.*)
    2.66 -    OR5  "[| evs: otway;  
    2.67 -             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.68 -               : set_of_list evs;
    2.69 -             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.70 -          ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    2.71 +         (*This message models possible leaks of session keys.  Alice's Nonce
    2.72 +           identifies the protocol run.*)
    2.73 +    Reveal "[| evs: otway;  A ~= Enemy;
    2.74 +               Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.75 +                 : set_of_list evs;
    2.76 +               Says A  B {|Nonce NA, Agent A, Agent B, 
    2.77 +                           Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    2.78 +                 : set_of_list evs |]
    2.79 +            ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
    2.80  
    2.81  end