--- /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];
+
+
--- /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
--- /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];
--- /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