src/HOL/Auth/Public.ML

--- a/src/HOL/Auth/Public.ML	Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Thu Sep 18 13:24:04 1997 +0200
@@ -44,49 +44,50 @@
 Addsimps [keysFor_parts_initState];
 
 
-(*** Function "sees" ***)
+(*** Function "spies" ***)
 
 (*Agents see their own private keys!*)
-goal thy "A ~= Spy --> Key (priK A) : sees A evs";
-by (induct_tac "evs" 1);
+goal thy "Key (priK A) : initState A";
 by (induct_tac "A" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-qed_spec_mp "sees_own_priK";
+by (Auto_tac());
+qed "priK_in_initState";
+AddIffs [priK_in_initState];
 
-(*All public keys are visible to all*)
-goal thy "Key (pubK A) : sees B evs";
+(*All public keys are visible*)
+goal thy "Key (pubK A) : spies evs";
 by (induct_tac "evs" 1);
-by (induct_tac "B" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Auto_tac ());
-qed_spec_mp "sees_pubK";
+by (ALLGOALS (asm_simp_tac
+	      (!simpset addsimps [imageI, spies_Cons]
+	                setloop split_tac [expand_event_case, expand_if])));
+qed_spec_mp "spies_pubK";
 
-(*Spy sees private keys of agents!*)
-goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs";
+(*Spy sees private keys of bad agents!*)
+goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
 by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons])));
-by (Blast_tac 1);
-qed "Spy_sees_lost";
+by (ALLGOALS (asm_simp_tac
+	      (!simpset addsimps [imageI, spies_Cons]
+	                setloop split_tac [expand_event_case, expand_if])));
+qed "Spy_spies_bad";
 
-AddIffs [sees_pubK, sees_pubK RS analz.Inj];
-AddSIs  [sees_own_priK, Spy_sees_lost];
+AddIffs [spies_pubK, spies_pubK RS analz.Inj];
+AddSIs  [Spy_spies_bad];
 
 
-(*For not_lost_tac*)
-goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs);  A: lost |] \
-\              ==> X : analz (sees Spy evs)";
+(*For not_bad_tac*)
+goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
+\              ==> X : analz (spies evs)";
 by (blast_tac (!claset addSDs [analz.Decrypt]) 1);
-qed "Crypt_Spy_analz_lost";
+qed "Crypt_Spy_analz_bad";
 
 (*Prove that the agent is uncompromised by the confidentiality of 
   a component of a message she's said.*)
-fun not_lost_tac s =
-    case_tac ("(" ^ s ^ ") : lost") THEN'
+fun not_bad_tac s =
+    case_tac ("(" ^ s ^ ") : bad") THEN'
     SELECT_GOAL 
-      (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
+      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
        REPEAT_DETERM (etac MPair_analz 1) THEN
        THEN_BEST_FIRST 
-         (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
+         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
          (has_fewer_prems 1, size_of_thm)
          (Step_tac 1));
 
@@ -100,27 +101,30 @@
 AddIffs [Nonce_notin_initState];
 
 goal thy "Nonce N ~: used []";
-by (simp_tac (!simpset addsimps [used_def]) 1);
+by (simp_tac (!simpset addsimps [used_Nil]) 1);
 qed "Nonce_notin_used_empty";
 Addsimps [Nonce_notin_used_empty];
 
 
 (*** Supply fresh nonces for possibility theorems. ***)
 
-goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+(*In any trace, there is an upper bound N on the greatest nonce in use.*)
+goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
 by (induct_tac "evs" 1);
 by (res_inst_tac [("x","0")] exI 1);
+by (ALLGOALS (asm_simp_tac
+	      (!simpset addsimps [used_Cons]
+			setloop split_tac [expand_event_case, expand_if])));
 by (Step_tac 1);
-by (Full_simp_tac 1);
-(*Inductive step*)
-by (induct_tac "a" 1);
-by (ALLGOALS (full_simp_tac 
-	      (!simpset addsimps [UN_parts_sees_Says,
-				  UN_parts_sees_Notes])));
 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
 by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
 val lemma = result();
 
+goal thy "EX N. Nonce N ~: used evs";
+by (rtac (lemma RS exE) 1);
+by (Blast_tac 1);
+qed "Nonce_supply1";
+
 goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
 by (rtac (lemma RS exE) 1);
 by (rtac selectI 1);