# HG changeset patch
# User paulson
# Date 835968399 -7200
# Node ID 199243afac2b9b182b0bd3043a6efa777b412f29
# Parent  91e0395adc72fa31653a21fa42684f5ef22f66c6
Proving safety properties of authentication protocols

diff -r 91e0395adc72 -r 199243afac2b src/HOL/Auth/Event.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Event.ML	Fri Jun 28 15:26:39 1996 +0200
@@ -0,0 +1,491 @@
+(*  Title:      HOL/Auth/Message
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Datatype of events;
+inductive relation "traces" for Needham-Schroeder (shared keys)
+*)
+
+
+open Event;
+
+(* invKey (serverKey A) = serverKey A *)
+bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
+
+(* invKey (newK(A,evs)) = newK(A,evs) *)
+bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
+Addsimps [invKey_serverKey, invKey_newK];
+
+
+(*New keys and nonces are fresh*)
+val serverKey_inject = inj_serverKey RS injD;
+val newN_inject = inj_newN RS injD RS Pair_inject
+and newK_inject = inj_newK RS injD RS Pair_inject;
+AddSEs [serverKey_inject, newN_inject, newK_inject,
+	fresh_newK RS notE, fresh_newN RS notE];
+Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
+Addsimps [fresh_newN, fresh_newK];
+
+goal thy "newK (A,evs) ~= serverKey B";
+by (subgoal_tac "newK (A,evs) = serverKey B --> \
+\                Key (newK(A,evs)) : parts (initState B)" 1);
+by (Fast_tac 1);
+by (agent.induct_tac "B" 1);
+by (auto_tac (!claset addIs [range_eqI], !simpset));
+qed "newK_neq_serverKey";
+
+Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
+
+(*Good for talking about Server's initial state*)
+goal thy "parts (range (Key o f)) = range (Key o f)";
+by (auto_tac (!claset addIs [range_eqI], !simpset));
+be parts.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "parts_range_Key";
+
+goal thy "analyze (range (Key o f)) = range (Key o f)";
+by (auto_tac (!claset addIs [range_eqI], !simpset));
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_range_Key";
+
+Addsimps [parts_range_Key, analyze_range_Key];
+
+goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
+by (agent.induct_tac "C" 1);
+by (auto_tac (!claset addIs [range_eqI], !simpset));
+qed "keysFor_parts_initState";
+Addsimps [keysFor_parts_initState];
+
+
+(**** Inductive relation "traces" -- basic properties ****)
+
+val mk_cases = traces.mk_cases (list.simps @ agent.simps @ event.simps);
+
+val Says_tracesE        = mk_cases "Says A B X # evs: traces";
+val Says_Server_tracesE = mk_cases "Says Server B X # evs: traces";
+val Says_Enemy_tracesE  = mk_cases "Says Enemy B X # evs: traces";
+val Says_to_Server_tracesE = mk_cases "Says A Server X # evs: traces";
+val Notes_tracesE       = mk_cases "Notes A X # evs: traces";
+
+
+(*The tail of a trace is a trace*)
+goal thy "!!ev evs. ev#evs : traces ==> evs : traces";
+by (fast_tac (!claset addEs [mk_cases "ev#evs:traces"]) 1);
+qed "traces_ConsE";
+
+(** Specialized rewrite rules for (sees A (Says...#evs)) **)
+
+goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "sees_own";
+
+goal thy "!!A. Server ~= A ==> \
+\              sees Server (Says A B X # evs) = sees Server evs";
+by (Asm_simp_tac 1);
+qed "sees_Server";
+
+goal thy "!!A. Friend i ~= A ==> \
+\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
+by (Asm_simp_tac 1);
+qed "sees_Friend";
+
+goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "sees_Enemy";
+
+goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Fast_tac 1);
+qed "sees_subset";
+
+(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
+goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
+\         parts {Y} Un (UN A. parts (sees A evs))";
+by (Step_tac 1);
+be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
+val ss = (!simpset addsimps [parts_Un, sees_Cons] 
+	           setloop split_tac [expand_if]);
+by (ALLGOALS (fast_tac (!claset addss ss)));
+qed "UN_parts_sees_Says";
+
+
+Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
+Delsimps [sees_Cons];
+
+
+(**** Inductive proofs about traces ****)
+
+(*The Enemy can see more than anybody else, except for their initial state*)
+goal thy 
+ "!!evs. evs : traces ==> \
+\     sees A evs <= initState A Un sees Enemy evs";
+be traces.induct 1;
+be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
+by (ALLGOALS (fast_tac (!claset addDs [sees_subset RS subsetD] 
+			        addss (!simpset))));
+qed "sees_agent_subset_sees_Enemy";
+
+
+(*** Server keys are not betrayed ***)
+
+(*No Enemy will ever see a Friend's server key
+   -- even if another friend's key is compromised.
+  The UN is essential to handle the Fake rule in the induction.*)
+goal thy 
+ "!!evs. [| evs : traces;  i~=j |] ==> \
+\        Key (serverKey (Friend i)) ~: \
+\        parts (initState (Friend j) Un sees Enemy evs)";
+be traces.induct 1;
+be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+by (Auto_tac());
+(*Deals with Faked messages*)
+by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
+			     imp_of_subset parts_insert_subset_Un]
+	              addss (!simpset)) 1);
+qed "Enemy_not_see_serverKey";
+
+(*No Friend will ever see another Friend's server key.*)
+goal thy 
+ "!!evs. [| evs : traces;  i~=j |] ==> \
+\        Key (serverKey (Friend i)) ~: parts (sees (Friend j) evs)";
+br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
+by (REPEAT (ares_tac [Enemy_not_see_serverKey] 1));
+qed "Friend_not_see_serverKey";
+
+(*Variant needed for the theorem below*)
+goal thy 
+ "!!evs. evs : traces ==> \
+\        Key (serverKey (Friend i)) ~: analyze (sees Enemy evs)";
+bd Enemy_not_see_serverKey 1;
+br n_not_Suc_n 1;
+by (Full_simp_tac 1);
+by (fast_tac (!claset addDs [imp_of_subset analyze_subset_parts]) 1);
+qed "serverKeys_not_analyzed";
+
+
+(*** Future keys can't be seen or used! ***)
+
+(*Nobody can have SEEN keys that will be generated in the future.
+  This has to be proved anew for each protocol description,
+  but should go by similar reasoning every time.  Hardest case is the
+  standard Fake rule.  
+      The length comparison, and Union over C, are essential for the 
+  induction! *)
+goal thy "!!evs. evs : traces ==> \
+\                length evs <= length evs' --> \
+\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
+be traces.induct 1;
+be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+by (ALLGOALS (asm_full_simp_tac
+	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
+(*Initial state?  New keys cannot clash*)
+by (Fast_tac 1);
+(*Rule NS1 in protocol*)
+by (fast_tac (!claset addDs [less_imp_le]) 2);
+(*Rule NS2 in protocol*)
+by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
+(*Rule Fake: where an Enemy agent can say practically anything*)
+by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
+			     imp_of_subset parts_insert_subset_Un,
+			     less_imp_le]
+	              addss (!simpset)) 1);
+val lemma = result();
+
+(*Variant needed for the main theorem below*)
+goal thy 
+ "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
+\        Key (newK (A,evs')) ~: parts (sees C evs)";
+by (fast_tac (!claset addDs [lemma]) 1);
+qed "new_keys_not_seen";
+
+goal thy "!!K. newK(A,evs) = invKey K ==> newK(A,evs) = K";
+br (invKey_eq RS iffD1) 1;
+by (Simp_tac 1);
+val newK_invKey = result();
+
+(*Nobody can have USED keys that will be generated in the future.
+  ...very like new_keys_not_seen*)
+goal thy "!!evs. evs : traces ==> \
+\                length evs <= length evs' --> \
+\                newK (A,evs') ~: keysFor (UN C. parts (sees C evs))";
+be traces.induct 1;
+be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+by (ALLGOALS (asm_full_simp_tac
+	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
+(*Rule NS1 in protocol*)
+by (fast_tac (!claset addDs [less_imp_le]) 2);
+(*Rule NS2 in protocol*)
+by (fast_tac (!claset addDs [less_imp_le]) 2);
+(*Rule Fake: where an Enemy agent can say practically anything*)
+by (best_tac 
+    (!claset addSDs [newK_invKey]
+	     addDs [imp_of_subset (analyze_subset_parts RS keysFor_mono),
+		    imp_of_subset (parts_insert_subset_Un RS keysFor_mono),
+		    less_imp_le]
+             addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)]
+	     addss (!simpset)) 1);
+val lemma = result();
+
+goal thy 
+ "!!evs. [| evs : traces;  length evs <= length evs' |] ==> \
+\        newK (A,evs') ~: keysFor (parts (sees C evs))";
+by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
+qed "new_keys_not_used";
+
+bind_thm ("new_keys_not_used_analyze",
+	  [analyze_subset_parts RS keysFor_mono,
+	   new_keys_not_used] MRS contra_subsetD);
+
+
+(*Pushes Crypt events in so that others might be pulled out*)
+goal thy "insert (Crypt X K) (insert y evs) = \
+\         insert y (insert (Crypt X K) evs)";
+by (Fast_tac 1);
+qed "insert_Crypt_delay";
+
+goal thy "insert (Key K) (insert y evs) = \
+\         insert y (insert (Key K) evs)";
+by (Fast_tac 1);
+qed "insert_Key_delay";
+
+(** Lemmas concerning the form of items passed in messages **)
+
+(*Describes the form *and age* of K when the following message is sent*)
+goal thy 
+ "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
+\               : setOfList evs;  \
+\           evs : traces          \
+\        |] ==> (EX evs'. K = Key (newK(Server,evs')) & \
+\                         length evs' < length evs)";
+be rev_mp 1;
+be traces.induct 1;
+be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
+qed "Says_Server_imp_Key_newK";
+
+Addsimps [serverKeys_not_analyzed, 
+	  new_keys_not_seen RS not_parts_not_analyze,
+	  new_keys_not_used_analyze];
+
+
+goal thy 
+ "!!evs. evs : traces ==> \
+\     Says Server (Friend i) \
+\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
+\     --> K ~: analyze (sees Enemy evs)";
+be traces.induct 1;
+be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
+by (ALLGOALS Asm_full_simp_tac);
+(*We infer that K has the form "Key (newK(Server,evs')" ... *)
+br conjI 3;
+by (REPEAT_FIRST (resolve_tac [impI]));
+by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
+(*NS1, subgoal concerns "(Says A Server
+                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
+(*... thus it cannot equal any components of A's message above.*)
+by (fast_tac (!claset addss (!simpset)) 2);
+(*NS2, the subcase where that message was the most recently sent;
+  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
+by (fast_tac (!claset addss (!simpset)) 2);
+(*NS2, other subcase!*)
+by (fast_tac 
+    (!claset addSEs [less_irrefl]
+             addDs [imp_of_subset analyze_insert_Crypt_subset]
+	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
+(*Now for the Fake case*)
+be exE 1;
+br notI 1;
+by (REPEAT (etac conjE 1));
+by (REPEAT (hyp_subst_tac 1));
+by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
+be (imp_of_subset analyze_mono) 2;
+by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
+			     (2,rev_subsetD),
+			     imp_of_subset synthesize_increasing,
+			     imp_of_subset analyze_increasing]) 2);
+(*Proves the Fake goal*)
+by (Auto_tac());
+qed "encrypted_key_not_seen";
+
+
+
+XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
+
+(*Nobody can have SEEN keys that will be generated in the future.
+  This has to be proved anew for each protocol description,
+  but should go by similar reasoning every time.  Hardest case is the
+  standard Fake rule.  
+      The length comparison, and Union over C, are essential for the 
+  induction! *)
+goal thy "!!evs. evs : traces ==> \
+\                length evs <= length evs' --> \
+\                          Key (newK (A,evs')) ~: (UN C. parts (sees C evs))";
+be traces.induct 1;
+be subst 4;	(*DISCARD evsa = Says A Server...#evs'a as irrelevant!*)
+by (ALLGOALS (asm_full_simp_tac
+	      (!simpset addsimps [de_Morgan_disj,Suc_le_eq])));
+(*Initial state?  New keys cannot clash*)
+by (Fast_tac 1);
+(*Rule NS1 in protocol*)
+by (fast_tac (!claset addDs [less_imp_le]) 2);
+(*Rule NS2 in protocol*)
+by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2);
+(*Rule Fake: where an Enemy agent can say practically anything*)
+by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts,
+			     imp_of_subset parts_insert_subset_Un,
+			     less_imp_le]
+	              addss (!simpset)) 1);
+val lemma = result();
+
+
+
+goal thy 
+ "!!evs. [| evs : traces;  i~=j |] ==> \
+\     Says Server (Friend i) \
+\          (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs  \
+\     --> K ~: analyze (initState (Friend j) Un sees Enemy evs)";
+be traces.induct 1;
+be subst 4;	(*simply DISCARD evsa = Says A Server... as irrelevant!*)
+by (ALLGOALS Asm_full_simp_tac);
+(*We infer that K has the form "Key (newK(Server,evs')" ... *)
+br conjI 3;
+by (REPEAT_FIRST (resolve_tac [impI]));
+by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac));
+(*NS1, subgoal concerns "(Says A Server
+                          {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*)
+(*... thus it cannot equal any components of A's message above.*)
+
+by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
+
+by (fast_tac (!claset addss (!simpset)) 2);
+(*NS2, the subcase where that message was the most recently sent;
+  it holds because here K' = serverKey(Friend i), which Enemies can't see*)
+by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
+by (Safe_step_tac 2);
+
+by (stac analyze_insert_Crypt 2);
+
+by (fast_tac (!claset addss (!simpset)) 2);
+(*NS2, other subcase!*)
+
+by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2);
+by (fast_tac 
+    (!claset addSEs [less_irrefl]
+             addDs [imp_of_subset analyze_insert_Crypt_subset]
+	     addss (!simpset addsimps [new_keys_not_used_analyze])) 2);
+(*Now for the Fake case*)
+be exE 1;
+br notI 1;
+by (REPEAT (etac conjE 1));
+by (REPEAT (hyp_subst_tac 1));
+by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1);
+be (imp_of_subset analyze_mono) 2;
+by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN 
+			     (2,rev_subsetD),
+			     imp_of_subset synthesize_increasing,
+			     imp_of_subset analyze_increasing]) 2);
+(*Proves the Fake goal*)
+by (Auto_tac());
+qed "encrypted_key_not_seen";
+
+
+
+
+(*Bet this requires the premise   A = Friend i *)
+goal thy "[| evs : traces;  \
+\            (Says Server A (Crypt {|Agent A, Agent B, K, N|} K')) \
+\            : setOfList evs  \
+\         |] ==> knownBy evs K <= {A,Server}";
+
+
+XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX;
+
+(*NEEDED??*)
+
+goal thy "!!A. X ~= Y ==> (X : sees A (Says B C Y # evs)) = (X : sees A evs)";
+by (asm_simp_tac (!simpset addsimps [sees_Cons] 
+                           setloop split_tac [expand_if]) 1); 
+qed "in_sees_Says";
+
+goal thy "!!A. X ~: parts {Y} ==> \
+\              (X : parts (sees A (Says B C Y # evs))) = \
+\              (X : parts (sees A evs))";
+by (asm_simp_tac (!simpset addsimps [sees_Cons] 
+                           setloop split_tac [expand_if]) 1); 
+by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); 
+qed "in_parts_sees_Says";
+
+goal thy "!!evs. length evs < length evs' ==> newK (A,evs) ~= newK (A',evs')";
+by (fast_tac (!claset addSEs [less_irrefl]) 1);
+qed "length_less_newK_neq";
+
+
+(*Initially
+goal thy "knownBy [] X = \
+\         {A. X = Key (invKey (serverKey A)) | (? i. X = Key (serverKey i))}";
+by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
+qed "knownBy_Nil";
+
+goal thy "!!X. knownBy (x#l) X = ?F(knownBy l X)";
+by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1);
+********************)
+
+goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \
+\         insert {|X,Y|} (insert (Crypt x) evs)";
+by (Fast_tac 1);
+qed "insert_Crypt_MPair_delay";
+
+
+
+WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW;
+
+goal thy 
+ "!!evs. evs : traces ==> \
+\     Says Server A       \
+\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
+\     --> (EX evs'. K = Key (newK(Server,evs')))";
+be traces.induct 1;
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+val Says_Server_lemma = result();
+
+goal thy 
+ "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \
+\               : setOfList evs;  \
+\           evs : traces          \
+\        |] ==> (EX evs'. K = Key (newK(Server,evs')))";
+bd Says_Server_lemma 1;
+by (Fast_tac 1);
+qed "Says_Server_imp_Key_newK";
+
+
+goal thy 
+ "!!evs. evs : traces ==> \
+\     Says Server A \
+\          (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs  \
+\     --> (EX evs'. N = Nonce (newN(A,evs')))";
+be traces.induct 1;
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+val Says_Server_lemma = result();
+
+
+YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY;
+
+goalw thy [keysFor_def]
+    "!!X. Crypt X K: H ==> invKey K : keysFor H";
+by (Fast_tac 1);
+qed "keysFor_I";
+AddSIs [keysFor_I];
+
+goalw thy [keysFor_def]
+    "!!K. K : keysFor H ==> EX X K'. K=invKey K' & Crypt X K': H";
+by (Fast_tac 1);
+qed "keysFor_D";
+AddSDs [keysFor_D];
+
+
diff -r 91e0395adc72 -r 199243afac2b src/HOL/Auth/Event.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Event.thy	Fri Jun 28 15:26:39 1996 +0200
@@ -0,0 +1,104 @@
+(*  Title:      HOL/Auth/Message
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Datatype of events;
+inductive relation "traces" for Needham-Schroeder (shared keys)
+
+WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
+  PUBLIC KEY...
+*)
+
+Event = Message + List + 
+
+consts
+  publicKey    :: agent => key
+  serverKey    :: agent => key	(*symmetric keys*)
+
+rules
+  isSym_serverKey "isSymKey (serverKey A)"
+
+consts	(*Initial states of agents -- parameter of the construction*)
+  initState :: agent => msg set
+
+primrec initState agent
+	(*Server knows all keys; other agents know only their own*)
+  initState_Server  "initState Server     = range (Key o serverKey)"
+  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
+  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
+
+(**
+For asymmetric keys: server knows all public and private keys,
+  others know their private key and perhaps all public keys  
+**)
+
+datatype  (*Messages, and components of agent stores*)
+  event = Says agent agent msg
+        | Notes agent msg
+
+consts  
+  sees1 :: [agent, event] => msg set
+
+primrec sees1 event
+           (*First agent recalls all that it says, but NOT everything
+             that is sent to it; it must note such things if/when received*)
+  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
+          (*part of A's internal state*)
+  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
+
+consts  
+  sees :: [agent, event list] => msg set
+
+primrec sees list
+	(*Initial knowledge includes all public keys and own private key*)
+  sees_Nil  "sees A []       = initState A"
+  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
+
+
+constdefs
+  knownBy :: [event list, msg] => agent set
+  "knownBy evs X == {A. X: analyze (sees A evs)}"
+
+
+(*Agents generate "random" nonces.  Different agents always generate
+  different nonces.  Different traces also yield different nonces.  Same
+  applies for keys.*)
+(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
+  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
+consts
+  newN :: "agent * event list => nat"
+  newK :: "agent * event list => key"
+
+rules
+  inj_serverKey "inj serverKey"
+
+  inj_newN   "inj(newN)"
+  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
+
+  inj_newK   "inj(newK)"
+  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
+  isSym_newK "isSymKey (newK(A,evs))"
+
+
+consts  traces   :: "event list set"
+inductive traces
+  intrs 
+    Nil  "[]: traces"
+
+    (*The enemy MAY say anything he CAN say.  We do not expect him to
+      invent new nonces here, but he can also use NS1.*)
+    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
+          |] ==> (Says Enemy B X) # evs : traces"
+
+    NS1  "[| evs: traces;  A ~= Server
+          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
+                 # evs : traces"
+
+    NS2  "[| evs: traces;  
+             evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
+          |] ==> (Says Server A 
+                       (Crypt {|Agent A, Agent B, 
+                                Key (newK(Server,evs)), Nonce NA|}
+                              (serverKey A))) # evs : traces"
+end
diff -r 91e0395adc72 -r 199243afac2b src/HOL/Auth/Message.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Message.ML	Fri Jun 28 15:26:39 1996 +0200
@@ -0,0 +1,606 @@
+(*  Title:      HOL/Auth/Message
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Datatypes of agents and messages;
+Inductive relations "parts", "analyze" and "synthesize"
+*)
+
+open Message;
+
+
+(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
+
+(*Maybe swap the safe_tac and simp_tac lines?**)
+fun auto_tac (cs,ss) = 
+    TRY (safe_tac cs) THEN 
+    ALLGOALS (asm_full_simp_tac ss) THEN
+    REPEAT (FIRSTGOAL (best_tac (cs addss ss)));
+
+fun Auto_tac() = auto_tac (!claset, !simpset);
+
+fun auto() = by (Auto_tac());
+
+fun imp_of_subset th = th RSN (2, rev_subsetD);
+
+(**************** INSTALL CENTRALLY SOMEWHERE? ****************)
+
+
+
+(** Inverse of keys **)
+
+goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
+by (Step_tac 1);
+br box_equals 1;
+by (REPEAT (rtac invKey 2));
+by (Asm_simp_tac 1);
+qed "invKey_eq";
+
+Addsimps [invKey, invKey_eq];
+
+
+(**** keysFor operator ****)
+
+goalw thy [keysFor_def] "keysFor {} = {}";
+by (Fast_tac 1);
+qed "keysFor_empty";
+
+goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
+by (Fast_tac 1);
+qed "keysFor_Un";
+
+goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
+by (Fast_tac 1);
+qed "keysFor_UN";
+
+(*Monotonicity*)
+goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
+by (Fast_tac 1);
+qed "keysFor_mono";
+
+goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
+by (fast_tac (!claset addss (!simpset)) 1);
+qed "keysFor_insert_Agent";
+
+goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
+by (fast_tac (!claset addss (!simpset)) 1);
+qed "keysFor_insert_Nonce";
+
+goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
+by (fast_tac (!claset addss (!simpset)) 1);
+qed "keysFor_insert_Key";
+
+goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
+by (fast_tac (!claset addss (!simpset)) 1);
+qed "keysFor_insert_MPair";
+
+goalw thy [keysFor_def]
+    "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
+by (Auto_tac());
+by (fast_tac (!claset addIs [image_eqI]) 1);
+qed "keysFor_insert_Crypt";
+
+Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
+	  keysFor_insert_Agent, keysFor_insert_Nonce,
+	  keysFor_insert_Key, keysFor_insert_MPair,
+	  keysFor_insert_Crypt];
+
+
+(**** Inductive relation "parts" ****)
+
+val major::prems = 
+goal thy "[| {|X,Y|} : parts H;       \
+\            [| X : parts H; Y : parts H |] ==> P  \
+\         |] ==> P";
+by (cut_facts_tac [major] 1);
+brs prems 1;
+by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1));
+qed "MPair_parts";
+
+AddIs  [parts.Inj];
+AddSEs [MPair_parts];
+AddDs  [parts.Body];
+
+goal thy "H <= parts(H)";
+by (Fast_tac 1);
+qed "parts_increasing";
+
+(*Monotonicity*)
+goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "parts_mono";
+
+goal thy "parts{} = {}";
+by (Step_tac 1);
+be parts.induct 1;
+by (ALLGOALS Fast_tac);
+qed "parts_empty";
+Addsimps [parts_empty];
+
+goal thy "!!X. X: parts{} ==> P";
+by (Asm_full_simp_tac 1);
+qed "parts_emptyE";
+AddSEs [parts_emptyE];
+
+
+(** Unions **)
+
+goal thy "parts(G) Un parts(H) <= parts(G Un H)";
+by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
+val parts_Un_subset1 = result();
+
+goal thy "parts(G Un H) <= parts(G) Un parts(H)";
+br subsetI 1;
+be parts.induct 1;
+by (ALLGOALS Fast_tac);
+val parts_Un_subset2 = result();
+
+goal thy "parts(G Un H) = parts(G) Un parts(H)";
+by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
+qed "parts_Un";
+
+goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
+by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
+val parts_UN_subset1 = result();
+
+goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
+br subsetI 1;
+be parts.induct 1;
+by (ALLGOALS Fast_tac);
+val parts_UN_subset2 = result();
+
+goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
+by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
+qed "parts_UN";
+
+goal thy "parts(UN x. H x) = (UN x. parts(H x))";
+by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1);
+qed "parts_UN1";
+
+(*Added to simplify arguments to parts, analyze and synthesize*)
+Addsimps [parts_Un, parts_UN, parts_UN1];
+
+goal thy "insert X (parts H) <= parts(insert X H)";
+by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1);
+qed "parts_insert_subset";
+
+(*Especially for reasoning about the Fake rule in traces*)
+goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
+br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1;
+by (Fast_tac 1);
+qed "parts_insert_subset_Un";
+
+(** Idempotence and transitivity **)
+
+goal thy "!!H. X: parts (parts H) ==> X: parts H";
+be parts.induct 1;
+by (ALLGOALS Fast_tac);
+qed "parts_partsE";
+AddSEs [parts_partsE];
+
+goal thy "parts (parts H) = parts H";
+by (Fast_tac 1);
+qed "parts_idem";
+Addsimps [parts_idem];
+
+goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
+by (dtac parts_mono 1);
+by (Fast_tac 1);
+qed "parts_trans";
+
+(*Cut*)
+goal thy "!!H. [| X: parts H;  Y: parts (insert X H) |] ==> Y: parts H";
+be parts_trans 1;
+by (Fast_tac 1);
+qed "parts_cut";
+
+
+(** Rewrite rules for pulling out atomic messages **)
+
+goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
+by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
+br subsetI 1;
+be parts.induct 1;
+(*Simplification breaks up equalities between messages;
+  how to make it work for fast_tac??*)
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "parts_insert_Agent";
+
+goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
+by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
+br subsetI 1;
+be parts.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "parts_insert_Nonce";
+
+goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
+by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
+br subsetI 1;
+be parts.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "parts_insert_Key";
+
+goal thy "parts (insert (Crypt X K) H) = \
+\         insert (Crypt X K) (parts (insert X H))";
+br equalityI 1;
+br subsetI 1;
+be parts.induct 1;
+by (Auto_tac());
+be parts.induct 1;
+by (ALLGOALS (best_tac (!claset addIs [parts.Body])));
+qed "parts_insert_Crypt";
+
+goal thy "parts (insert {|X,Y|} H) = \
+\         insert {|X,Y|} (parts (insert X (insert Y H)))";
+br equalityI 1;
+br subsetI 1;
+be parts.induct 1;
+by (Auto_tac());
+be parts.induct 1;
+by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
+qed "parts_insert_MPair";
+
+Addsimps [parts_insert_Agent, parts_insert_Nonce, 
+	  parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
+
+
+(**** Inductive relation "analyze" ****)
+
+val major::prems = 
+goal thy "[| {|X,Y|} : analyze H;       \
+\            [| X : analyze H; Y : analyze H |] ==> P  \
+\         |] ==> P";
+by (cut_facts_tac [major] 1);
+brs prems 1;
+by (REPEAT (eresolve_tac [asm_rl, analyze.Fst, analyze.Snd] 1));
+qed "MPair_analyze";
+
+AddIs  [analyze.Inj];
+AddSEs [MPair_analyze];
+AddDs  [analyze.Decrypt];
+
+goal thy "H <= analyze(H)";
+by (Fast_tac 1);
+qed "analyze_increasing";
+
+goal thy "analyze H <= parts H";
+by (rtac subsetI 1);
+be analyze.induct 1;
+by (ALLGOALS Fast_tac);
+qed "analyze_subset_parts";
+
+bind_thm ("not_parts_not_analyze", analyze_subset_parts RS contra_subsetD);
+
+
+goal thy "parts (analyze H) = parts H";
+br equalityI 1;
+br (analyze_subset_parts RS parts_mono RS subset_trans) 1;
+by (Simp_tac 1);
+by (fast_tac (!claset addDs [analyze_increasing RS parts_mono RS subsetD]) 1);
+qed "parts_analyze";
+Addsimps [parts_analyze];
+
+(*Monotonicity; Lemma 1 of Lowe*)
+goalw thy analyze.defs "!!G H. G<=H ==> analyze(G) <= analyze(H)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "analyze_mono";
+
+(** General equational properties **)
+
+goal thy "analyze{} = {}";
+by (Step_tac 1);
+be analyze.induct 1;
+by (ALLGOALS Fast_tac);
+qed "analyze_empty";
+Addsimps [analyze_empty];
+
+(*Converse fails: we can analyze more from the union than from the 
+  separate parts, as a key in one might decrypt a message in the other*)
+goal thy "analyze(G) Un analyze(H) <= analyze(G Un H)";
+by (REPEAT (ares_tac [Un_least, analyze_mono, Un_upper1, Un_upper2] 1));
+qed "analyze_Un";
+
+goal thy "insert X (analyze H) <= analyze(insert X H)";
+by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1);
+qed "analyze_insert";
+
+(** Rewrite rules for pulling out atomic messages **)
+
+goal thy "analyze (insert (Agent agt) H) = insert (Agent agt) (analyze H)";
+by (rtac (analyze_insert RSN (2, equalityI)) 1);
+br subsetI 1;
+be analyze.induct 1;
+(*Simplification breaks up equalities between messages;
+  how to make it work for fast_tac??*)
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Agent";
+
+goal thy "analyze (insert (Nonce N) H) = insert (Nonce N) (analyze H)";
+by (rtac (analyze_insert RSN (2, equalityI)) 1);
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Nonce";
+
+(*Can only pull out Keys if they are not needed to decrypt the rest*)
+goalw thy [keysFor_def]
+    "!!K. K ~: keysFor (analyze H) ==>  \
+\         analyze (insert (Key K) H) = insert (Key K) (analyze H)";
+by (rtac (analyze_insert RSN (2, equalityI)) 1);
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Key";
+
+goal thy "!!H. Key (invKey K) ~: analyze H ==>  \
+\              analyze (insert (Crypt X K) H) = \
+\              insert (Crypt X K) (analyze H)";
+by (rtac (analyze_insert RSN (2, equalityI)) 1);
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Crypt";
+
+goal thy "!!H. Key (invKey K) : analyze H ==>  \
+\              analyze (insert (Crypt X K) H) <= \
+\              insert (Crypt X K) (analyze (insert X H))";
+br subsetI 1;
+by (eres_inst_tac [("za","x")] analyze.induct 1);
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+val lemma1 = result();
+
+goal thy "!!H. Key (invKey K) : analyze H ==>  \
+\              insert (Crypt X K) (analyze (insert X H)) <= \
+\              analyze (insert (Crypt X K) H)";
+by (Auto_tac());
+by (eres_inst_tac [("za","x")] analyze.induct 1);
+by (Auto_tac());
+by (best_tac (!claset addIs [subset_insertI RS analyze_mono RS subsetD,
+			     analyze.Decrypt]) 1);
+val lemma2 = result();
+
+goal thy "!!H. Key (invKey K) : analyze H ==>  \
+\              analyze (insert (Crypt X K) H) = \
+\              insert (Crypt X K) (analyze (insert X H))";
+by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
+qed "analyze_insert_Decrypt";
+
+Addsimps [analyze_insert_Agent, analyze_insert_Nonce, 
+	  analyze_insert_Key, analyze_insert_Crypt,
+	  analyze_insert_Decrypt];
+
+
+(*This rule supposes "for the sake of argument" that we have the key.*)
+goal thy  "analyze (insert (Crypt X K) H) <=  \
+\         insert (Crypt X K) (analyze (insert X H))";
+br subsetI 1;
+be analyze.induct 1;
+by (Auto_tac());
+qed "analyze_insert_Crypt_subset";
+
+
+(** Rewrite rules for pulling out atomic parts of messages **)
+
+goal thy "analyze (insert X H) <= analyze (insert {|X,Y|} H)";
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (best_tac (!claset addIs [analyze.Fst]))); 
+qed "analyze_insert_subset_MPair1";
+
+goal thy "analyze (insert Y H) <= analyze (insert {|X,Y|} H)";
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (best_tac (!claset addIs [analyze.Snd]))); 
+qed "analyze_insert_subset_MPair2";
+
+goal thy "analyze (insert {|Agent agt,Y|} H) = \
+\         insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))";
+by (rtac equalityI 1);
+by (best_tac (!claset addIs [analyze.Fst,
+			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Agent_MPair";
+
+goal thy "analyze (insert {|Nonce N,Y|} H) = \
+\         insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))";
+by (rtac equalityI 1);
+by (best_tac (!claset addIs [analyze.Fst,
+			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Nonce_MPair";
+
+(*Can only pull out Keys if they are not needed to decrypt the rest*)
+goalw thy [keysFor_def]
+    "!!K. K ~: keysFor (analyze (insert Y H)) ==>  \
+\         analyze (insert {|Key K, Y|} H) = \
+\         insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))";
+by (rtac equalityI 1);
+by (best_tac (!claset addIs [analyze.Fst,
+			     imp_of_subset analyze_insert_subset_MPair2]) 2); 
+br subsetI 1;
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "analyze_insert_Key_MPair";
+
+Addsimps [analyze_insert_Agent_MPair, analyze_insert_Nonce_MPair,
+	  analyze_insert_Key_MPair];
+
+(** Idempotence and transitivity **)
+
+goal thy "!!H. X: analyze (analyze H) ==> X: analyze H";
+be analyze.induct 1;
+by (ALLGOALS Fast_tac);
+qed "analyze_analyzeE";
+AddSEs [analyze_analyzeE];
+
+goal thy "analyze (analyze H) = analyze H";
+by (Fast_tac 1);
+qed "analyze_idem";
+Addsimps [analyze_idem];
+
+goal thy "!!H. [| X: analyze G;  G <= analyze H |] ==> X: analyze H";
+by (dtac analyze_mono 1);
+by (Fast_tac 1);
+qed "analyze_trans";
+
+(*Cut; Lemma 2 of Lowe*)
+goal thy "!!H. [| X: analyze H;  Y: analyze (insert X H) |] ==> Y: analyze H";
+be analyze_trans 1;
+by (Fast_tac 1);
+qed "analyze_cut";
+
+(*Cut can be proved easily by induction on
+   "!!H. Y: analyze (insert X H) ==> X: analyze H --> Y: analyze H"
+*)
+
+(*If there are no pairs or encryptions then analyze does nothing*)
+goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
+\         analyze H = H";
+by (Step_tac 1);
+be analyze.induct 1;
+by (ALLGOALS Fast_tac);
+qed "analyze_trivial";
+
+(*Helps to prove Fake cases*)
+goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)";
+be analyze.induct 1;
+by (ALLGOALS (fast_tac (!claset addEs [imp_of_subset analyze_mono])));
+val lemma = result();
+
+goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)";
+by (fast_tac (!claset addIs [lemma]
+		      addEs [imp_of_subset analyze_mono]) 1);
+qed "analyze_UN_analyze";
+Addsimps [analyze_UN_analyze];
+
+
+(**** Inductive relation "synthesize" ****)
+
+AddIs  synthesize.intrs;
+
+goal thy "H <= synthesize(H)";
+by (Fast_tac 1);
+qed "synthesize_increasing";
+
+(*Monotonicity*)
+goalw thy synthesize.defs "!!G H. G<=H ==> synthesize(G) <= synthesize(H)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "synthesize_mono";
+
+(** Unions **)
+
+(*Converse fails: we can synthesize more from the union than from the 
+  separate parts, building a compound message using elements of each.*)
+goal thy "synthesize(G) Un synthesize(H) <= synthesize(G Un H)";
+by (REPEAT (ares_tac [Un_least, synthesize_mono, Un_upper1, Un_upper2] 1));
+qed "synthesize_Un";
+
+(** Idempotence and transitivity **)
+
+goal thy "!!H. X: synthesize (synthesize H) ==> X: synthesize H";
+be synthesize.induct 1;
+by (ALLGOALS Fast_tac);
+qed "synthesize_synthesizeE";
+AddSEs [synthesize_synthesizeE];
+
+goal thy "synthesize (synthesize H) = synthesize H";
+by (Fast_tac 1);
+qed "synthesize_idem";
+
+goal thy "!!H. [| X: synthesize G;  G <= synthesize H |] ==> X: synthesize H";
+by (dtac synthesize_mono 1);
+by (Fast_tac 1);
+qed "synthesize_trans";
+
+(*Cut; Lemma 2 of Lowe*)
+goal thy "!!H. [| X: synthesize H;  Y: synthesize (insert X H) \
+\              |] ==> Y: synthesize H";
+be synthesize_trans 1;
+by (Fast_tac 1);
+qed "synthesize_cut";
+
+
+(*Can only produce a nonce or key if it is already known,
+  but can synthesize a pair or encryption from its components...*)
+val mk_cases = synthesize.mk_cases msg.simps;
+
+val Nonce_synthesize = mk_cases "Nonce n : synthesize H";
+val Key_synthesize   = mk_cases "Key K : synthesize H";
+val MPair_synthesize = mk_cases "{|X,Y|} : synthesize H";
+val Crypt_synthesize = mk_cases "Crypt X K : synthesize H";
+
+AddSEs [Nonce_synthesize, Key_synthesize, MPair_synthesize, Crypt_synthesize];
+
+goal thy "(Nonce N : synthesize H) = (Nonce N : H)";
+by (Fast_tac 1);
+qed "Nonce_synthesize_eq";
+
+goal thy "(Key K : synthesize H) = (Key K : H)";
+by (Fast_tac 1);
+qed "Key_synthesize_eq";
+
+Addsimps [Nonce_synthesize_eq, Key_synthesize_eq];
+
+
+goalw thy [keysFor_def]
+    "keysFor (synthesize H) = keysFor H Un invKey``{K. Key K : H}";
+by (Fast_tac 1);
+qed "keysFor_synthesize";
+Addsimps [keysFor_synthesize];
+
+
+(*** Combinations of parts, analyze and synthesize ***)
+
+(*Not that useful, in view of the following one...*)
+goal thy "parts (synthesize H) <= synthesize (parts H)";
+by (Step_tac 1);
+be parts.induct 1;
+be (parts_increasing RS synthesize_mono RS subsetD) 1;
+by (ALLGOALS Fast_tac);
+qed "parts_synthesize_subset";
+
+goal thy "parts (synthesize H) = parts H Un synthesize H";
+br equalityI 1;
+br subsetI 1;
+be parts.induct 1;
+by (ALLGOALS
+    (best_tac (!claset addIs ((synthesize_increasing RS parts_mono RS subsetD)
+			     ::parts.intrs))));
+qed "parts_synthesize";
+Addsimps [parts_synthesize];
+
+goal thy "analyze (synthesize H) = analyze H Un synthesize H";
+br equalityI 1;
+br subsetI 1;
+be analyze.induct 1;
+by (best_tac
+    (!claset addIs [synthesize_increasing RS analyze_mono RS subsetD]) 5);
+(*Strange that best_tac just can't hack this one...*)
+by (ALLGOALS (deepen_tac (!claset addIs analyze.intrs) 0));
+qed "analyze_synthesize";
+Addsimps [analyze_synthesize];
+
+(*Hard to prove; still needed now that there's only one Enemy?*)
+goal thy "analyze (UN i. synthesize (H i)) = \
+\         analyze (UN i. H i) Un (UN i. synthesize (H i))";
+br equalityI 1;
+br subsetI 1;
+be analyze.induct 1;
+by (best_tac
+    (!claset addEs [imp_of_subset synthesize_increasing,
+		    imp_of_subset analyze_mono]) 5);
+by (Best_tac 1);
+by (deepen_tac (!claset addIs [analyze.Fst]) 0 1);
+by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);
+by (deepen_tac (!claset addSEs [analyze.Decrypt]
+			addIs  [analyze.Decrypt]) 0 1);
+qed "analyze_UN1_synthesize";
+Addsimps [analyze_UN1_synthesize];
diff -r 91e0395adc72 -r 199243afac2b src/HOL/Auth/Message.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Message.thy	Fri Jun 28 15:26:39 1996 +0200
@@ -0,0 +1,114 @@
+(*  Title:      HOL/Auth/Message
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+Datatypes of agents and messages;
+Inductive relations "parts", "analyze" and "synthesize"
+*)
+
+Message = Arith +
+
+(*Is there a difference between a nonce and arbitrary numerical data?
+  Do we need a type of nonces?*)
+
+types 
+  key = nat
+
+consts
+  invKey :: key=>key
+
+rules
+  invKey "invKey (invKey K) = K"
+
+  (*The inverse of a symmetric key is itself;
+    that of a public key is the private key and vice versa*)
+
+constdefs
+  isSymKey :: key=>bool
+  "isSymKey K == (invKey K = K)"
+
+  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
+    because Crypt is a constructor!  We assume that encryption is injective,
+    which is not true in the real world.  The alternative is to take
+    Crypt as an uninterpreted function symbol satisfying the equation
+    above.  This seems to require moving to ZF and regarding msg as an
+    inductive definition instead of a datatype.*) 
+
+datatype  (*We allow any number of friendly agents*)
+  agent = Server | Friend nat | Enemy
+
+consts  
+  isEnemy :: agent => bool
+
+primrec isEnemy agent
+  isEnemy_Server  "isEnemy Server  = False"
+  isEnemy_Friend  "isEnemy (Friend i) = False"
+  isEnemy_Enemy   "isEnemy Enemy = True"
+
+datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
+  msg = Agent agent
+      | Nonce nat
+      | Key   key
+      | MPair msg msg
+      | Crypt msg key
+
+(*Allows messages of the form {|A,B,NA|}, etc...*)
+syntax
+  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
+
+translations
+  "{|x, y, z|}"   == "{|x, {|y, z|}|}"
+  "{|x, y|}"      == "MPair x y"
+
+
+constdefs  (*Keys useful to decrypt elements of a message set*)
+  keysFor :: msg set => key set
+  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
+
+(** Inductive definition of all "parts" of a message.  **)
+
+consts  parts   :: msg set => msg set
+inductive "parts H"
+  intrs 
+    Inj     "X: H ==> X: parts H"
+    Fst     "{|X,Y|} : parts H ==> X : parts H"
+    Snd     "{|X,Y|} : parts H ==> Y : parts H"
+    Body    "Crypt X K : parts H ==> X : parts H"
+
+
+(** Inductive definition of "analyze" -- what can be broken down from a set of
+    messages, including keys.  A form of downward closure.  Pairs can
+    be taken apart; messages decrypted with known keys.  **)
+
+consts  analyze   :: msg set => msg set
+inductive "analyze H"
+  intrs 
+    Inj     "X: H ==> X: analyze H"
+
+    Fst     "{|X,Y|} : analyze H ==> X : analyze H"
+
+    Snd     "{|X,Y|} : analyze H ==> Y : analyze H"
+
+    Decrypt "[| Crypt X K : analyze H; Key(invKey K): analyze H
+             |] ==> X : analyze H"
+
+
+(** Inductive definition of "synthesize" -- what can be built up from a set of
+    messages.  A form of upward closure.  Pairs can be built, messages
+    encrypted with known keys.  Agent names may be quoted.  **)
+
+consts  synthesize   :: msg set => msg set
+inductive "synthesize H"
+  intrs 
+    Inj     "X: H ==> X: synthesize H"
+
+    Agent   "Agent agt : synthesize H"
+
+    MPair   "[| X: synthesize H;  Y: synthesize H
+             |] ==> {|X,Y|} : synthesize H"
+
+    Crypt   "[| X: synthesize H; Key(K): synthesize H
+             |] ==> Crypt X K : synthesize H"
+
+end