Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a
translation.
--- a/src/HOL/Auth/Event.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Event.ML Tue Mar 09 11:01:39 1999 +0100
@@ -2,90 +2,170 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Theory of events for security protocols
-
-Datatype of events; function "sees"; freshness
*)
AddIffs [Spy_in_bad, Server_not_bad];
-(**** Function "spies" ****)
+Addsimps [knows_Cons, used_Cons];
+
+(**** Function "knows" ****)
-(** Simplifying parts (insert X (spies evs))
- = parts {X} Un parts (spies evs) -- since general case loops*)
+(** Simplifying parts (insert X (knows Spy evs))
+ = parts {X} Un parts (knows Spy evs) -- since general case loops*)
-bind_thm ("parts_insert_spies",
+bind_thm ("parts_insert_knows_Spy",
parts_insert |>
- read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
+ read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]);
-Goal "P(event_case sf nf ev) = \
+Goal "P(event_case sf nf gf ev) = \
\ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
-\ (ALL A X. ev = Notes A X --> P(nf A X)))";
+\ (ALL A X. ev = Notes A X --> P(nf A X)) & \
+\ (ALL A X. ev = Gets A X --> P(gf A X)))";
by (induct_tac "ev" 1);
by Auto_tac;
qed "expand_event_case";
-Goal "spies (Says A B X # evs) = insert X (spies evs)";
+Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
by (Simp_tac 1);
-qed "spies_Says";
+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 "spies (Notes A X # evs) = \
-\ (if A:bad then insert X (spies evs) else spies evs)";
+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 "spies_Notes";
+qed "knows_Spy_Notes";
-Goal "spies evs <= spies (Says A B X # evs)";
+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 "spies_subset_spies_Says";
+qed "knows_Spy_subset_knows_Spy_Says";
-Goal "spies evs <= spies (Notes A X # evs)";
+Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
by (Simp_tac 1);
by (Fast_tac 1);
-qed "spies_subset_spies_Notes";
+qed "knows_Spy_subset_knows_Spy_Notes";
-(*Spy sees all traffic*)
-Goal "Says A B X : set evs --> X : spies evs";
+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_spies";
+qed_spec_mp "Says_imp_knows_Spy";
-(*Spy sees Notes of bad agents*)
-Goal "Notes A X : set evs --> A: bad --> X : spies evs";
+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_spies";
+qed_spec_mp "Notes_imp_knows_Spy";
+
(*Use with addSEs to derive contradictions from old Says events containing
items known to be fresh*)
-val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs;
+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";
-Addsimps [spies_Says, spies_Notes];
+(*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 [spies_Cons];
+Delsimps [knows_Cons];
(*** Fresh nonces ***)
-Goal "parts (spies evs) <= used evs";
+Goal "parts (knows Spy evs) <= used evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_spies]
+ (simpset() addsimps [parts_insert_knows_Spy]
addsplits [expand_event_case])));
by (ALLGOALS Blast_tac);
-qed "parts_spies_subset_used";
+qed "parts_knows_Spy_subset_used";
-bind_thm ("usedI", impOfSubs parts_spies_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_spies]
+ (simpset() addsimps [parts_insert_knows_Spy]
addsplits [expand_event_case])));
by (ALLGOALS Blast_tac);
bind_thm ("initState_into_used", impOfSubs (result()));
@@ -100,6 +180,11 @@
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);
@@ -109,29 +194,34 @@
Delsimps [used_Nil, used_Cons];
-(*currently unused*)
-Goal "used evs <= used (evs@evs')";
-by (induct_tac "evs" 1);
-by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
-by (induct_tac "a" 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
-qed "used_subset_append";
-
-
-(*For proving theorems of the form X ~: analz (spies evs) --> P
+(*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 (spies ?evs)")] impI;
+ [("P", "?Y ~: analz (knows Spy ?evs)")] impI;
in
rtac analz_impI THEN'
REPEAT1 o
(dresolve_tac
- [spies_subset_spies_Says RS analz_mono RS contra_subsetD,
- spies_subset_spies_Notes RS analz_mono RS contra_subsetD])
+ [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 Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Event.thy Tue Mar 09 11:01:39 1999 +0100
@@ -19,24 +19,49 @@
datatype (*Messages--could add another constructor for agent knowledge*)
event = Says agent agent msg
| Notes agent msg
+ | Gets agent msg
+
+consts
+ bad :: agent set (*compromised agents*)
+ knows :: agent => event list => msg set
-consts
- bad :: agent set (*compromised agents*)
+
+(*"spies" is retained for compability's sake*)
+syntax
spies :: event list => msg set
+translations
+ "spies" => "knows Spy"
+
+
rules
(*Spy has access to his own key for spoof messages, but Server is secure*)
Spy_in_bad "Spy: bad"
Server_not_bad "Server ~: bad"
primrec
- (*Spy reads all traffic whether addressed to him or not*)
- spies_Nil "spies [] = initState Spy"
- spies_Cons "spies (ev # evs) =
- (case ev of
- Says A B X => insert X (spies evs)
- | Notes A X =>
- if A:bad then insert X (spies evs) else spies evs)"
+ knows_Nil "knows A [] = initState A"
+ knows_Cons "knows A (ev # evs) =
+ (if A = Spy then
+ (case ev of
+ Says A' B X => insert X (knows Spy evs)
+ | Notes A' X =>
+ if A' : bad then insert X (knows Spy evs) else knows Spy evs
+ | Gets A' X => knows Spy evs)
+ else
+ (case ev of
+ Says A' B X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Notes A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs
+ | Gets A' X =>
+ if A'=A then insert X (knows A evs) else knows A evs))"
+
+(*
+ Case A=Spy on the Gets event
+ enforces the fact that if a message is received then it must have been sent,
+ therefore the oops case must use Notes
+*)
consts
(*Set of items that might be visible to somebody:
@@ -48,6 +73,9 @@
used_Cons "used (ev # evs) =
(case ev of
Says A B X => parts {X} Un (used evs)
- | Notes A X => parts {X} Un (used evs))"
+ | Notes A X => parts {X} Un (used evs)
+ | Gets A X => used evs)"
+
+
end
--- a/src/HOL/Auth/OtwayRees.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Mar 09 11:01:39 1999 +0100
@@ -12,68 +12,81 @@
Proc. Royal Soc. 426 (1989)
*)
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
(*A "possibility property": there are traces that reach the end*)
Goal "[| B ~= Server |] \
-\ ==> EX K. EX NA. EX evs: otway. \
+\ ==> EX NA K. EX evs: otway. \
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS
+ otway.OR1 RS otway.Reception RS
+ otway.OR2 RS otway.Reception RS
+ otway.OR3 RS otway.Reception RS otway.OR4) 2);
by possibility_tac;
result();
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
(**** Inductive proofs about otway ****)
(** For reasoning about the encrypted portion of messages **)
-Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\ ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR2_analz_spies";
+Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \
+\ ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR2_analz_knows_Spy";
-Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\ ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \
+\ ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (spies evs)";
+\ ==> K : parts (knows Spy evs)";
by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
-bind_thm ("OR2_parts_spies",
- OR2_analz_spies RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_spies",
- OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_knows_Spy",
+ OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+ OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_spies] (i+6) THEN
- forward_tac [OR4_parts_spies] (i+5) THEN
- forward_tac [OR2_parts_spies] (i+3) THEN
+ forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+ forward_tac [OR4_parts_knows_Spy] (i+6) THEN
+ forward_tac [OR2_parts_knows_Spy] (i+4) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -83,7 +96,7 @@
(*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -114,18 +127,18 @@
(*For proofs involving analz.*)
-val analz_spies_tac =
- dtac OR2_analz_spies 4 THEN
- dtac OR4_analz_spies 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
- REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac =
+ dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN
+ dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+ forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (spies evs)) ==>
- Key K : analz (spies evs)
+ Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K : analz (knows Spy evs)
A more general formula must be proved inductively.
****)
@@ -135,10 +148,10 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key``KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+\ (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\ (K : KK | Key K : analz (knows Spy evs))";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -148,8 +161,8 @@
Goal "[| evs : otway; KAB ~: range shrK |] \
-\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+\ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \
+\ (K = KAB | Key K : analz (knows Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -169,7 +182,7 @@
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 spies_partsEs) 1);
+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; \
@@ -179,12 +192,11 @@
qed "unique_session_keys";
-
(**** Authenticity properties relating to NA ****)
(*Only OR1 can have caused such a part of a message to appear.*)
Goal "[| A ~: bad; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs";
@@ -192,12 +204,21 @@
by (Blast_tac 1);
qed_spec_mp "Crypt_imp_OR1";
+Goal "[| Gets B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\ A ~: bad; evs : otway |] \
+\ ==> Says A B {|NA, Agent A, Agent B, \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
+\ : set evs";
+by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1);
+qed"Crypt_imp_OR1_Gets";
+
(** 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 (spies evs) \
+\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) \
\ --> B = B'";
by (parts_induct_tac 1);
by (Blast_tac 1);
@@ -207,8 +228,8 @@
by (Blast_tac 1);
val lemma = result();
-Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
-\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
+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);
@@ -219,19 +240,19 @@
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
over-simplified version of this protocol: see OtwayRees_Bad.*)
Goal "[| A ~: bad; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
-\ ~: parts (spies evs)";
+\ ~: parts (knows Spy evs)";
by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed_spec_mp"no_nonce_OR1_OR2";
+by Auto_tac;
+qed_spec_mp "no_nonce_OR1_OR2";
val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE);
(*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!*)
Goal "[| A ~: bad; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \
\ --> Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
@@ -253,7 +274,7 @@
(*OR3, two cases*) (** LEVEL 7 **)
by (blast_tac (claset() addSEs [nonce_OR1_OR2_E]
delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
-by (blast_tac (claset() addIs [unique_NA]) 1);
+by (blast_tac (claset() addIs [unique_NA]) 1);
qed_spec_mp "NA_Crypt_imp_Server_msg";
@@ -263,7 +284,7 @@
Spy_not_see_encrypted_key*)
Goal "[| Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
\ A ~: bad; evs : otway |] \
\ ==> EX NB. Says Server B \
\ {|NA, \
@@ -283,9 +304,9 @@
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
-\ Key K ~: analz (spies evs)";
+\ Key K ~: analz (knows Spy evs)";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -305,7 +326,7 @@
\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -315,10 +336,10 @@
what it is.*)
Goal "[| Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
qed "A_gets_good_key";
@@ -329,7 +350,7 @@
know anything about X: it does NOT have to have the right form.*)
Goal "[| B ~: bad; evs : otway |] \
\ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ : parts (spies evs) --> \
+\ : parts (knows Spy evs) --> \
\ (EX X. Says B Server \
\ {|NA, Agent A, Agent B, X, \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -343,7 +364,7 @@
Goal "[| evs : otway; B ~: bad |] \
\ ==> EX NA' A'. ALL NA A. \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
+\ 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);
@@ -353,18 +374,17 @@
by (Blast_tac 1);
val lemma = result();
-Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
-\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
+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);
qed "unique_NB";
-
(*If the encrypted message appears, and B has used Nonce NB,
then it originated with the Server!*)
Goal "[| B ~: bad; evs : otway |] \
-\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \
+\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \
\ --> (ALL X'. Says B Server \
\ {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
@@ -385,7 +405,8 @@
*)
by (safe_tac (claset() delrules [disjCI, impCE]));
by (Blast_tac 3);
-by (blast_tac (claset() addDs [unique_NB]) 2);
+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);
qed_spec_mp "NB_Crypt_imp_Server_msg";
@@ -396,7 +417,7 @@
Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs; \
-\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ B ~: bad; evs : otway |] \
\ ==> Says Server B \
\ {|NA, \
@@ -411,10 +432,10 @@
Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
\ : set evs; \
-\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
+\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
qed "B_gets_good_key";
@@ -436,7 +457,7 @@
(*After getting and checking OR4, agent A can trust that B has been active.
We could probably prove that X has the expected form, but that is not
strictly necessary for authentication.*)
-Goal "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
--- a/src/HOL/Auth/OtwayRees.thy Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Tue Mar 09 11:01:39 1999 +0100
@@ -1,19 +1,14 @@
-(* Title: HOL/Auth/OtwayRees
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "otway" for the Otway-Rees protocol.
+(*
+Inductive relation "otway" for the Otway-Rees protocol
+extended by Gets primitive.
Version that encrypts Nonce NB
-From page 244 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
*)
OtwayRees = Shared +
+
consts otway :: event list set
inductive "otway"
intrs
@@ -25,8 +20,13 @@
(*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: otway; X: synth (analz (spies evs)) |]
- ==> Says Spy B X # evs : otway"
+ Fake "[| evsa: otway; X: synth (analz (knows Spy evsa)) |]
+ ==> Says Spy B X # evsa : otway"
+
+ (*A message that has been sent can be received by the
+ intended recipient.*)
+ Reception "[| evsr: otway; Says A B X : set evsr |]
+ ==> Gets B X # evsr : otway"
(*Alice initiates a protocol run*)
OR1 "[| evs1: otway; Nonce NA ~: used evs1 |]
@@ -38,7 +38,7 @@
the sender is, hence the A' in the sender field.
Note that NB is encrypted.*)
OR2 "[| evs2: otway; Nonce NB ~: used evs2;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+ Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
@@ -49,7 +49,7 @@
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
OR3 "[| evs3: otway; Key KAB ~: used evs3;
- Says B' Server
+ Gets Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
@@ -68,7 +68,7 @@
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
: set evs4;
- Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evs4 |]
==> Says B A {|Nonce NA, X|} # evs4 : otway"
--- a/src/HOL/Auth/OtwayRees_AN.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 09 11:01:39 1999 +0100
@@ -12,7 +12,7 @@
IEEE Trans. SE 22 (1), 1996
*)
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
@@ -23,48 +23,62 @@
\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS
+ otway.OR1 RS otway.Reception RS
+ otway.OR2 RS otway.Reception RS
+ otway.OR3 RS otway.Reception RS otway.OR4) 2);
by possibility_tac;
result();
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
(**** Inductive proofs about otway ****)
(** For reasoning about the encrypted portion of messages **)
-Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
-\ X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|X, Crypt(shrK B) X'|} : set evs; evs : otway |] ==> \
+\ X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
-Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
-\ : set evs ==> K : parts (spies evs)";
+Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} : set evs \
+\ ==> K : parts (knows Spy evs)";
by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
-bind_thm ("OR4_parts_spies",
- OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+ OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_spies] (i+6) THEN
- forward_tac [OR4_parts_spies] (i+5) THEN
+ forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+ forward_tac [OR4_parts_knows_Spy] (i+6) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -74,7 +88,7 @@
(*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -107,18 +121,17 @@
(*For proofs involving analz.*)
-val analz_spies_tac =
- dtac OR4_analz_spies 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN
- assume_tac 7 THEN
- REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac =
+ dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+ forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (spies evs)) ==>
- Key K : analz (spies evs)
+ Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K : analz (knows Spy evs)
A more general formula must be proved inductively.
****)
@@ -129,10 +142,10 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : otway ==> \
\ ALL K KK. KK <= -(range shrK) --> \
-\ (Key K : analz (Key``KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+\ (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\ (K : KK | Key K : analz (knows Spy evs))";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -142,8 +155,8 @@
Goal "[| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+\ Key K : analz (insert (Key KAB) (knows Spy evs)) = \
+\ (K = KAB | Key K : analz (knows Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -165,7 +178,7 @@
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 spies_partsEs) 1);
+by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
val lemma = result();
@@ -188,7 +201,7 @@
(*If the encrypted message appears then it originated with the Server!*)
Goal "[| A ~: bad; A ~= B; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
\ --> (EX NB. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -203,7 +216,7 @@
(*Corollary: if A receives B's OR4 message then it originated with the Server.
Freshness may be inferred from nonce NA.*)
-Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
+Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
\ A ~: bad; A ~= B; evs : otway |] \
\ ==> EX NB. Says Server B \
@@ -224,9 +237,9 @@
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs --> \
\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
-\ Key K ~: analz (spies evs)";
+\ Key K ~: analz (knows Spy evs)";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -247,7 +260,7 @@
\ : set evs; \
\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -255,11 +268,11 @@
(*A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.*)
-Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
+Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set evs; \
\ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; A ~= B; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
qed "A_gets_good_key";
@@ -268,7 +281,7 @@
(*If the encrypted message appears then it originated with the Server!*)
Goal "[| B ~: bad; A ~= B; evs : otway |] \
-\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
+\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (knows Spy evs) \
\ --> (EX NA. Says Server B \
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
@@ -283,7 +296,7 @@
(*Guarantee for B: if it gets a well-formed certificate then the Server
has sent the correct message in round 3.*)
-Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
\ B ~: bad; A ~= B; evs : otway |] \
\ ==> EX NA. Says Server B \
@@ -295,10 +308,10 @@
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
+Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
\ : set evs; \
\ ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; A ~= B; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
qed "B_gets_good_key";
--- a/src/HOL/Auth/OtwayRees_AN.thy Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 09 11:01:39 1999 +0100
@@ -28,9 +28,14 @@
(*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: otway; X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |]
==> Says Spy B X # evs : otway"
+ (*A message that has been sent can be received by the
+ intended recipient.*)
+ Reception "[| evsr: otway; Says A B X : set evsr |]
+ ==> Gets B X # evsr : otway"
+
(*Alice initiates a protocol run*)
OR1 "[| evs1: otway |]
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
@@ -38,14 +43,14 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
OR2 "[| evs2: otway;
- Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
+ Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
# evs2 : otway"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
OR3 "[| evs3: otway; Key KAB ~: used evs3;
- Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+ Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set evs3 |]
==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
@@ -57,7 +62,7 @@
Need B ~= Server because we allow messages to self.*)
OR4 "[| evs4: otway; B ~= Server;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
- Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
+ Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set evs4 |]
==> Says B A X # evs4 : otway"
--- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 09 11:01:39 1999 +0100
@@ -15,7 +15,7 @@
indicates the possibility of this attack.
*)
-AddEs spies_partsEs;
+AddEs knows_Spy_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
@@ -26,58 +26,71 @@
\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
\ : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
+by (rtac (otway.Nil RS
+ otway.OR1 RS otway.Reception RS
+ otway.OR2 RS otway.Reception RS
+ otway.OR3 RS otway.Reception RS otway.OR4) 2);
by possibility_tac;
result();
+Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by Auto_tac;
+qed"Gets_imp_Says";
+
+(*Must be proved separately for each protocol*)
+Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs";
+by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
+qed"Gets_imp_knows_Spy";
+AddDs [Gets_imp_knows_Spy RS parts.Inj];
+
(**** Inductive proofs about otway ****)
(** For reasoning about the encrypted portion of messages **)
-Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
-\ ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR2_analz_spies";
+Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \
+\ ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR2_analz_knows_Spy";
-Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
-\ ==> X : analz (spies evs)";
-by (dtac (Says_imp_spies RS analz.Inj) 1);
-by (Blast_tac 1);
-qed "OR4_analz_spies";
+Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \
+\ ==> X : analz (knows Spy evs)";
+by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
+qed "OR4_analz_knows_Spy";
Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
-\ ==> K : parts (spies evs)";
+\ ==> K : parts (knows Spy evs)";
by (Blast_tac 1);
-qed "Oops_parts_spies";
+qed "Oops_parts_knows_Spy";
-bind_thm ("OR2_parts_spies",
- OR2_analz_spies RS (impOfSubs analz_subset_parts));
-bind_thm ("OR4_parts_spies",
- OR4_analz_spies RS (impOfSubs analz_subset_parts));
+bind_thm ("OR2_parts_knows_Spy",
+ OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("OR4_parts_knows_Spy",
+ OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-(*For proving the easier theorems about X ~: parts (spies evs).*)
+(*For proving the easier theorems about X ~: parts (knows Spy evs).*)
fun parts_induct_tac i =
etac otway.induct i THEN
- forward_tac [Oops_parts_spies] (i+6) THEN
- forward_tac [OR4_parts_spies] (i+5) THEN
- forward_tac [OR2_parts_spies] (i+3) THEN
+ forward_tac [Oops_parts_knows_Spy] (i+7) THEN
+ forward_tac [OR4_parts_knows_Spy] (i+6) THEN
+ forward_tac [OR2_parts_knows_Spy] (i+4) THEN
prove_simple_subgoals_tac i;
-(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY
sends messages containing X! **)
(*Spy never sees a good agent's shared key!*)
-Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)";
by (parts_induct_tac 1);
by (ALLGOALS Blast_tac);
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
-Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
+Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)";
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -87,7 +100,7 @@
(*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))";
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -118,18 +131,18 @@
(*For proofs involving analz.*)
-val analz_spies_tac =
- dtac OR2_analz_spies 4 THEN
- dtac OR4_analz_spies 6 THEN
- forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
- REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
+val analz_knows_Spy_tac =
+ dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN
+ dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
+ forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key KAB) (spies evs)) ==>
- Key K : analz (spies evs)
+ Key K : analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K : analz (knows Spy evs)
A more general formula must be proved inductively.
****)
@@ -140,10 +153,10 @@
(*The equality makes the induction hypothesis easier to apply*)
Goal "evs : otway ==> \
\ ALL K KK. KK <= - (range shrK) --> \
-\ (Key K : analz (Key``KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+\ (Key K : analz (Key``KK Un (knows Spy evs))) = \
+\ (K : KK | Key K : analz (knows Spy evs))";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
@@ -153,8 +166,8 @@
Goal "[| evs : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+\ Key K : analz (insert (Key KAB) (knows Spy evs)) = \
+\ (K = KAB | Key K : analz (knows Spy evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -174,7 +187,7 @@
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 spies_partsEs) 1);
+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; \
@@ -193,9 +206,9 @@
\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
\ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
\ Notes Spy {|NA, NB, Key K|} ~: set evs --> \
-\ Key K ~: analz (spies evs)";
+\ Key K ~: analz (knows Spy evs)";
by (etac otway.induct 1);
-by analz_spies_tac;
+by analz_knows_Spy_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addcongs [conj_cong]
addsimps [analz_insert_eq, analz_insert_freshK]
@@ -215,7 +228,7 @@
\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
\ Notes Spy {|NA, NB, Key K|} ~: set evs; \
\ A ~: bad; B ~: bad; evs : otway |] \
-\ ==> Key K ~: analz (spies evs)";
+\ ==> Key K ~: analz (knows Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
by (blast_tac (claset() addSEs [lemma]) 1);
qed "Spy_not_see_encrypted_key";
@@ -227,7 +240,7 @@
The premise A ~= B prevents OR2's similar-looking cryptogram from being
picked up. Original Otway-Rees doesn't need it.*)
Goal "[| A ~: bad; A ~= B; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs";
by (parts_induct_tac 1);
@@ -236,11 +249,12 @@
(*Crucial property: If the encrypted message appears, and A has used NA
- to start a run, then it originated with the Server!*)
+ to start a run, then it originated with the Server!
+ The premise A ~= B allows use of Crypt_imp_OR1*)
(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
-Goal "[| A ~: bad; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
+Goal "[| A ~: bad; A ~= B; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \
@@ -261,7 +275,7 @@
(*OR3*) (** LEVEL 5 **)
(*The hypotheses at this point suggest an attack in which nonce NB is used
in two different roles:
- Says B' Server
+ Gets Server
{|Nonce NA, Agent Aa, Agent A,
Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
--- a/src/HOL/Auth/OtwayRees_Bad.thy Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Mar 09 11:01:39 1999 +0100
@@ -22,9 +22,14 @@
(*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: otway; X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |]
==> Says Spy B X # evs : otway"
+ (*A message that has been sent can be received by the
+ intended recipient.*)
+ Reception "[| evsr: otway; Says A B X : set evsr |]
+ ==> Gets B X # evsr : otway"
+
(*Alice initiates a protocol run*)
OR1 "[| evs1: otway; Nonce NA ~: used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
@@ -35,7 +40,7 @@
the sender is, hence the A' in the sender field.
We modify the published protocol by NOT encrypting NB.*)
OR2 "[| evs2: otway; Nonce NB ~: used evs2;
- Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
+ Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
@@ -45,7 +50,7 @@
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
OR3 "[| evs3: otway; Key KAB ~: used evs3;
- Says B' Server
+ Gets Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
Nonce NB,
@@ -60,11 +65,11 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
Need B ~= Server because we allow messages to self.*)
- OR4 "[| evs4: otway; A ~= B; B ~= Server;
+ OR4 "[| evs4: otway; B ~= Server;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
: set evs4;
- Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
+ Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evs4 |]
==> Says B A {|Nonce NA, X|} # evs4 : otway"
--- a/src/HOL/Auth/Public.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Public.ML Tue Mar 09 11:01:39 1999 +0100
@@ -72,7 +72,7 @@
Goal "Key (pubK A) : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, spies_Cons]
+ (simpset() addsimps [imageI, knows_Cons]
addsplits [expand_event_case])));
qed_spec_mp "spies_pubK";
@@ -80,7 +80,7 @@
Goal "A: bad ==> Key (priK A) : spies evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, spies_Cons]
+ (simpset() addsimps [imageI, knows_Cons]
addsplits [expand_event_case])));
qed "Spy_spies_bad";
--- a/src/HOL/Auth/Shared.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/Shared.ML Tue Mar 09 11:01:39 1999 +0100
@@ -28,11 +28,11 @@
(*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 (fast_tac
+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]
- addss (simpset())) 1);
+ addIs [impOfSubs analz_subset_parts],
+ simpset()) 1);
qed "keysFor_parts_insert";
Goal "Crypt K X : H ==> K : keysFor H";
@@ -41,22 +41,21 @@
qed "Crypt_imp_keysFor";
-(*** Function "spies" ***)
+(*** Function "knows" ***)
(*Spy sees shared keys of agents!*)
-Goal "A: bad ==> Key (shrK A) : spies evs";
+Goal "A: bad ==> Key (shrK A) : knows Spy evs";
by (induct_tac "evs" 1);
by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [imageI, spies_Cons]
+ (simpset() addsimps [imageI, knows_Cons]
addsplits [expand_event_case])));
-qed "Spy_spies_bad";
-
-AddSIs [Spy_spies_bad];
+qed "Spy_knows_Spy_bad";
+AddSIs [Spy_knows_Spy_bad];
(*For not_bad_tac*)
-Goal "[| Crypt (shrK A) X : analz (spies evs); A: bad |] \
-\ ==> X : analz (spies evs)";
-by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1);
+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
@@ -202,7 +201,8 @@
such as Nonce ?N ~: used evs that match Nonce_supply*)
fun possibility_tac st = st |>
(REPEAT
- (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
+ (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])));
--- a/src/HOL/Auth/TLS.ML Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/TLS.ML Tue Mar 09 11:01:39 1999 +0100
@@ -480,7 +480,7 @@
(*ClientAccepts and ServerAccepts: because PMS was already visible*)
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS,
Says_imp_spies RS analz.Inj,
- Notes_imp_spies RS analz.Inj]) 6));
+ Notes_imp_knows_Spy RS analz.Inj]) 6));
(*ClientHello*)
by (Blast_tac 3);
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)