diff -r 883359757a56 -r ee98c2528a8f doc-src/TutorialI/Protocol/Public.thy
--- a/doc-src/TutorialI/Protocol/Public.thy	Mon Jul 23 14:30:53 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy	Mon Jul 23 14:31:34 2007 +0200
@@ -6,20 +6,24 @@
 Theory of Public Keys (common to all public-key protocols)
 
 Private and public keys; initial states of agents
-*)
-
+*)(*<*)
 theory Public imports Event
-uses ("Public_lemmas.ML") begin
+begin
+(*>*)
 
-consts
-  pubK    :: "agent => key"
+text {*
+The function
+@{text pubK} maps agents to their public keys.  The function
+@{text priK} maps agents to their private keys.  It is defined in terms of
+@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is
+not a proper constant, so we declare it using \isacommand{syntax}
+(cf.\ \S\ref{sec:syntax-translations}).
+*}
 
-syntax
-  priK    :: "agent => key"
-
-translations  (*BEWARE! expressions like  (inj priK)  will NOT work!*)
-  "priK x"  == "invKey(pubK x)"
-
+consts pubK :: "agent => key"
+syntax priK :: "agent => key"
+translations "priK x" \<rightleftharpoons> "invKey(pubK x)"
+(*<*)
 primrec
         (*Agents know their private key and all public keys*)
   initState_Server:  "initState Server     =    
@@ -28,19 +32,139 @@
  		         insert (Key (priK (Friend i))) (Key ` range pubK)"
   initState_Spy:     "initState Spy        =    
  		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+(*>*)
 
+text {*
+\noindent
+The set @{text bad} consists of those agents whose private keys are known to
+the spy.
+
+Two axioms are asserted about the public-key cryptosystem. 
+No two agents have the same public key, and no private key equals
+any public key.
+*}
 
 axioms
-  (*Public keys are disjoint, and never clash with private keys*)
   inj_pubK:        "inj pubK"
   priK_neq_pubK:   "priK A ~= pubK B"
+(*<*)
+lemmas [iff] = inj_pubK [THEN inj_eq]
 
-use "Public_lemmas.ML"
+lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
+  apply safe
+  apply (drule_tac f=invKey in arg_cong)
+  apply simp
+  done
+
+lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]
+
+lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys"
+  by (simp add: symKeys_def)
+
+lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
+  by (simp add: symKeys_def)
+
+lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
+  by blast
+
+lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H;  K \<in> symKeys;  Key K \<in> analz H |]
+     ==> X \<in> analz H"
+  by (auto simp add: symKeys_def)
+
+
+(** "Image" equations that hold for injective functions **)
+
+lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)"
+  by auto
+
+(*holds because invKey is injective*)
+lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)"
+  by auto
+
+lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)"
+  by auto
+
+
+(** Rewrites should not refer to  initState(Friend i) 
+    -- not in normal form! **)
+
+lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
+  apply (unfold keysFor_def)
+  apply (induct C)
+  apply (auto intro: range_eqI)
+  done
+
+
+(*** Function "spies" ***)
+
+(*Agents see their own private keys!*)
+lemma priK_in_initState[iff]: "Key (priK A) : initState A"
+  by (induct A) auto
+
+(*All public keys are visible*)
+lemma spies_pubK[iff]: "Key (pubK A) : spies evs"
+  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
+
+(*Spy sees private keys of bad agents!*)
+lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs"
+  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
+
+lemmas [iff] = spies_pubK [THEN analz.Inj]
+
+
+(*** Fresh nonces ***)
+
+lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)"
+  by (induct B) auto
+
+lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []"
+  by (simp add: used_Nil)
+
+
+(*** Supply fresh nonces for possibility theorems. ***)
+
+(*In any trace, there is an upper bound N on the greatest nonce in use.*)
+lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
+apply (induct_tac "evs")
+apply (rule_tac x = 0 in exI)
+apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
+apply safe
+apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
+done
+
+lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
+by (rule Nonce_supply_lemma [THEN exE], blast)
+
+lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
+apply (rule Nonce_supply_lemma [THEN exE])
+apply (rule someI, fast)
+done
+
+
+(*** Specialized rewriting for the analz_image_... theorems ***)
+
+lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
+  by blast
+
+lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
+  by blast
+
 
 (*Specialized methods*)
 
+(*Tactic for possibility theorems*)
+ML {*
+fun possibility_tac st = st |>
+    REPEAT (*omit used_Says so that Nonces start from different traces!*)
+    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
+     THEN
+     REPEAT_FIRST (eq_assume_tac ORELSE' 
+                   resolve_tac [refl, conjI, @{thm Nonce_supply}]));
+*}
+
 method_setup possibility = {*
     Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
     "for proving possibility theorems"
 
 end
+(*>*)
\ No newline at end of file