--- a/src/HOL/Auth/Event.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(* Title: HOL/Auth/Event
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-*)
-
-AddIffs [Spy_in_bad, Server_not_bad];
-
-Addsimps [knows_Cons, used_Cons];
-
-(**** Function "knows" ****)
-
-(** Simplifying parts (insert X (knows Spy evs))
- = parts {X} Un parts (knows Spy evs) -- since general case loops*)
-
-bind_thm ("parts_insert_knows_Spy",
- parts_insert |>
- read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
-
-
-Goal "P(event_case sf gf nf ev) = \
-\ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
-\ (ALL A X. ev = Gets A X --> P(gf A X)) & \
-\ (ALL A X. ev = Notes A X --> P(nf A X)))";
-by (induct_tac "ev" 1);
-by Auto_tac;
-qed "expand_event_case";
-
-Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Says";
-
-(*The point of letting the Spy see "bad" agents' notes is to prevent
- redundant case-splits on whether A=Spy and whether A:bad*)
-Goal "knows Spy (Notes A X # evs) = \
-\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Notes";
-
-Goal "knows Spy (Gets A X # evs) = knows Spy evs";
-by (Simp_tac 1);
-qed "knows_Spy_Gets";
-
-Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Says";
-
-Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "knows_Spy_subset_knows_Spy_Notes";
-
-Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Gets";
-
-(*Spy sees what is sent on the traffic*)
-Goal "Says A B X : set evs --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Says_imp_knows_Spy";
-
-Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Notes_imp_knows_Spy";
-
-
-(*Use with addSEs to derive contradictions from old Says events containing
- items known to be fresh*)
-val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs;
-
-Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
-
-
-(*Begin lemmas about agents' knowledge*)
-
-Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Says";
-
-Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Notes";
-
-Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Gets";
-
-
-Goal "knows A evs <= knows A (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Says";
-
-Goal "knows A evs <= knows A (Notes A X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Notes";
-
-Goal "knows A evs <= knows A (Gets A X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Gets";
-
-(*Agents know what they say*)
-Goal "Says A B X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Says_imp_knows";
-
-(*Agents know what they note*)
-Goal "Notes A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Notes_imp_knows";
-
-(*Agents know what they receive*)
-Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Gets_imp_knows_agents";
-
-
-(*What agents DIFFERENT FROM Spy know
- was either said, or noted, or got, or known initially*)
-Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
-\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
-
-(*What the Spy knows -- for the time being --
- was either said or noted, or known initially*)
-Goal "[| X : knows Spy evs |] ==> EX A B. \
-\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
-
-(*END lemmas about agents' knowledge*)
-
-
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [knows_Cons];
-
-
-(*** Fresh nonces ***)
-
-Goal "parts (knows Spy evs) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-qed "parts_knows_Spy_subset_used";
-
-bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
-AddIs [usedI];
-
-Goal "parts (initState B) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-bind_thm ("initState_into_used", impOfSubs (result()));
-
-Goal "used (Says A B X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Says";
-Addsimps [used_Says];
-
-Goal "used (Notes A X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Notes";
-Addsimps [used_Notes];
-
-Goal "used (Gets A X # evs) = used evs";
-by (Simp_tac 1);
-qed "used_Gets";
-Addsimps [used_Gets];
-
-Goal "used [] <= used evs";
-by (Simp_tac 1);
-by (blast_tac (claset() addIs [initState_into_used]) 1);
-qed "used_nil_subset";
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [used_Nil, used_Cons];
-
-
-(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
- New events added by induction to "evs" are discarded. Provided
- this information isn't needed, the proof will be much shorter, since
- it will omit complicated reasoning about analz.*)
-val analz_mono_contra_tac =
- let val analz_impI = read_instantiate_sg (sign_of thy)
- [("P", "?Y ~: analz (knows Spy ?evs)")] impI;
- in
- rtac analz_impI THEN'
- REPEAT1 o
- (dresolve_tac
- [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
- THEN'
- mp_tac
- end;
-
-fun Reception_tac i =
- blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj,
- impOfSubs (parts_insert RS equalityD1),
- parts_trans,
- Says_imp_knows_Spy RS analz.Inj,
- impOfSubs analz_mono, analz_cut]
- addIs [less_SucI]) i;
-
-
-(*Compatibility for the old "spies" function*)
-val spies_partsEs = knows_Spy_partsEs;
-val Says_imp_spies = Says_imp_knows_Spy;
-val parts_insert_spies = parts_insert_knows_Spy;
--- a/src/HOL/Auth/Event.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Event.thy Tue Feb 13 13:16:27 2001 +0100
@@ -11,10 +11,17 @@
stores are visible to him
*)
-Event = Message + List +
+theory Event = Message
+files ("Event_lemmas.ML"):
+
+(*from Message.ML*)
+method_setup spy_analz = {*
+ Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
+ "for proving the Fake case when analz is involved"
+
consts (*Initial states of agents -- parameter of the construction*)
- initState :: agent => msg set
+ initState :: "agent => msg set"
datatype
event = Says agent agent msg
@@ -22,26 +29,26 @@
| Notes agent msg
consts
- bad :: agent set (*compromised agents*)
- knows :: agent => event list => msg set
+ bad :: "agent set" (*compromised agents*)
+ knows :: "agent => event list => msg set"
(*"spies" is retained for compability's sake*)
syntax
- spies :: event list => msg set
+ spies :: "event list => msg set"
translations
"spies" => "knows Spy"
-rules
+axioms
(*Spy has access to his own key for spoof messages, but Server is secure*)
- Spy_in_bad "Spy: bad"
- Server_not_bad "Server ~: bad"
+ Spy_in_bad [iff] : "Spy: bad"
+ Server_not_bad [iff] : "Server ~: bad"
primrec
- knows_Nil "knows A [] = initState A"
- knows_Cons
+ knows_Nil: "knows A [] = initState A"
+ knows_Cons:
"knows A (ev # evs) =
(if A = Spy then
(case ev of
@@ -67,16 +74,22 @@
consts
(*Set of items that might be visible to somebody:
complement of the set of fresh items*)
- used :: event list => msg set
+ used :: "event list => msg set"
primrec
- used_Nil "used [] = (UN B. parts (initState B))"
- used_Cons "used (ev # evs) =
- (case ev of
- Says A B X => parts {X} Un (used evs)
- | Gets A X => used evs
- | Notes A X => parts {X} Un (used evs))"
+ used_Nil: "used [] = (UN B. parts (initState B))"
+ used_Cons: "used (ev # evs) =
+ (case ev of
+ Says A B X => parts {X} Un (used evs)
+ | Gets A X => used evs
+ | Notes A X => parts {X} Un (used evs))"
+use "Event_lemmas.ML"
+
+method_setup analz_mono_contra = {*
+ Method.no_args
+ (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
+ "for proving theorems of the form X ~: analz (knows Spy evs) --> P"
end
--- a/src/HOL/Auth/KerberosIV.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/KerberosIV.ML Tue Feb 13 13:16:27 2001 +0100
@@ -358,7 +358,7 @@
\ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) \
\ | ServTicket : analz (spies evs)";
by (case_tac "Key AuthKey : analz (spies evs)" 1);
-by (force_tac (claset() addSDs [Says_imp_spies RS analz.Inj], simpset()) 1);
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 1);
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
by (blast_tac (claset() addSDs [ServTicket_form]) 1);
qed "Says_tgs_message_form";
@@ -370,54 +370,38 @@
(* The session key, if secure, uniquely identifies the Ticket
whether AuthTicket or ServTicket. As a matter of fact, one can read
also Tgs in the place of B. *)
-Goal "evs : kerberos ==> \
-\ Key SesKey ~: analz (spies evs) --> \
-\ (EX A B T. ALL A' B' T'. \
-\ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|} \
-\ : parts (spies evs) --> A'=A & B'=B & T'=T)";
-by (parts_induct_tac 1);
-by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)
- THEN Fake_parts_insert_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-by (expand_case_tac "SesKey = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
-by (expand_case_tac "SesKey = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
-val lemma = result();
Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|} \
\ : parts (spies evs); \
\ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|} \
-\ : parts (spies evs); \
-\ evs : kerberos; Key SesKey ~: analz (spies evs) |] \
+\ : parts (spies evs); Key SesKey ~: analz (spies evs); \
+\ evs : kerberos |] \
\ ==> A=A' & B=B' & T=T'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Fake, K2, K4*)
+by (Fake_parts_insert_tac 1);
+by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
qed "unique_CryptKey";
-Goal "evs : kerberos \
-\ ==> Key SesKey ~: analz (spies evs) --> \
-\ (EX K' B' T' Ticket'. ALL K B T Ticket. \
-\ Crypt K {|Key SesKey, Agent B, T, Ticket|} \
-\ : parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')";
-by (parts_induct_tac 1);
-by (REPEAT (etac (exI RSN (2,exE)) 1) THEN Fake_parts_insert_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-by (expand_case_tac "SesKey = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
-by (expand_case_tac "SesKey = ?y" 1);
-by (blast_tac (claset() addSEs spies_partsEs) 1);
-val lemma = result();
-
(*An AuthKey is encrypted by one and only one Shared key.
A ServKey is encrypted by one and only one AuthKey.
*)
Goal "[| Crypt K {|Key SesKey, Agent B, T, Ticket|} \
\ : parts (spies evs); \
\ Crypt K' {|Key SesKey, Agent B', T', Ticket'|} \
-\ : parts (spies evs); \
-\ evs : kerberos; Key SesKey ~: analz (spies evs) |] \
+\ : parts (spies evs); Key SesKey ~: analz (spies evs); \
+\ evs : kerberos |] \
\ ==> K=K' & B=B' & T=T' & Ticket=Ticket'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Fake, K2, K4*)
+by (Fake_parts_insert_tac 1);
+by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
qed "Key_unique_SesKey";
@@ -439,50 +423,29 @@
would fail on the K2 and K4 cases.
*)
-(* AuthKey uniquely identifies the message from Kas *)
-Goal "evs : kerberos ==> \
-\ EX A' Ka' Tk' X'. ALL A Ka Tk X. \
-\ Says Kas A (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \
-\ : set evs --> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
-by (etac kerberos.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (Step_tac 1);
-(*K2: it can't be a new key*)
-by (expand_case_tac "AuthKey = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*)
- addSEs spies_partsEs) 1);
-val lemma = result();
-
Goal "[| Says Kas A \
\ (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) : set evs; \
\ Says Kas A' \
\ (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) : set evs; \
\ evs : kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*K2*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
qed "unique_AuthKeys";
(* ServKey uniquely identifies the message from Tgs *)
-Goal "evs : kerberos ==> \
-\ EX A' B' AuthKey' Tk' X'. ALL A B AuthKey Tk X. \
-\ Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tk, X|}) \
-\ : set evs --> A=A' & B=B' & AuthKey=AuthKey' & Tk=Tk' & X=X'";
-by (etac kerberos.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (Step_tac 1);
-(*K4: it can't be a new key*)
-by (expand_case_tac "ServKey = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*)
- addSEs spies_partsEs) 1);
-val lemma = result();
-
Goal "[| Says Tgs A \
\ (Crypt K {|Key ServKey, Agent B, Tt, X|}) : set evs; \
\ Says Tgs A' \
\ (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) : set evs; \
\ evs : kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*K4*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
qed "unique_ServKeys";
--- a/src/HOL/Auth/Kerberos_BAN.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.ML Tue Feb 13 13:16:27 2001 +0100
@@ -202,27 +202,16 @@
(** The session key K uniquely identifies the message **)
-Goal "evs : kerberos_ban ==> \
-\ EX A' Ts' B' X'. ALL A Ts B X. \
-\ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
-\ : set evs \
-\ --> A=A' & Ts=Ts' & B=B' & X=X'";
-by (etac kerberos_ban.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by Safe_tac;
-(*Kb2: it can't be a new key*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (blast_tac (claset() delrules [conjI]) 1);
-val lemma = result();
-
-(*In messages of this form, the session key uniquely identifies the rest*)
Goal "[| Says Server A \
\ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \
\ Says Server A' \
\ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) : set evs;\
\ evs : kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Kb2: it can't be a new key*)
+by (Blast_tac 1);
qed "unique_session_keys";
--- a/src/HOL/Auth/Message.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Message.ML Tue Feb 13 13:16:27 2001 +0100
@@ -367,7 +367,7 @@
by (REPEAT (ares_tac basic_monos 1));
qed "analz_mono";
-val analz_insertI = impOfSubs (subset_insertI RS analz_mono);
+bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
(** General equational properties **)
@@ -847,7 +847,7 @@
"Hash ?X'", "MPair ?X' ?Y"];
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
-val pushes = pushKeys@pushCrypts;
+bind_thms ("pushes", pushKeys@pushCrypts);
(*** Tactics useful for many protocol proofs ***)
@@ -901,20 +901,6 @@
DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
-(** Useful in many uniqueness proofs **)
-fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN
- assume_tac (i+1);
-
-(*Apply the EX-ALL quantification to prove uniqueness theorems in
- their standard form*)
-fun prove_unique_tac lemma =
- EVERY' [dtac lemma,
- REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
- (*Duplicate the assumption*)
- forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
- Blast.depth_tac (claset() addSDs [spec]) 0];
-
-
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
goal Set.thy "A Un (B Un A) = B Un A";
by (Blast_tac 1);
--- a/src/HOL/Auth/NS_Public.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,247 +0,0 @@
-(* Title: HOL/Auth/NS_Public
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
-Version incorporating Lowe's fix (inclusion of B's identify in round 2).
-*)
-
-AddEs spies_partsEs;
-AddDs [impOfSubs analz_subset_parts];
-AddDs [impOfSubs Fake_parts_insert];
-
-AddIffs [Spy_in_bad];
-
-Addsimps [image_eq_UN]; (*accelerates proofs involving nested images*)
-
-(*A "possibility property": there are traces that reach the end*)
-Goal
- "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
-by possibility_tac;
-result();
-
-
-(**** Inductive proofs about ns_public ****)
-
-(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (spies evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (spies evs)) *)
-fun parts_induct_tac i =
- etac ns_public.induct i
- THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN
- prove_simple_subgoals_tac i;
-
-
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's private key! (unless it's bad at start)*)
-Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "Spy_see_priK";
-Addsimps [Spy_see_priK];
-
-Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
-by Auto_tac;
-qed "Spy_analz_priK";
-Addsimps [Spy_analz_priK];
-
-AddSDs [Spy_see_priK RSN (2, rev_iffD1),
- Spy_analz_priK RSN (2, rev_iffD1)];
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
- is secret. (Honest users generate fresh nonces.)*)
-Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
-\ Nonce NA ~: analz (spies evs); evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "no_nonce_NS1_NS2";
-
-(*Adding it to the claset slows down proofs...*)
-val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE);
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
-\ A=A' & B=B'";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*NS1*)
-by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2);
-(*Fake*)
-by (Clarify_tac 1);
-by (Blast_tac 1);
-val lemma = result();
-
-Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
-\ Nonce NA ~: analz (spies evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
-
-(*Tactic for proving secrecy theorems*)
-fun analz_induct_tac i =
- etac ns_public.induct i THEN
- ALLGOALS Asm_simp_tac;
-
-
-(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
-Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Nonce NA ~: analz (spies evs)";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
-(*NS2*)
-by (blast_tac (claset() addDs [unique_NA]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NA";
-
-
-(*Authentication for A: if she receives message 2 and has used NA
- to start a run, then B has sent message 2.*)
-Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs";
-by (etac rev_mp 1);
-(*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
-by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
-by (etac ns_public.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
-qed "A_trusts_NS2";
-
-
-(*If the encrypted message appears then it originated with Alice in NS1*)
-Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
-\ Nonce NA ~: analz (spies evs); \
-\ evs : ns_public |] \
-\==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "B_trusts_NS1";
-
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B
- [unicity of B makes Lowe's fix work]
- [proof closely follows that for unique_NA] *)
-Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' NA' B'. ALL A NA B. \
-\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
-\ --> A=A' & NA=NA' & B=B'";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*NS2*)
-by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2);
-(*Fake*)
-by (Clarify_tac 1);
-by (Blast_tac 1);
-val lemma = result();
-
-Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \
-\ : parts(spies evs); \
-\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
-\ : parts(spies evs); \
-\ Nonce NB ~: analz (spies evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & NA=NA' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NB";
-
-AddDs [unique_NB];
-
-
-(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
-Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Nonce NB ~: analz (spies evs)";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (Blast_tac 4);
-(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NB";
-
-AddDs [Spy_not_see_NB];
-
-
-(*Authentication for B: if he receives message 3 and has used NB
- in message 2, then A has sent message 3.*)
-Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
-by (etac rev_mp 1);
-(*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-by (ALLGOALS Blast_tac);
-qed "B_trusts_NS3";
-
-
-(**** Overall guarantee for B*)
-
-(*Matches only NS2, not NS1 (or NS3)*)
-val Says_imp_spies' =
- read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_spies;
-
-
-(*If B receives NS3 and the nonce NB agrees with the nonce he joined with
- NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*)
-Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\ : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
-by (etac rev_mp 1);
-(*prepare induction over Crypt (pubK B) {|NB|} : parts H*)
-by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
-by (etac ns_public.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Clarify_tac);
-(*NS3 holds because NB determines A and NA*)
-by (ALLGOALS Blast_tac);
-qed "B_trusts_protocol";
-
--- a/src/HOL/Auth/NS_Public.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/NS_Public.thy Tue Feb 13 13:16:27 2001 +0100
@@ -7,39 +7,199 @@
Version incorporating Lowe's fix (inclusion of B's identity in round 2).
*)
-NS_Public = Public +
+theory NS_Public = Public:
-consts ns_public :: event list set
+consts ns_public :: "event list set"
inductive ns_public
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[]: ns_public"
+ Nil: "[] \<in> ns_public"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_public; X: synth (analz (spies evs)) |]
- ==> Says Spy B X # evs : ns_public"
+ Fake: "\<lbrakk>evs \<in> ns_public; X \<in> synth (analz (spies evs))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evs \<in> ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs1: ns_public; Nonce NA ~: used evs1 |]
- ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- # evs1 : ns_public"
+ NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs2: ns_public; Nonce NB ~: used evs2;
- Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
- # evs2 : ns_public"
+ NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
+ # evs2 \<in> ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
- NS3 "[| evs3: ns_public;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
- : set evs3 |]
- ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
+ NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
+ \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+ (*No Oops message. Should there be one?*)
+
+declare knows_Spy_partsEs [elim]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
+ THEN ns_public.NS3])
+by possibility
+
+
+(**** Inductive proofs about ns_public ****)
+
+(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
+lemma Spy_see_priK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+by (erule ns_public.induct, auto)
+
+lemma Spy_analz_priK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+
+(*** Authenticity properties obtained from NS2 ***)
+
+
+(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
+ is secret. (Honest users generate fresh nonces.)*)
+lemma no_nonce_NS1_NS2 [rule_format]:
+ "evs \<in> ns_public
+ \<Longrightarrow> Crypt (pubK C) \<lbrace>NA', Nonce NA, Agent D\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Nonce NA \<in> analz (spies evs)"
+apply (erule ns_public.induct, simp_all)
+apply (blast intro: analz_insertI)+
+done
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+lemma unique_NA:
+ "\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
+ Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
+ Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> A=A' \<and> B=B'"
+apply (erule rev_mp, erule rev_mp, erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+(*Fake, NS1*)
+apply (blast intro: analz_insertI)+
+done
+
+
+(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
+ The major premise "Says A B ..." makes it a dest-rule, so we use
+ (erule rev_mp) rather than rule_format. *)
+theorem Spy_not_see_NA:
+ "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
+apply (erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+apply spy_analz
+apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
+done
+
- (**Oops message??**)
+(*Authentication for A: if she receives message 2 and has used NA
+ to start a run, then B has sent message 2.*)
+lemma A_trusts_NS2_lemma [rule_format]:
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
+ Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+apply (erule ns_public.induct, simp_all)
+(*Fake, NS1*)
+apply (blast dest: Spy_not_see_NA)+
+done
+
+theorem A_trusts_NS2:
+ "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs"
+by (blast intro: A_trusts_NS2_lemma)
+
+
+(*If the encrypted message appears then it originated with Alice in NS1*)
+lemma B_trusts_NS1 [rule_format]:
+ "evs \<in> ns_public
+ \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Nonce NA \<notin> analz (spies evs) \<longrightarrow>
+ Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+apply (erule ns_public.induct, simp_all)
+(*Fake*)
+apply (blast intro!: analz_insertI)
+done
+
+
+
+(*** Authenticity properties obtained from NS2 ***)
+
+(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B
+ [unicity of B makes Lowe's fix work]
+ [proof closely follows that for unique_NA] *)
+
+lemma unique_NB [dest]:
+ "\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace> \<in> parts(spies evs);
+ Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB, Agent B'\<rbrace> \<in> parts(spies evs);
+ Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B'"
+apply (erule rev_mp, erule rev_mp, erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+(*Fake, NS2*)
+apply (blast intro: analz_insertI)+
+done
+
+
+(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
+theorem Spy_not_see_NB [dest]:
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+apply (erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+apply spy_analz
+apply (blast intro: no_nonce_NS1_NS2)+
+done
+
+
+(*Authentication for B: if he receives message 3 and has used NB
+ in message 2, then A has sent message 3.*)
+lemma B_trusts_NS3_lemma [rule_format]:
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
+ Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
+ Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+by (erule ns_public.induct, auto)
+
+theorem B_trusts_NS3:
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs;
+ Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+by (blast intro: B_trusts_NS3_lemma)
+
+(*** Overall guarantee for B ***)
+
+
+(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with
+ NA, then A initiated the run using NA.*)
+theorem B_trusts_protocol:
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
+ Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs \<longrightarrow>
+ Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+by (erule ns_public.induct, auto)
end
--- a/src/HOL/Auth/NS_Public_Bad.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(* Title: HOL/Auth/NS_Public_Bad
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
-Flawed version, vulnerable to Lowe's attack.
-
-From page 260 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-AddEs spies_partsEs;
-AddDs [impOfSubs analz_subset_parts];
-AddDs [impOfSubs Fake_parts_insert];
-
-AddIffs [Spy_in_bad];
-
-Addsimps [image_eq_UN]; (*accelerates proofs involving nested images*)
-
-(*A "possibility property": there are traces that reach the end*)
-Goal
- "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
-by possibility_tac;
-result();
-
-
-(**** Inductive proofs about ns_public ****)
-
-(*Induction for regularity theorems. If induction formula has the form
- X ~: analz (spies evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (spies evs)) *)
-fun parts_induct_tac i =
- etac ns_public.induct i
- THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN
- prove_simple_subgoals_tac i;
-
-
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's private key! (unless it's bad at start)*)
-Goal "evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "Spy_see_priK";
-Addsimps [Spy_see_priK];
-
-Goal "evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
-by Auto_tac;
-qed "Spy_analz_priK";
-Addsimps [Spy_analz_priK];
-
-AddSDs [Spy_see_priK RSN (2, rev_iffD1),
- Spy_analz_priK RSN (2, rev_iffD1)];
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
- is secret. (Honest users generate fresh nonces.)*)
-Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
-\ Nonce NA ~: analz (spies evs); evs : ns_public |] \
-\ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "no_nonce_NS1_NS2";
-
-(*Adding it to the claset slows down proofs...*)
-val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE);
-
-
-(*Unicity for NS1: nonce NA identifies agents A and B*)
-Goal "[| Nonce NA ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' B'. ALL A B. \
-\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
-\ A=A' & B=B'";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*NS1*)
-by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2);
-(*Fake*)
-by (Clarify_tac 1);
-by (Blast_tac 1);
-val lemma = result();
-
-Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies evs); \
-\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
-\ Nonce NA ~: analz (spies evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
-qed "unique_NA";
-
-
-(*Tactic for proving secrecy theorems*)
-fun analz_induct_tac i =
- etac ns_public.induct i THEN
- ALLGOALS Asm_simp_tac;
-
-
-(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
-Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Nonce NA ~: analz (spies evs)";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*NS3*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
-(*NS2*)
-by (blast_tac (claset() addDs [unique_NA]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NA";
-
-
-(*Authentication for A: if she receives message 2 and has used NA
- to start a run, then B has sent message 2.*)
-Goal "[| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
-\ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
-by (etac rev_mp 1);
-(*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
-by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
-by (etac ns_public.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Clarify_tac);
-(*NS2*)
-by (blast_tac (claset() addDs [Spy_not_see_NA, unique_NA]) 3);
-(*NS1*)
-by (Blast_tac 2);
-(*Fake*)
-by (blast_tac (claset() addDs [Spy_not_see_NA]) 1);
-qed "A_trusts_NS2";
-
-
-(*If the encrypted message appears then it originated with Alice in NS1*)
-Goal "[| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
-\ Nonce NA ~: analz (spies evs); \
-\ evs : ns_public |] \
-\==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "B_trusts_NS1";
-
-
-
-(**** Authenticity properties obtained from NS2 ****)
-
-(*Unicity for NS2: nonce NB identifies nonce NA and agent A
- [proof closely follows that for unique_NA] *)
-Goal "[| Nonce NB ~: analz (spies evs); evs : ns_public |] \
-\ ==> EX A' NA'. ALL A NA. \
-\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \
-\ --> A=A' & NA=NA'";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*NS2*)
-by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2);
-(*Fake*)
-by (Blast_tac 1);
-val lemma = result();
-
-Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies evs); \
-\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \
-\ Nonce NB ~: analz (spies evs); \
-\ evs : ns_public |] \
-\ ==> A=A' & NA=NA'";
-by (prove_unique_tac lemma 1);
-qed "unique_NB";
-
-
-(*NB remains secret PROVIDED Alice never responds with round 3*)
-Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
-\ ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Nonce NB ~: analz (spies evs)";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A*)
-by (blast_tac (claset() addDs [unique_NB]) 4);
-(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-qed "Spy_not_see_NB";
-
-
-
-(*Authentication for B: if he receives message 3 and has used NB
- in message 2, then A has sent message 3--to somebody....*)
-Goal "[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
-\ Says A' B (Crypt (pubK B) (Nonce NB)): set evs; \
-\ A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
-by (etac rev_mp 1);
-(*prepare induction over Crypt (pubK B) NB : parts H*)
-by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A (this use of unique_NB is more robust) *)
-by (blast_tac (claset() addDs [Spy_not_see_NB]
- addIs [unique_NB RS conjunct1]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (blast_tac (claset() addDs [Spy_not_see_NB]) 1);
-qed "B_trusts_NS3";
-
-
-(*Can we strengthen the secrecy theorem? NO*)
-Goal "[| A ~: bad; B ~: bad; evs : ns_public |] \
-\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
-\ --> Nonce NB ~: analz (spies evs)";
-by (analz_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-(*NS2: by freshness and unicity of NB*)
-by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
-(*NS1: by freshness*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(*NS3: unicity of NB identifies A and NA, but not B*)
-by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
- THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
-by Auto_tac;
-by (rename_tac "C B' evs3" 1);
-
-(*
-THIS IS THE ATTACK!
-Level 8
-!!evs. [| A ~: bad; B ~: bad; evs : ns_public |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs -->
- Nonce NB ~: analz (spies evs)
- 1. !!C B' evs3.
- [| A ~: bad; B ~: bad; evs3 : ns_public;
- Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set evs3;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3; C : bad;
- Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3;
- Nonce NB ~: analz (spies evs3) |]
- ==> False
-*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Tue Feb 13 13:16:27 2001 +0100
@@ -11,38 +11,222 @@
Proc. Royal Soc. 426 (1989)
*)
-NS_Public_Bad = Public +
+theory NS_Public_Bad = Public:
-consts ns_public :: event list set
+consts ns_public :: "event list set"
inductive ns_public
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[]: ns_public"
+ Nil: "[] \<in> ns_public"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: ns_public; X: synth (analz (spies evs)) |]
- ==> Says Spy B X # evs : ns_public"
+ Fake: "\<lbrakk>evs \<in> ns_public; X \<in> synth (analz (spies evs))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evs \<in> ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs1: ns_public; Nonce NA ~: used evs1 |]
- ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
- # evs1 : ns_public"
+ NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
+ # evs1 \<in> ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs2: ns_public; Nonce NB ~: used evs2;
- Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
- # evs2 : ns_public"
+ NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2;
+ Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
+ # evs2 \<in> ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
- NS3 "[| evs3: ns_public;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
- ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
+ NS3: "\<lbrakk>evs3 \<in> ns_public;
+ Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
+
+ (*No Oops message. Should there be one?*)
+
+declare knows_Spy_partsEs [elim]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
+ THEN ns_public.NS3])
+by possibility
+
+
+(**** Inductive proofs about ns_public ****)
+
+(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
+lemma Spy_see_priK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+by (erule ns_public.induct, auto)
+
+lemma Spy_analz_priK [simp]:
+ "evs \<in> ns_public \<Longrightarrow> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+
+(*** Authenticity properties obtained from NS2 ***)
+
+(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
+ is secret. (Honest users generate fresh nonces.)*)
+lemma no_nonce_NS1_NS2 [rule_format]:
+ "evs \<in> ns_public
+ \<Longrightarrow> Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Nonce NA \<in> analz (spies evs)"
+apply (erule ns_public.induct, simp_all)
+apply (blast intro: analz_insertI)+
+done
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+lemma unique_NA:
+ "\<lbrakk>Crypt(pubK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs);
+ Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs);
+ Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> A=A' \<and> B=B'"
+apply (erule rev_mp, erule rev_mp, erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+(*Fake, NS1*)
+apply (blast intro!: analz_insertI)+
+done
+
+
+(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
+ The major premise "Says A B ..." makes it a dest-rule, so we use
+ (erule rev_mp) rather than rule_format. *)
+theorem Spy_not_see_NA:
+ "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
+apply (erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+apply spy_analz
+apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
+done
+
+
+(*Authentication for A: if she receives message 2 and has used NA
+ to start a run, then B has sent message 2.*)
+lemma A_trusts_NS2_lemma [rule_format]:
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
+ Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
+apply (erule ns_public.induct)
+apply (auto dest: Spy_not_see_NA unique_NA)
+done
+
+theorem A_trusts_NS2:
+ "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
+ Says B' A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
+by (blast intro: A_trusts_NS2_lemma)
+
- (**Oops message??**)
+(*If the encrypted message appears then it originated with Alice in NS1*)
+lemma B_trusts_NS1 [rule_format]:
+ "evs \<in> ns_public
+ \<Longrightarrow> Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Nonce NA \<notin> analz (spies evs) \<longrightarrow>
+ Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
+apply (erule ns_public.induct, simp_all)
+(*Fake*)
+apply (blast intro!: analz_insertI)
+done
+
+
+
+(*** Authenticity properties obtained from NS2 ***)
+
+(*Unicity for NS2: nonce NB identifies nonce NA and agent A
+ [proof closely follows that for unique_NA] *)
+lemma unique_NB [dest]:
+ "\<lbrakk>Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs);
+ Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs);
+ Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> A=A' \<and> NA=NA'"
+apply (erule rev_mp, erule rev_mp, erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+(*Fake, NS2*)
+apply (blast intro!: analz_insertI)+
+done
+
+
+(*NB remains secret PROVIDED Alice never responds with round 3*)
+theorem Spy_not_see_NB [dest]:
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
+apply (erule rev_mp, erule rev_mp)
+apply (erule ns_public.induct, simp_all)
+apply spy_analz
+apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
+apply (blast intro: no_nonce_NS1_NS2)+
+done
+
+
+(*Authentication for B: if he receives message 3 and has used NB
+ in message 2, then A has sent message 3--to somebody....*)
+
+lemma B_trusts_NS3_lemma [rule_format]:
+ "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Crypt (pubK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
+ (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set evs)"
+apply (erule ns_public.induct, auto)
+by (blast intro: no_nonce_NS1_NS2)+
+
+theorem B_trusts_NS3:
+ "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs;
+ Says A' B (Crypt (pubK B) (Nonce NB)) \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> \<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set evs"
+by (blast intro: B_trusts_NS3_lemma)
+
+
+(*Can we strengthen the secrecy theorem Spy_not_see_NB? NO*)
+lemma "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs
+ \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
+apply (erule ns_public.induct, simp_all)
+apply spy_analz
+(*NS1: by freshness*)
+apply (blast)
+(*NS2: by freshness and unicity of NB*)
+apply (blast intro: no_nonce_NS1_NS2)
+(*NS3: unicity of NB identifies A and NA, but not B*)
+apply clarify
+apply (frule_tac A' = "A" in
+ Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB])
+apply auto
+apply (rename_tac C B' evs3)
+oops
+
+(*
+THIS IS THE ATTACK!
+Level 8
+!!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
+ Nonce NB \<notin> analz (spies evs)
+ 1. !!C B' evs3.
+ \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public
+ Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
+ Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
+ C \<in> bad;
+ Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
+ Nonce NB \<notin> analz (spies evs3)\<rbrakk>
+ \<Longrightarrow> False
+*)
end
--- a/src/HOL/Auth/NS_Shared.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,387 +0,0 @@
-(* Title: HOL/Auth/NS_Shared
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
-
-From page 247 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-AddEs spies_partsEs;
-AddDs [impOfSubs analz_subset_parts];
-AddDs [impOfSubs Fake_parts_insert];
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= Server |] \
-\ ==> EX N K. EX evs: ns_shared. \
-\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS
- ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
-by possibility_tac;
-result();
-
-Goal "[| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX evs: ns_shared. \
-\ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS
- ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
-by possibility_tac;
-
-(**** Inductive proofs about ns_shared ****)
-
-(*For reasoning about the encrypted portion of message NS3*)
-Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \
-\ ==> X : parts (spies evs)";
-by (Blast_tac 1);
-qed "NS3_msg_in_parts_spies";
-
-Goal "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
-\ ==> K : parts (spies evs)";
-by (Blast_tac 1);
-qed "Oops_parts_spies";
-
-(*For proving the easier theorems about X ~: parts (spies evs).*)
-fun parts_induct_tac i =
- EVERY [etac ns_shared.induct i,
- REPEAT (FIRSTGOAL analz_mono_contra_tac),
- ftac Oops_parts_spies (i+7),
- ftac NS3_msg_in_parts_spies (i+4),
- prove_simple_subgoals_tac i];
-
-
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by Auto_tac;
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*Nobody can have used non-existent keys!*)
-Goal "evs : ns_shared ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
-by (parts_induct_tac 1);
-(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*NS2, NS4, NS5*)
-by (ALLGOALS Blast_tac);
-qed_spec_mp "new_keys_not_used";
-
-bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
-
-Addsimps [new_keys_not_used, new_keys_not_analzd];
-
-
-(** Lemmas concerning the form of items passed in messages **)
-
-(*Describes the form of K, X and K' when the Server sends this message.*)
-Goal "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
-\ evs : ns_shared |] \
-\ ==> K ~: range shrK & \
-\ X = (Crypt (shrK B) {|Key K, Agent A|}) & \
-\ K' = shrK A";
-by (etac rev_mp 1);
-by (etac ns_shared.induct 1);
-by Auto_tac;
-qed "Says_Server_message_form";
-
-
-(*If the encrypted message appears then it originated with the Server*)
-Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
-\ A ~: bad; evs : ns_shared |] \
-\ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "A_trusts_NS2";
-
-
-Goal "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
-\ A ~: bad; evs : ns_shared |] \
-\ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})";
-by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
-qed "cert_A_form";
-
-
-(*EITHER describes the form of X when the following message is sent,
- OR reduces it to the Fake case.
- Use Says_Server_message_form if applicable.*)
-Goal "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
-\ : set evs; \
-\ evs : ns_shared |] \
-\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \
-\ | X : analz (spies evs)";
-by (case_tac "A : bad" 1);
-by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
- addss (simpset())) 1);
-by (blast_tac (claset() addSDs [cert_A_form]) 1);
-qed "Says_S_message_form";
-
-
-(*For proofs involving analz.*)
-val analz_spies_tac =
- ftac Says_Server_message_form 8 THEN
- ftac Says_S_message_form 5 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac);
-
-
-(****
- The following is to prove theorems of the form
-
- Key K : analz (insert (Key KAB) (spies evs)) ==>
- Key K : analz (spies evs)
-
- A more general formula must be proved inductively.
-****)
-
-
-(*NOT useful in this form, but it says that session keys are not used
- to encrypt messages containing other keys, in the actual protocol.
- We require that agents should behave like this subsequently also.*)
-Goal "[| evs : ns_shared; Kab ~: range shrK |] ==> \
-\ (Crypt KAB X) : parts (spies evs) & \
-\ Key K : parts {X} --> Key K : parts (spies evs)";
-by (parts_induct_tac 1);
-(*Fake*)
-by (blast_tac (claset() addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]) 1);
-(*Base, NS4 and NS5*)
-by Auto_tac;
-result();
-
-
-(** Session keys are not used to encrypt other session keys **)
-
-(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs : ns_shared ==> \
-\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key`KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
-by (etac ns_shared.induct 1);
-by analz_spies_tac;
-by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
-(*Takes 9 secs*)
-by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-
-Goal "[| evs : ns_shared; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(** The session key K uniquely identifies the message **)
-
-Goal "evs : ns_shared ==> \
-\ EX A' NA' B' X'. ALL A NA B X. \
-\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
-\ --> A=A' & NA=NA' & B=B' & X=X'";
-by (etac ns_shared.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by Safe_tac;
-(*NS3*)
-by (ex_strip_tac 2);
-by (Blast_tac 2);
-(*NS2: it can't be a new key*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (Blast_tac 1);
-val lemma = result();
-
-(*In messages of this form, the session key uniquely identifies the rest*)
-Goal "[| Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
-\ Says Server A' \
-\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
-\ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
-by (prove_unique_tac lemma 1);
-qed "unique_session_keys";
-
-
-(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
-
-Goal "[| A ~: bad; B ~: bad; evs : ns_shared |] \
-\ ==> Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, \
-\ Crypt (shrK B) {|Key K, Agent A|}|}) \
-\ : set evs --> \
-\ (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) --> \
-\ Key K ~: analz (spies evs)";
-by (etac ns_shared.induct 1);
-by analz_spies_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [analz_insert_eq, analz_insert_freshK] @
- pushes @ split_ifs)));
-(*Oops*)
-by (blast_tac (claset() addDs [unique_session_keys]) 5);
-(*NS3, replay sub-case*)
-by (Blast_tac 4);
-(*NS2*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(*NS3, Server sub-case*) (**LEVEL 6 **)
-by (clarify_tac (claset() delrules [impCE]) 1);
-by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1);
-by (assume_tac 2);
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
- Crypt_Spy_analz_bad]) 1);
-(*PROOF FAILED if addDs*)
-by (blast_tac (claset() addSDs [unique_session_keys]) 1);
-qed_spec_mp "lemma2";
-
-
-(*Final version: Server's message in the most abstract form*)
-Goal "[| Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : ns_shared \
-\ |] ==> Key K ~: analz (spies evs)";
-by (ftac Says_Server_message_form 1 THEN assume_tac 1);
-by (blast_tac (claset() delrules [notI]
- addIs [lemma2]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(**** Guarantees available at various stages of protocol ***)
-
-A_trusts_NS2 RS Spy_not_see_encrypted_key;
-
-
-(*If the encrypted message appears then it originated with the Server*)
-Goal "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
-\ B ~: bad; evs : ns_shared |] \
-\ ==> EX NA. Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, \
-\ Crypt (shrK B) {|Key K, Agent A|}|}) \
-\ : set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "B_trusts_NS3";
-
-
-Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
-\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs; \
-\ Key K ~: analz (spies evs); \
-\ evs : ns_shared |] \
-\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*NS3*)
-by (Blast_tac 3);
-by (Blast_tac 1);
-(*NS2: contradiction from the assumptions
- Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *)
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-(**LEVEL 7**)
-(*NS4*)
-by (Clarify_tac 1);
-by (not_bad_tac "Ba" 1);
-by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1);
-qed "A_trusts_NS4_lemma";
-
-
-(*This version no longer assumes that K is secure*)
-Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
-\ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
-\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : ns_shared |] \
-\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
-by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma]
- addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
-qed "A_trusts_NS4";
-
-
-(*If the session key has been used in NS4 then somebody has forwarded
- component X in some instance of NS4. Perhaps an interesting property,
- but not needed (after all) for the proofs below.*)
-Goal "[| Crypt K (Nonce NB) : parts (spies evs); \
-\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
-\ : set evs; \
-\ Key K ~: analz (spies evs); \
-\ evs : ns_shared |] \
-\ ==> EX A'. Says A' B X : set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-by (ALLGOALS Clarify_tac);
-by (Blast_tac 1);
-(**LEVEL 7**)
-(*NS2*)
-by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
- addSDs [Crypt_imp_keysFor]) 1);
-(*NS4*)
-by (not_bad_tac "Ba" 1);
-by (Asm_full_simp_tac 1);
-by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1);
-by (ALLGOALS Clarify_tac);
-by (blast_tac (claset() addDs [unique_session_keys]) 1);
-qed "NS4_implies_NS3";
-
-
-Goal "[| B ~: bad; evs : ns_shared |] \
-\ ==> Key K ~: analz (spies evs) --> \
-\ Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, \
-\ Crypt (shrK B) {|Key K, Agent A|}|}) \
-\ : set evs --> \
-\ Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \
-\ Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
-by (parts_induct_tac 1);
-(*NS3*)
-by (blast_tac (claset() addSDs [cert_A_form]) 3);
-(*NS2*)
-by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)]
- addSDs [Crypt_imp_keysFor]) 2);
-by (Blast_tac 1);
-(**LEVEL 5**)
-(*NS5*)
-by (Clarify_tac 1);
-by (not_bad_tac "Aa" 1);
-by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1);
-qed_spec_mp "B_trusts_NS5_lemma";
-
-
-(*Very strong Oops condition reveals protocol's weakness*)
-Goal "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \
-\ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
-\ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: bad; B ~: bad; evs : ns_shared |] \
-\ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs";
-by (dtac B_trusts_NS3 1);
-by (ALLGOALS Clarify_tac);
-by (blast_tac (claset() addSIs [B_trusts_NS5_lemma]
- addDs [Spy_not_see_encrypted_key]) 1);
-qed "B_trusts_NS5";
--- a/src/HOL/Auth/NS_Shared.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Tue Feb 13 13:16:27 2001 +0100
@@ -10,69 +10,387 @@
Proc. Royal Soc. 426 (1989)
*)
-NS_Shared = Shared +
+theory NS_Shared = Shared:
-consts ns_shared :: event list set
+consts ns_shared :: "event list set"
inductive "ns_shared"
- intrs
- (*Initial trace is empty*)
- Nil "[]: ns_shared"
+ intros
+ (*Initial trace is empty*)
+ Nil: "[] \<in> ns_shared"
+ (*The spy MAY say anything he CAN say. We do not expect him to
+ invent new nonces here, but he can also use NS1. Common to
+ all similar protocols.*)
+ Fake: "\<lbrakk>evs \<in> ns_shared; X \<in> synth (analz (spies evs))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evs \<in> ns_shared"
+
+ (*Alice initiates a protocol run, requesting to talk to any B*)
+ NS1: "\<lbrakk>evs1 \<in> ns_shared; Nonce NA \<notin> used evs1\<rbrakk>
+ \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> ns_shared"
+
+ (*Server's response to Alice's message.
+ !! It may respond more than once to A's request !!
+ Server doesn't know who the true sender is, hence the A' in
+ the sender field.*)
+ NS2: "\<lbrakk>evs2 \<in> ns_shared; Key KAB \<notin> used evs2;
+ Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
+ \<Longrightarrow> Says Server A
+ (Crypt (shrK A)
+ \<lbrace>Nonce NA, Agent B, Key KAB,
+ (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
+ # evs2 \<in> ns_shared"
+
+ (*We can't assume S=Server. Agent A "remembers" her nonce.
+ Need A \<noteq> Server because we allow messages to self.*)
+ NS3: "\<lbrakk>evs3 \<in> ns_shared; A \<noteq> Server;
+ Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
+ Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
+ \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
+
+ (*Bob's nonce exchange. He does not know who the message came
+ from, but responds to A because she is mentioned inside.*)
+ NS4: "\<lbrakk>evs4 \<in> ns_shared; Nonce NB \<notin> used evs4;
+ Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
- (*The spy MAY say anything he CAN say. We do not expect him to
- invent new nonces here, but he can also use NS1. Common to
- all similar protocols.*)
- Fake "[| evs: ns_shared; X: synth (analz (spies evs)) |]
- ==> Says Spy B X # evs : ns_shared"
+ (*Alice responds with Nonce NB if she has seen the key before.
+ Maybe should somehow check Nonce NA again.
+ We do NOT send NB-1 or similar as the Spy cannot spoof such things.
+ Letting the Spy add or subtract 1 lets him send \<forall>nonces.
+ Instead we distinguish the messages by sending the nonce twice.*)
+ NS5: "\<lbrakk>evs5 \<in> ns_shared;
+ Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
+ Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+ \<in> set evs5\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
+
+ (*This message models possible leaks of session keys.
+ The two Nonces identify the protocol run: the rule insists upon
+ the true senders in order to make them accurate.*)
+ Oops: "\<lbrakk>evso \<in> ns_shared; Says B A (Crypt K (Nonce NB)) \<in> set evso;
+ Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+ \<in> set evso\<rbrakk>
+ \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
+
+declare knows_Spy_partsEs [elim]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
+ Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] ns_shared.Nil
+ [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
+ THEN ns_shared.NS4, THEN ns_shared.NS5])
+apply possibility
+done
+
+(*This version is similar, while instantiating ?K and ?N to epsilon-terms
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
+ Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
+*)
+
+
+(**** Inductive proofs about ns_shared ****)
+
+(*Forwarding lemmas, to aid simplification*)
- (*Alice initiates a protocol run, requesting to talk to any B*)
- NS1 "[| evs1: ns_shared; Nonce NA ~: used evs1 |]
- ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
- : ns_shared"
+(*For reasoning about the encrypted portion of message NS3*)
+lemma NS3_msg_in_parts_spies:
+ "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
+by blast
+
+(*For reasoning about the Oops message*)
+lemma Oops_parts_spies:
+ "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
+ \<Longrightarrow> K \<in> parts (spies evs)"
+by blast
+
+(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+apply blast+;
+done
+
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+
+(*Nobody can have used non-existent keys!*)
+lemma new_keys_not_used [rule_format, simp]:
+ "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+(*Fake, NS2, NS4, NS5*)
+apply (blast dest!: keysFor_parts_insert)+
+done
+
+
+(** Lemmas concerning the form of items passed in messages **)
+
+(*Describes the form of K, X and K' when the Server sends this message.*)
+lemma Says_Server_message_form:
+ "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> K \<notin> range shrK \<and>
+ X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
+ K' = shrK A"
+by (erule rev_mp, erule ns_shared.induct, auto)
+
- (*Server's response to Alice's message.
- !! It may respond more than once to A's request !!
- Server doesn't know who the true sender is, hence the A' in
- the sender field.*)
- NS2 "[| evs2: ns_shared; Key KAB ~: used evs2;
- Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
- ==> Says Server A
- (Crypt (shrK A)
- {|Nonce NA, Agent B, Key KAB,
- (Crypt (shrK B) {|Key KAB, Agent A|})|})
- # evs2 : ns_shared"
+(*If the encrypted message appears then it originated with the Server*)
+lemma A_trusts_NS2:
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply auto
+done
+
+lemma cert_A_form:
+ "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
+by (blast dest!: A_trusts_NS2 Says_Server_message_form)
+
+(*EITHER describes the form of X when the following message is sent,
+ OR reduces it to the Fake case.
+ Use Says_Server_message_form if applicable.*)
+lemma Says_S_message_form:
+ "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
+ \<or> X \<in> analz (spies evs)"
+apply (frule Says_imp_knows_Spy)
+(*mystery: why is this frule needed?*)
+apply (blast dest: cert_A_form analz.Inj)
+done
+
+(*Alternative version also provable
+lemma Says_S_message_form2:
+ "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
+ \<or> X \<in> analz (spies evs)"
+apply (case_tac "A \<in> bad")
+apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
+by (blast dest!: A_trusts_NS2 Says_Server_message_form)
+*)
+
+
+(****
+ SESSION KEY COMPROMISE THEOREM. To prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
+ Key K \<in> analz (spies evs)
+
+ A more general formula must be proved inductively.
+****)
- (*We can't assume S=Server. Agent A "remembers" her nonce.
- Need A ~= Server because we allow messages to self.*)
- NS3 "[| evs3: ns_shared; A ~= Server;
- Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evs3;
- Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
- ==> Says A B X # evs3 : ns_shared"
+(*NOT useful in this form, but it says that session keys are not used
+ to encrypt messages containing other keys, in the actual protocol.
+ We require that agents should behave like this subsequently also.*)
+lemma "\<lbrakk>evs \<in> ns_shared; Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
+ (Crypt KAB X) \<in> parts (spies evs) \<and>
+ Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+(*Fake*)
+apply (blast dest: parts_insert_subset_Un)
+(*Base, NS4 and NS5*)
+apply auto
+done
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*The equality makes the induction hypothesis easier to apply*)
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> ns_shared \<Longrightarrow>
+ \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+ (Key K \<in> analz (Key`KK \<union> (spies evs))) =
+ (K \<in> KK \<or> Key K \<in> analz (spies evs))"
+apply (erule ns_shared.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (erule_tac [4] Says_S_message_form [THEN disjE])
+apply (analz_freshK)
+apply (spy_analz)
+done
+
+
+lemma analz_insert_freshK:
+ "\<lbrakk>evs \<in> ns_shared; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
+ Key K \<in> analz (insert (Key KAB) (spies evs)) =
+ (K = KAB \<or> Key K \<in> analz (spies evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(** The session key K uniquely identifies the message **)
- (*Bob's nonce exchange. He does not know who the message came
- from, but responds to A because she is mentioned inside.*)
- NS4 "[| evs4: ns_shared; Nonce NB ~: used evs4;
- Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
- ==> Says B A (Crypt K (Nonce NB)) # evs4
- : ns_shared"
+(*In messages of this form, the session key uniquely identifies the rest*)
+lemma unique_session_keys:
+ "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
+ evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
+apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
+apply simp_all
+apply blast+
+done
+
+
+(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
+
+lemma secrecy_lemma [rule_format]:
+ "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
+ Key K \<notin> analz (spies evs)"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (frule_tac [4] Says_S_message_form)
+apply (erule_tac [5] disjE)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
+apply spy_analz (*Fake*)
+apply blast (*NS2*)
+(*NS3, Server sub-case*) (**LEVEL 6 **)
+apply clarify
+apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
+apply assumption
+apply (blast dest: unique_session_keys)+ (*also proves Oops*)
+done
+
+
+(*Final version: Server's message in the most abstract form*)
+lemma Spy_not_see_encrypted_key:
+ "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Key K \<notin> analz (spies evs)"
+apply (frule Says_Server_message_form, assumption)
+apply (auto dest: Says_Server_message_form secrecy_lemma)
+done
+
+
+(**** Guarantees available at various stages of protocol ***)
- (*Alice responds with Nonce NB if she has seen the key before.
- Maybe should somehow check Nonce NA again.
- We do NOT send NB-1 or similar as the Spy cannot spoof such things.
- Letting the Spy add or subtract 1 lets him send ALL nonces.
- Instead we distinguish the messages by sending the nonce twice.*)
- NS5 "[| evs5: ns_shared;
- Says B' A (Crypt K (Nonce NB)) : set evs5;
- Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evs5 |]
- ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
-
- (*This message models possible leaks of session keys.
- The two Nonces identify the protocol run: the rule insists upon
- the true senders in order to make them accurate.*)
- Oops "[| evso: ns_shared; Says B A (Crypt K (Nonce NB)) : set evso;
- Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
- : set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
+(*If the encrypted message appears then it originated with the Server*)
+lemma B_trusts_NS3:
+ "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+ B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> \<exists>NA. Says Server A
+ (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply auto
+done
+
+
+lemma A_trusts_NS4_lemma [rule_format]:
+ "evs \<in> ns_shared \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
+ Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ Says B A (Crypt K (Nonce NB)) \<in> set evs"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply simp_all
+apply blast (*Fake*)
+(*NS2: contradiction from the assumptions
+ Key K \<notin> used evs2 and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
+apply (force dest!: Crypt_imp_keysFor)
+apply blast (*NS3*)
+(*NS4*)
+apply clarify;
+apply (frule Says_imp_knows_Spy [THEN analz.Inj])
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
+ B_trusts_NS3 unique_session_keys)
+done
+
+(*This version no longer assumes that K is secure*)
+lemma A_trusts_NS4:
+ "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
+ Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+ \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
+by (blast intro: A_trusts_NS4_lemma
+ dest: A_trusts_NS2 Spy_not_see_encrypted_key)
+
+(*If the session key has been used in NS4 then somebody has forwarded
+ component X in some instance of NS4. Perhaps an interesting property,
+ but not needed (after all) for the proofs below.*)
+theorem NS4_implies_NS3 [rule_format]:
+ "evs \<in> ns_shared \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
+ Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+ (\<exists>A'. Says A' B X \<in> set evs)"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply (simp_all add: ex_disj_distrib)
+apply blast (*Fake*)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
+apply blast (*NS3*)
+(*NS4*)
+apply (case_tac "Ba \<in> bad")
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
+apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3],
+ assumption+)
+apply (blast dest: unique_session_keys)
+done
+
+
+lemma B_trusts_NS5_lemma [rule_format]:
+ "\<lbrakk>B \<notin> bad; evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
+ Key K \<notin> analz (spies evs) \<longrightarrow>
+ Says Server A
+ (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
+ Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+ Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply simp_all
+apply blast (*Fake*)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
+apply (blast dest!: cert_A_form) (*NS3*)
+(**LEVEL 5**)
+(*NS5*)
+apply clarify
+apply (case_tac "Aa \<in> bad")
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
+apply (blast dest: A_trusts_NS2 unique_session_keys)
+done
+
+
+(*Very strong Oops condition reveals protocol's weakness*)
+lemma B_trusts_NS5:
+ "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
+ Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+ \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk>
+ \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
+apply (drule B_trusts_NS3, clarify+)
+apply (blast intro: B_trusts_NS5_lemma
+ dest: dest: Spy_not_see_encrypted_key)
+(*surprisingly delicate proof due to quantifier interactions*)
+done
end
--- a/src/HOL/Auth/OtwayRees.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Feb 13 13:16:27 2001 +0100
@@ -169,26 +169,15 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : otway ==> \
-\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
-\ B=B' & NA=NA' & NB=NB' & X=X'";
-by (etac otway.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*Remaining cases: OR3 and OR4*)
-by (ex_strip_tac 2);
-by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-val lemma = result();
-
Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*Remaining cases: OR3 and OR4*)
+by (REPEAT (Blast_tac 1));
qed "unique_session_keys";
@@ -216,23 +205,15 @@
(** The Nonce NA uniquely identifies A's message. **)
-Goal "[| evs : otway; A ~: bad |] \
-\ ==> EX B'. ALL B. \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) \
-\ --> B = B'";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-(*OR1: creation of new Nonce. Move assertion into global context*)
-by (expand_case_tac "NA = ?y" 1);
-by (Blast_tac 1);
-val lemma = result();
-
Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \
\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \
\ evs : otway; A ~: bad |] \
\ ==> B = C";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Fake, OR1*)
+by (REPEAT (Blast_tac 1));
qed "unique_NA";
@@ -363,23 +344,15 @@
(** The Nonce NB uniquely identifies B's message. **)
-Goal "[| evs : otway; B ~: bad |] \
-\ ==> EX NA' A'. ALL NA A. \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs) \
-\ --> NA = NA' & A = A'";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-(*OR2: creation of new Nonce. Move assertion into global context*)
-by (expand_case_tac "NB = ?y" 1);
-by (Blast_tac 1);
-val lemma = result();
-
Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \
\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \
\ evs : otway; B ~: bad |] \
\ ==> NC = NA & C = A";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Fake, OR2*)
+by (REPEAT (Blast_tac 1));
qed "unique_NB";
(*If the encrypted message appears, and B has used Nonce NB,
@@ -401,15 +374,7 @@
(*OR4*)
by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2);
(*OR3*)
-(*Provable in 38s by the single command
- by (blast_tac (claset() addDs [unique_NB] addEs[nonce_OR1_OR2_E]) 1);
-*)
-by (safe_tac (claset() delrules [disjCI, impCE]));
-by (Blast_tac 3);
-by (blast_tac (claset() addSDs [unique_NB]
- delrules [impCE] (*stop split-up*)) 2);
-by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
- delrules [conjI] (*stop split-up*)) 1);
+by (blast_tac (claset() addDs [unique_NB] addEs [nonce_OR1_OR2_E]) 1);
qed_spec_mp "NB_Crypt_imp_Server_msg";
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Feb 13 13:16:27 2001 +0100
@@ -163,25 +163,6 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : otway ==> \
-\ EX A' B' NA' NB'. ALL A B NA NB. \
-\ Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs \
-\ --> A=A' & B=B' & NA=NA' & NB=NB'";
-by (etac otway.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*Remaining cases: OR3 and OR4*)
-by (ex_strip_tac 2);
-by (Blast_tac 2);
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-val lemma = result();
-
-
Goal "[| Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
@@ -192,7 +173,12 @@
\ : set evs; \
\ evs : otway |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*Remaining cases: OR3 and OR4*)
+by (REPEAT (Blast_tac 1));
qed "unique_session_keys";
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Feb 13 13:16:27 2001 +0100
@@ -174,26 +174,15 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : otway ==> \
-\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
-\ B=B' & NA=NA' & NB=NB' & X=X'";
-by (etac otway.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*Remaining cases: OR3 and OR4*)
-by (ex_strip_tac 2);
-by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message, and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-val lemma = result();
-
Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \
\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*Remaining cases: OR3 and OR4*)
+by (REPEAT (Blast_tac 1));
qed "unique_session_keys";
--- a/src/HOL/Auth/Public.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,177 +0,0 @@
-(* Title: HOL/Auth/Public
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Theory of Public Keys (common to all symmetric-key protocols)
-
-Server keys; initial states of agents; new nonces and keys; function "sees"
-*)
-
-(*** Basic properties of pubK & priK ***)
-
-AddIffs [inj_pubK RS inj_eq];
-
-Goal "(priK A = priK B) = (A=B)";
-by Safe_tac;
-by (dres_inst_tac [("f","invKey")] arg_cong 1);
-by (Full_simp_tac 1);
-qed "priK_inj_eq";
-
-AddIffs [priK_inj_eq];
-AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
-
-Goalw [isSymKey_def] "~ isSymKey (pubK A)";
-by (Simp_tac 1);
-qed "not_isSymKey_pubK";
-
-Goalw [isSymKey_def] "~ isSymKey (priK A)";
-by (Simp_tac 1);
-qed "not_isSymKey_priK";
-
-AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
-
-
-(** "Image" equations that hold for injective functions **)
-
-Goal "(invKey x : invKey`A) = (x:A)";
-by Auto_tac;
-qed "invKey_image_eq";
-
-(*holds because invKey is injective*)
-Goal "(pubK x : pubK`A) = (x:A)";
-by Auto_tac;
-qed "pubK_image_eq";
-
-Goal "(priK x ~: pubK`A)";
-by Auto_tac;
-qed "priK_pubK_image_eq";
-Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
-
-
-(** Rewrites should not refer to initState(Friend i)
- -- not in normal form! **)
-
-Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
-by (induct_tac "C" 1);
-by (auto_tac (claset() addIs [range_eqI], simpset()));
-qed "keysFor_parts_initState";
-Addsimps [keysFor_parts_initState];
-
-
-(*** Function "spies" ***)
-
-(*Agents see their own private keys!*)
-Goal "Key (priK A) : initState A";
-by (induct_tac "A" 1);
-by Auto_tac;
-qed "priK_in_initState";
-AddIffs [priK_in_initState];
-
-(*All public keys are visible*)
-Goal "Key (pubK A) : spies evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, knows_Cons]
- addsplits [expand_event_case])));
-qed_spec_mp "spies_pubK";
-
-(*Spy sees private keys of bad agents!*)
-Goal "A: bad ==> Key (priK A) : spies evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, knows_Cons]
- addsplits [expand_event_case])));
-qed "Spy_spies_bad";
-
-AddIffs [spies_pubK, spies_pubK RS analz.Inj];
-AddSIs [Spy_spies_bad];
-
-
-(*For not_bad_tac*)
-Goal "[| 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_bad";
-
-(*Prove that the agent is uncompromised by the confidentiality of
- a component of a message she's said.*)
-fun not_bad_tac s =
- case_tac ("(" ^ s ^ ") : bad") THEN'
- SELECT_GOAL
- (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_bad 1 THEN assume_tac 1)
- (has_fewer_prems 1, size_of_thm)
- Safe_tac);
-
-
-(*** Fresh nonces ***)
-
-Goal "Nonce N ~: parts (initState B)";
-by (induct_tac "B" 1);
-by Auto_tac;
-qed "Nonce_notin_initState";
-AddIffs [Nonce_notin_initState];
-
-Goal "Nonce N ~: used []";
-by (simp_tac (simpset() addsimps [used_Nil]) 1);
-qed "Nonce_notin_used_empty";
-Addsimps [Nonce_notin_used_empty];
-
-
-(*** Supply fresh nonces for possibility theorems. ***)
-
-(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-Goal "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]
- addsplits [expand_event_case])));
-by Safe_tac;
-by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
-by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
-val lemma = result();
-
-Goal "EX N. Nonce N ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (Blast_tac 1);
-qed "Nonce_supply1";
-
-Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (rtac someI 1);
-by (Fast_tac 1);
-qed "Nonce_supply";
-
-(*Tactic for possibility theorems*)
-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, Nonce_supply]));
-
-
-(*** Specialized rewriting for the analz_image_... theorems ***)
-
-Goal "insert (Key K) H = Key ` {K} Un H";
-by (Blast_tac 1);
-qed "insert_Key_singleton";
-
-Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
-by (Blast_tac 1);
-qed "insert_Key_image";
-
-(*Reverse the normal simplification of "image" to build up (not break down)
- the set of keys. Based on analz_image_freshK_ss, but simpler.*)
-val analz_image_keys_ss =
- simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
- addsimps [image_insert RS sym, image_Un RS sym,
- rangeI,
- insert_Key_singleton,
- insert_Key_image, Un_assoc RS sym];
-
--- a/src/HOL/Auth/Public.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Public.thy Tue Feb 13 13:16:27 2001 +0100
@@ -8,30 +8,39 @@
Private and public keys; initial states of agents
*)
-Public = Event +
+theory Public = Event
+files ("Public_lemmas.ML"):
consts
- pubK :: agent => key
+ pubK :: "agent => key"
syntax
- priK :: agent => key
+ priK :: "agent => key"
translations (*BEWARE! expressions like (inj priK) will NOT work!*)
"priK x" == "invKey(pubK x)"
primrec
(*Agents know their private key and all public keys*)
- initState_Server "initState Server =
+ initState_Server: "initState Server =
insert (Key (priK Server)) (Key ` range pubK)"
- initState_Friend "initState (Friend i) =
+ initState_Friend: "initState (Friend i) =
insert (Key (priK (Friend i))) (Key ` range pubK)"
- initState_Spy "initState Spy =
+ initState_Spy: "initState Spy =
(Key`invKey`pubK`bad) Un (Key ` range pubK)"
-rules
+axioms
(*Public keys are disjoint, and never clash with private keys*)
- inj_pubK "inj pubK"
- priK_neq_pubK "priK A ~= pubK B"
+ inj_pubK: "inj pubK"
+ priK_neq_pubK: "priK A ~= pubK B"
+
+use "Public_lemmas.ML"
+
+(*Specialized methods*)
+
+method_setup possibility = {*
+ Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+ "for proving possibility theorems"
end
--- a/src/HOL/Auth/Recur.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Recur.ML Tue Feb 13 13:16:27 2001 +0100
@@ -20,9 +20,9 @@
(*Simplest case: Alice goes directly to the server*)
-Goal "EX K NA. EX evs: recur. \
+Goal "\\<exists>K NA. \\<exists>evs \\<in> recur. \
\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\ END|} : set evs";
+\ END|} \\<in> set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2);
by possibility_tac;
@@ -30,9 +30,9 @@
(*Case two: Alice, Bob and the server*)
-Goal "EX K. EX NA. EX evs: recur. \
+Goal "\\<exists>K. \\<exists>NA. \\<exists>evs \\<in> recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ END|} : set evs";
+\ END|} \\<in> set evs";
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -46,16 +46,15 @@
(*Case three: Alice, Bob, Charlie and the server
TOO SLOW to run every time!
-Goal "EX K. EX NA. EX evs: recur. \
+Goal "\\<exists>K. \\<exists>NA. \\<exists>evs \\<in> recur. \
\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\ END|} : set evs";
+\ END|} \\<in> set evs";
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
(respond.One RS respond.Cons RS respond.Cons RSN
(3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-(*SLOW: 33 seconds*)
by basic_possibility_tac;
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
ORELSE
@@ -65,19 +64,12 @@
(**** Inductive proofs about recur ****)
-
-Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
-by (etac respond.induct 1);
-by (ALLGOALS Simp_tac);
-qed "respond_Key_in_parts";
-
-Goal "(PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
+Goal "(PA,RB,KAB) \\<in> respond evs ==> Key KAB \\<notin> used evs";
by (etac respond.induct 1);
by (REPEAT (assume_tac 1));
qed "respond_imp_not_used";
-Goal "[| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
-\ ==> Key K ~: used evs";
+Goal "[| Key K \\<in> parts {RB}; (PB,RB,K') \\<in> respond evs |] ==> Key K \\<notin> used evs";
by (etac rev_mp 1);
by (etac respond.induct 1);
by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used],
@@ -85,7 +77,7 @@
qed_spec_mp "Key_in_parts_respond";
(*Simple inductive reasoning about responses*)
-Goal "(PA,RB,KAB) : respond evs ==> RB : responses evs";
+Goal "(PA,RB,KAB) \\<in> respond evs ==> RB \\<in> responses evs";
by (etac respond.induct 1);
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
qed "respond_imp_responses";
@@ -95,7 +87,7 @@
val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
-Goal "Says C' B {|Crypt K X, X', RA|} : set evs ==> RA : analz (spies evs)";
+Goal "Says C' B {|Crypt K X, X', RA|} \\<in> set evs ==> RA \\<in> analz (spies evs)";
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
qed "RA4_analz_spies";
@@ -109,7 +101,7 @@
bind_thm ("RA4_parts_spies",
RA4_analz_spies RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X \\<notin> parts (spies evs).*)
fun parts_induct_tac i =
EVERY [etac recur.induct i,
ftac RA4_parts_spies (i+5),
@@ -118,13 +110,13 @@
prove_simple_subgoals_tac i];
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
sends messages containing X! **)
(** Spy never sees another agent's shared key! (unless it's bad at start) **)
-Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs \\<in> recur ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
by (parts_induct_tac 1);
by Auto_tac;
(*RA3*)
@@ -133,7 +125,7 @@
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs \\<in> recur ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -145,28 +137,22 @@
(** Nobody can have used non-existent keys! **)
(*The special case of H={} has the same proof*)
-Goal "[| K : keysFor (parts (insert RB H)); RB : responses evs |] \
-\ ==> K : range shrK | K : keysFor (parts H)";
+Goal "[| K \\<in> keysFor (parts (insert RB H)); RB \\<in> responses evs |] \
+\ ==> K \\<in> range shrK | K \\<in> keysFor (parts H)";
by (etac rev_mp 1);
by (etac responses.induct 1);
by Auto_tac;
qed_spec_mp "Key_in_keysFor_parts";
-Goal "evs : recur ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs \\<in> recur ==> Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
qed_spec_mp "new_keys_not_used";
-
-
-bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
-
-Addsimps [new_keys_not_used, new_keys_not_analzd];
+Addsimps [new_keys_not_used];
@@ -175,7 +161,7 @@
(*For proofs involving analz.*)
val analz_spies_tac =
dtac RA2_analz_spies 4 THEN
- ftac respond_imp_responses 5 THEN
+ ftac respond_imp_responses 5 THEN
dtac RA4_analz_spies 6;
@@ -184,22 +170,22 @@
(*Version for "responses" relation. Handles case RA3 in the theorem below.
Note that it holds for *any* set H (not just "spies evs")
satisfying the inductive hypothesis.*)
-Goal "[| RB : responses evs; \
-\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key`KK Un H)) = \
-\ (K : KK | Key K : analz H) |] \
-\ ==> ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (insert RB (Key`KK Un H))) = \
-\ (K : KK | Key K : analz (insert RB H))";
+Goal "[| RB \\<in> responses evs; \
+\ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \
+\ (Key K \\<in> analz (Key`KK Un H)) = \
+\ (K \\<in> KK | Key K \\<in> analz H) |] \
+\ ==> \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \
+\ (Key K \\<in> analz (insert RB (Key`KK Un H))) = \
+\ (K \\<in> KK | Key K \\<in> analz (insert RB H))";
by (etac responses.induct 1);
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
qed "resp_analz_image_freshK_lemma";
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
-Goal "evs : recur ==> \
-\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key`KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+Goal "evs \\<in> recur ==> \
+\ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \
+\ (Key K \\<in> analz (Key`KK Un (spies evs))) = \
+\ (K \\<in> KK | Key K \\<in> analz (spies evs))";
by (etac recur.induct 1);
by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
@@ -214,25 +200,25 @@
(*Instance of the lemma with H replaced by (spies evs):
- [| RB : responses evs; evs : recur; |]
- ==> KK <= - (range shrK) -->
- Key K : analz (insert RB (Key`KK Un spies evs)) =
- (K : KK | Key K : analz (insert RB (spies evs)))
+ [| RB \\<in> responses evs; evs \\<in> recur; |]
+ ==> KK \\<subseteq> - (range shrK) -->
+ Key K \\<in> analz (insert RB (Key`KK Un spies evs)) =
+ (K \\<in> KK | Key K \\<in> analz (insert RB (spies evs)))
*)
bind_thm ("resp_analz_image_freshK",
raw_analz_image_freshK RSN
(2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
-Goal "[| evs : recur; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+Goal "[| evs \\<in> recur; KAB \\<notin> range shrK |] ==> \
+\ Key K \\<in> analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K \\<in> analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
(*Everything that's hashed is already in past traffic. *)
-Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] ==> X : parts (spies evs)";
+Goal "[| Hash {|Key(shrK A), X|} \\<in> parts (spies evs); \
+\ evs \\<in> recur; A \\<notin> bad |] ==> X \\<in> parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3 requires a further induction*)
@@ -249,28 +235,19 @@
Unicity is not used in other proofs but is desirable in its own right.
**)
-Goal "[| evs : recur; A ~: bad |] \
-\ ==> EX B' P'. ALL B P. \
-\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
-\ --> B=B' & P=P'";
+Goal
+ "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \\<in> parts (spies evs); \
+\ Hash {|Key(shrK A), Agent A, B',NA, P'|} \\<in> parts (spies evs); \
+\ evs \\<in> recur; A \\<notin> bad |] \
+\ ==> B=B' & P=P'";
+by (etac rev_mp 1);
+by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Blast_tac 1);
by (etac responses.induct 3);
-by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib])));
-by (clarify_tac (claset() addSEs partsEs) 1);
-(*RA1,2: creation of new Nonce. Move assertion into global context*)
-by (ALLGOALS (expand_case_tac "NA = ?y"));
-by (REPEAT_FIRST (ares_tac [exI]));
+by (Asm_full_simp_tac 4);
+(*RA1,2: creation of new Nonce*)
by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1));
-val lemma = result();
-
-Goalw [HPair_def]
- "[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \
-\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] \
-\ ==> B=B' & P=P'";
-by (REPEAT (eresolve_tac partsEs 1));
-by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -278,8 +255,8 @@
(relations "respond" and "responses")
***)
-Goal "[| RB : responses evs; evs : recur |] \
-\ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
+Goal "[| RB \\<in> responses evs; evs \\<in> recur |] \
+\ ==> (Key (shrK B) \\<in> analz (insert RB (spies evs))) = (B:bad)";
by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
@@ -289,12 +266,12 @@
Addsimps [shrK_in_analz_respond];
-Goal "[| RB : responses evs; \
-\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key`KK Un H)) = \
-\ (K : KK | Key K : analz H) |] \
-\ ==> (Key K : analz (insert RB H)) --> \
-\ (Key K : parts{RB} | Key K : analz H)";
+Goal "[| RB \\<in> responses evs; \
+\ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \
+\ (Key K \\<in> analz (Key`KK Un H)) = \
+\ (K \\<in> KK | Key K \\<in> analz H) |] \
+\ ==> (Key K \\<in> analz (insert RB H)) --> \
+\ (Key K \\<in> parts{RB} | Key K \\<in> analz H)";
by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
@@ -310,38 +287,32 @@
(*The last key returned by respond indeed appears in a certificate*)
-Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
-\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
+Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \\<in> respond evs \
+\ ==> Crypt (shrK A) {|Key K, B, NA|} \\<in> parts {RA}";
by (etac respond.elim 1);
by (ALLGOALS Asm_full_simp_tac);
qed "respond_certificate";
-
-Goal "(PB,RB,KXY) : respond evs \
-\ ==> EX A' B'. ALL A B N. \
-\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
-\ --> (A'=A & B'=B) | (A'=B & B'=A)";
+(*This unicity proof differs from all the others in the HOL/Auth directory.
+ The conclusion isn't quite unicity but duplicity, in that there are two
+ possibilities. Also, the presence of two different matching messages in
+ the inductive step complicates the case analysis. Unusually for such proofs,
+ the quantifiers appear to be necessary.*)
+Goal "(PB,RB,KXY) \\<in> respond evs ==> \
+\ \\<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \\<in> parts {RB} --> \
+\ (\\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \\<in> parts {RB} --> \
+\ (A'=A & B'=B) | (A'=B & B'=A))";
by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*Base case*)
-by (Blast_tac 1);
-by Safe_tac;
-by (expand_case_tac "K = KBC" 1);
-by (dtac respond_Key_in_parts 1);
-by (blast_tac (claset() addSIs [exI]
- addDs [Key_in_parts_respond]) 1);
-by (expand_case_tac "K = KAB" 1);
-by (REPEAT (ares_tac [exI] 2));
-by (ex_strip_tac 1);
-by (dtac respond_certificate 1);
-by (Blast_tac 1);
-val lemma = result();
+by (blast_tac (claset() addDs [respond_certificate]) 1);
+qed_spec_mp "unique_lemma";
-Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
-\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
-\ (PB,RB,KXY) : respond evs |] \
+Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} \\<in> parts {RB}; \
+\ Crypt (shrK A') {|Key K, Agent B', N'|} \\<in> parts {RB}; \
+\ (PB,RB,KXY) \\<in> respond evs |] \
\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1);
+by (rtac unique_lemma 1);
+by Auto_tac;
qed "unique_session_keys";
@@ -349,10 +320,10 @@
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
-Goal "[| (PB,RB,KAB) : respond evs; evs : recur |] \
-\ ==> ALL A A' N. A ~: bad & A' ~: bad --> \
-\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
-\ Key K ~: analz (insert RB (spies evs))";
+Goal "[| (PB,RB,KAB) \\<in> respond evs; evs \\<in> recur |] \
+\ ==> \\<forall>A A' N. A \\<notin> bad & A' \\<notin> bad --> \
+\ Crypt (shrK A) {|Key K, Agent A', N|} \\<in> parts{RB} --> \
+\ Key K \\<notin> analz (insert RB (spies evs))";
by (etac respond.induct 1);
by (ftac respond_imp_responses 2);
by (ftac respond_imp_not_used 2);
@@ -367,11 +338,10 @@
by (Blast_tac 1);
by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
by (ALLGOALS Clarify_tac);
-by (blast_tac (claset() addSDs [resp_analz_insert]
- addIs [impOfSubs analz_subset_parts]) 3);
+by (blast_tac (claset() addSDs [resp_analz_insert]) 3);
by (blast_tac (claset() addSDs [respond_certificate]) 2);
by (Asm_full_simp_tac 1);
-(*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
+(*by unicity, either B=Aa or B=A', a contradiction if B \\<in> bad*)
by (blast_tac
(claset() addSEs [MPair_parts]
addDs [parts.Body,
@@ -379,9 +349,9 @@
qed_spec_mp "respond_Spy_not_see_session_key";
-Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
-\ A ~: bad; A' ~: bad; evs : recur |] \
-\ ==> Key K ~: analz (spies evs)";
+Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} \\<in> parts (spies evs); \
+\ A \\<notin> bad; A' \\<notin> bad; evs \\<in> recur |] \
+\ ==> Key K \\<notin> analz (spies evs)";
by (etac rev_mp 1);
by (etac recur.induct 1);
by analz_spies_tac;
@@ -389,9 +359,9 @@
(asm_simp_tac
(simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK])));
(*RA4*)
-by (spy_analz_tac 5);
+by (Blast_tac 5);
(*RA2*)
-by (spy_analz_tac 3);
+by (Blast_tac 3);
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -411,9 +381,9 @@
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
-Goal "[| Hash {|Key (shrK B), M|} : parts (insert RB H); \
-\ (PB,RB,K) : respond evs |] \
-\ ==> Hash {|Key (shrK B), M|} : parts H";
+Goal "[| Hash {|Key (shrK B), M|} \\<in> parts (insert RB H); \
+\ (PB,RB,K) \\<in> respond evs |] \
+\ ==> Hash {|Key (shrK B), M|} \\<in> parts H";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
by Auto_tac;
@@ -424,9 +394,9 @@
it can say nothing about how recent A's message is. It might later be
used to prove B's presence to A at the run's conclusion.*)
Goalw [HPair_def]
- "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
-\ A ~: bad; evs : recur |] \
-\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
+ "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \\<in> parts(spies evs); \
+\ A \\<notin> bad; evs \\<in> recur |] \
+\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \\<in> set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Blast_tac 1);
@@ -440,10 +410,10 @@
(*Certificates can only originate with the Server.*)
-Goal "[| Crypt (shrK A) Y : parts (spies evs); \
-\ A ~: bad; evs : recur |] \
-\ ==> EX C RC. Says Server C RC : set evs & \
-\ Crypt (shrK A) Y : parts {RC}";
+Goal "[| Crypt (shrK A) Y \\<in> parts (spies evs); \
+\ A \\<notin> bad; evs \\<in> recur |] \
+\ ==> \\<exists>C RC. Says Server C RC \\<in> set evs & \
+\ Crypt (shrK A) Y \\<in> parts {RC}";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Blast_tac 1);
--- a/src/HOL/Auth/Shared.ML Tue Feb 13 01:32:54 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-(* Title: HOL/Auth/Shared
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Theory of Shared Keys (common to all symmetric-key protocols)
-
-Shared, long-term keys; initial states of agents
-*)
-
-(*** Basic properties of shrK ***)
-
-(*Injectiveness: Agents' long-term keys are distinct.*)
-AddIffs [inj_shrK RS inj_eq];
-
-(* invKey(shrK A) = shrK A *)
-Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
-
-(** Rewrites should not refer to initState(Friend i)
- -- not in normal form! **)
-
-Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
-by (induct_tac "C" 1);
-by Auto_tac;
-qed "keysFor_parts_initState";
-Addsimps [keysFor_parts_initState];
-
-(*Specialized to shared-key model: no need for addss in protocol proofs*)
-Goal "[| K: keysFor (parts (insert X H)); X : synth (analz H) |] \
-\ ==> K : keysFor (parts H) | Key K : parts H";
-by (force_tac
- (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- impOfSubs (analz_subset_parts RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts],
- simpset()) 1);
-qed "keysFor_parts_insert";
-
-Goal "Crypt K X : H ==> K : keysFor H";
-by (dtac Crypt_imp_invKey_keysFor 1);
-by (Asm_full_simp_tac 1);
-qed "Crypt_imp_keysFor";
-
-
-(*** Function "knows" ***)
-
-(*Spy sees shared keys of agents!*)
-Goal "A: bad ==> Key (shrK A) : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, knows_Cons]
- addsplits [expand_event_case])));
-qed "Spy_knows_Spy_bad";
-AddSIs [Spy_knows_Spy_bad];
-
-(*For not_bad_tac*)
-Goal "[| Crypt (shrK A) X : analz (knows Spy evs); A: bad |] \
-\ ==> X : analz (knows Spy evs)";
-by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1);
-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_bad_tac s =
- case_tac ("(" ^ s ^ ") : bad") THEN'
- SELECT_GOAL
- (REPEAT_DETERM (etac exE 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_bad 1 THEN assume_tac 1)
- (has_fewer_prems 1, size_of_thm)
- (Step_tac 1));
-
-
-(** Fresh keys never clash with long-term shared keys **)
-
-(*Agents see their own shared keys!*)
-Goal "Key (shrK A) : initState A";
-by (induct_tac "A" 1);
-by Auto_tac;
-qed "shrK_in_initState";
-AddIffs [shrK_in_initState];
-
-Goal "Key (shrK A) : used evs";
-by (rtac initState_into_used 1);
-by (Blast_tac 1);
-qed "shrK_in_used";
-AddIffs [shrK_in_used];
-
-(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
- from long-term shared keys*)
-Goal "Key K ~: used evs ==> K ~: range shrK";
-by (Blast_tac 1);
-qed "Key_not_used";
-
-Goal "Key K ~: used evs ==> shrK B ~= K";
-by (Blast_tac 1);
-qed "shrK_neq";
-
-Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
-
-
-(*** Fresh nonces ***)
-
-Goal "Nonce N ~: parts (initState B)";
-by (induct_tac "B" 1);
-by Auto_tac;
-qed "Nonce_notin_initState";
-AddIffs [Nonce_notin_initState];
-
-Goal "Nonce N ~: used []";
-by (simp_tac (simpset() addsimps [used_Nil]) 1);
-qed "Nonce_notin_used_empty";
-Addsimps [Nonce_notin_used_empty];
-
-
-(*** Supply fresh nonces for possibility theorems. ***)
-
-(*In any trace, there is an upper bound N on the greatest nonce in use.*)
-Goal "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]
- addsplits [expand_event_case])));
-by Safe_tac;
-by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
-by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
-val lemma = result();
-
-Goal "EX N. Nonce N ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (Blast_tac 1);
-qed "Nonce_supply1";
-
-Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
-by (cut_inst_tac [("evs","evs")] lemma 1);
-by (cut_inst_tac [("evs","evs'")] lemma 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","N")] exI 1);
-by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
-by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
- less_Suc_eq_le]) 1);
-qed "Nonce_supply2";
-
-Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
-\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
-by (cut_inst_tac [("evs","evs")] lemma 1);
-by (cut_inst_tac [("evs","evs'")] lemma 1);
-by (cut_inst_tac [("evs","evs''")] lemma 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","N")] exI 1);
-by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
-by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
-by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
- less_Suc_eq_le]) 1);
-qed "Nonce_supply3";
-
-Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
-by (rtac (lemma RS exE) 1);
-by (rtac someI 1);
-by (Blast_tac 1);
-qed "Nonce_supply";
-
-(*** Supply fresh keys for possibility theorems. ***)
-
-Goal "EX K. Key K ~: used evs";
-by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
-by (Blast_tac 1);
-qed "Key_supply1";
-
-Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
-by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
-by (etac exE 1);
-by (cut_inst_tac [("evs","evs'")]
- (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
-by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
-qed "Key_supply2";
-
-Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
-\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
-by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
-by (etac exE 1);
-(*Blast_tac requires instantiation of the keys for some reason*)
-by (cut_inst_tac [("evs","evs'"), ("a1","K")]
- (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
-by (etac exE 1);
-by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")]
- (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
-by (Blast_tac 1);
-qed "Key_supply3";
-
-Goal "Key (@ K. Key K ~: used evs) ~: used evs";
-by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
-by (rtac someI 1);
-by (Blast_tac 1);
-qed "Key_supply";
-
-(*** Tactics for possibility theorems ***)
-
-(*Omitting used_Says makes the tactic much faster: it leaves expressions
- such as Nonce ?N ~: used evs that match Nonce_supply*)
-fun possibility_tac st = st |>
- (REPEAT
- (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets]
- setSolver safe_solver))
- THEN
- REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
-
-(*For harder protocols (such as Recur) where we have to set up some
- nonces and keys initially*)
-fun basic_possibility_tac st = st |>
- REPEAT
- (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
- THEN
- REPEAT_FIRST (resolve_tac [refl, conjI]));
-
-
-(*** Specialized rewriting for analz_insert_freshK ***)
-
-Goal "A <= - (range shrK) ==> shrK x ~: A";
-by (Blast_tac 1);
-qed "subset_Compl_range";
-
-Goal "insert (Key K) H = Key ` {K} Un H";
-by (Blast_tac 1);
-qed "insert_Key_singleton";
-
-Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C";
-by (Blast_tac 1);
-qed "insert_Key_image";
-
-(*Reverse the normal simplification of "image" to build up (not break down)
- the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to
- erase occurrences of forwarded message components (X).*)
-val analz_image_freshK_ss =
- simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
- addsimps [image_insert RS sym, image_Un RS sym,
- analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
- insert_Key_singleton, subset_Compl_range,
- Key_not_used, insert_Key_image, Un_assoc RS sym]
- @disj_comms;
-
-(*Lemma for the trivial direction of the if-and-only-if*)
-Goal "(Key K : analz (Key`nE Un H)) --> (K : nE | Key K : analz H) ==> \
-\ (Key K : analz (Key`nE Un H)) = (K : nE | Key K : analz H)";
-by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
-qed "analz_image_freshK_lemma";
--- a/src/HOL/Auth/Shared.thy Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Shared.thy Tue Feb 13 13:16:27 2001 +0100
@@ -8,29 +8,51 @@
Shared, long-term keys; initial states of agents
*)
-Shared = Event + Finite +
+theory Shared = Event
+files ("Shared_lemmas.ML"):
consts
- shrK :: agent => key (*symmetric keys*)
+ shrK :: "agent => key" (*symmetric keys*)
-rules
- isSym_keys "isSymKey K" (*All keys are symmetric*)
- inj_shrK "inj shrK" (*No two agents have the same long-term key*)
+axioms
+ isSym_keys: "isSymKey K" (*All keys are symmetric*)
+ inj_shrK: "inj shrK" (*No two agents have the same long-term key*)
primrec
(*Server knows all long-term keys; other agents know only their own*)
- initState_Server "initState Server = Key ` range shrK"
- initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}"
- initState_Spy "initState Spy = Key`shrK`bad"
+ initState_Server: "initState Server = Key ` range shrK"
+ initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}"
+ initState_Spy: "initState Spy = Key`shrK`bad"
-rules
+axioms
(*Unlike the corresponding property of nonces, this cannot be proved.
We have infinitely many agents and there is nothing to stop their
long-term keys from exhausting all the natural numbers. The axiom
assumes that their keys are dispersed so as to leave room for infinitely
many fresh session keys. We could, alternatively, restrict agents to
an unspecified finite number.*)
- Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
+ Key_supply_ax: "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
+
+use "Shared_lemmas.ML"
+
+(*Lets blast_tac perform this step without needing the simplifier*)
+lemma invKey_shrK_iff [iff]:
+ "(Key (invKey K) \\<in> X) = (Key K \\<in> X)"
+by auto;
+
+(*Specialized methods*)
+
+method_setup analz_freshK = {*
+ Method.no_args
+ (Method.METHOD
+ (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]),
+ REPEAT_FIRST (rtac analz_image_freshK_lemma),
+ ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+ "for proving the Session Key Compromise theorem"
+
+method_setup possibility = {*
+ Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+ "for proving possibility theorems"
end
--- a/src/HOL/Auth/TLS.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/TLS.ML Tue Feb 13 13:16:27 2001 +0100
@@ -281,26 +281,18 @@
(*** Unicity results for PMS, the pre-master-secret ***)
-(*PMS determines B. Proof borrowed from NS_Public/unique_NA and from Yahalom*)
-Goal "[| Nonce PMS ~: analz (spies evs); evs : tls |] \
-\ ==> EX B'. ALL B. \
-\ Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-(*ClientKeyExch*)
-by (ClientKeyExch_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-by (expand_case_tac "PMS = ?y" 1 THEN
- blast_tac (claset() addSEs partsEs) 1);
-val lemma = result();
-
+(*PMS determines B.*)
Goal "[| Crypt(pubK B) (Nonce PMS) : parts (spies evs); \
\ Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
\ Nonce PMS ~: analz (spies evs); \
\ evs : tls |] \
\ ==> B=B'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*Fake, ClientKeyExch*)
+by (ALLGOALS Blast_tac);
qed "Crypt_unique_PMS";
@@ -311,24 +303,18 @@
**)
(*In A's internal Note, PMS determines A and B.*)
-Goal "evs : tls ==> EX A' B'. ALL A B. \
-\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
-by (parts_induct_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
-by (expand_case_tac "PMS = ?y" 1 THEN
- blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
-val lemma = result();
-
Goal "[| Notes A {|Agent B, Nonce PMS|} : set evs; \
\ Notes A' {|Agent B', Nonce PMS|} : set evs; \
\ evs : tls |] \
\ ==> A=A' & B=B'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+(*ClientKeyExch*)
+by (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]) 1);
qed "Notes_unique_PMS";
-
(**** Secrecy Theorems ****)
(*Key compromise lemma needed to prove analz_image_keys.
--- a/src/HOL/Auth/Yahalom.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Yahalom.ML Tue Feb 13 13:16:27 2001 +0100
@@ -168,23 +168,6 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : yahalom ==> \
-\ EX A' B' na' nb' X'. ALL A B na nb X. \
-\ Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
-by (etac yahalom.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-by (ex_strip_tac 2);
-by (Blast_tac 2);
-(*Remaining case: YM3*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs
- delrules [conjI] (*no split-up to 4 subgoals*)) 1);
-val lemma = result();
Goal "[| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
@@ -192,7 +175,14 @@
\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*YM4*)
+by (Blast_tac 2);
+(*YM3, by freshness*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
qed "unique_session_keys";
@@ -411,26 +401,16 @@
(*** The Nonce NB uniquely identifies B's message. ***)
-Goal "evs : yahalom ==> \
-\EX NA' A' B'. ALL NA A B. \
-\ Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(knows Spy evs) \
-\ --> B ~: bad --> NA = NA' & A = A' & B = B'";
-by (parts_induct_tac 1);
-(*Fake*)
-by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*)
- THEN Fake_parts_insert_tac 1);
-by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
-(*YM2: creation of new Nonce. Move assertion into global context*)
-by (expand_case_tac "nb = ?y" 1);
-by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-val lemma = result();
-
Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (knows Spy evs); \
\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (knows Spy evs); \
\ evs : yahalom; B ~: bad; B' ~: bad |] \
\ ==> NA' = NA & A' = A & B' = B";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (parts_induct_tac 1);
+by (Fake_parts_insert_tac 1);
+(*YM2, by freshness*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
qed "unique_NB";
--- a/src/HOL/Auth/Yahalom2.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Tue Feb 13 13:16:27 2001 +0100
@@ -169,29 +169,18 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : yahalom ==> \
-\ EX A' B' na' nb' X'. ALL A B na nb X. \
-\ Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
-by (etac yahalom.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (Clarify_tac 1);
-(*Remaining case: YM3*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*)
- addss (simpset() addsimps [parts_insertI])) 1);
-val lemma = result();
-
Goal "[| Says Server A \
\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
\ Says Server A' \
\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} : set evs; \
\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*YM3, by freshness*)
+by (Blast_tac 1);
qed "unique_session_keys";
--- a/src/HOL/Auth/Yahalom_Bad.ML Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.ML Tue Feb 13 13:16:27 2001 +0100
@@ -142,31 +142,20 @@
(*** The Key K uniquely identifies the Server's message. **)
-Goal "evs : yahalom ==> \
-\ EX A' B' na' nb' X'. ALL A B na nb X. \
-\ Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
-by (etac yahalom.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
-by (ALLGOALS Clarify_tac);
-by (ex_strip_tac 2);
-by (Blast_tac 2);
-(*Remaining case: YM3*)
-by (expand_case_tac "K = ?y" 1);
-by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-(*...we assume X is a recent message and handle this case by contradiction*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs
- delrules [conjI] (*no split-up to 4 subgoals*)) 1);
-val lemma = result();
-
Goal "[| Says Server A \
\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
\ Says Server A' \
\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} : set evs; \
\ evs : yahalom |] \
\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (prove_unique_tac lemma 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac yahalom.induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*YM4*)
+by (Blast_tac 2);
+(*YM3, by freshness*)
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
qed "unique_session_keys";