--- a/src/HOL/Auth/OtwayRees.ML Mon Sep 09 17:33:23 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Mon Sep 09 17:34:24 1996 +0200
@@ -62,7 +62,10 @@
qed "OR5_parts_sees_Enemy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
- argument as for the Fake case.*)
+ argument as for the Fake case. This is possible for most, but not all,
+ proofs: Fake does not invent new nonces (as in OR2), and of course Fake
+ messages originate from the Enemy. *)
+
val OR2_OR4_tac =
dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
@@ -70,9 +73,9 @@
(*** Shared keys are not betrayed ***)
-(*Enemy never sees another agent's shared key!*)
+(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
goal thy
- "!!evs. [| evs : otway; A ~= Enemy |] ==> \
+ "!!evs. [| evs : otway; A ~= Enemy; A ~: Friend``leaked |] ==> \
\ Key (shrK A) ~: parts (sees Enemy evs)";
be otway.induct 1;
by OR2_OR4_tac;
@@ -90,16 +93,20 @@
Enemy_not_analz_shrK,
not_sym RSN (2, Enemy_not_analz_shrK)];
-(*We go to some trouble to preserve R in the 3rd subgoal*)
+(*We go to some trouble to preserve R in the 3rd and 4th subgoals
+ As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
-goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : otway; \
-\ A=Enemy ==> R \
+goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
+\ evs : otway; \
+\ A=Enemy ==> R; \
+\ !!i. [| A = Friend i; i: leaked |] ==> R \
\ |] ==> R";
br ccontr 1;
br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
+br notI 3;
+be imageE 3;
by (swap_res_tac prems 2);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems)));
qed "Enemy_see_shrK_E";
bind_thm ("Enemy_analz_shrK_E",
@@ -109,28 +116,6 @@
AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
-(*No Friend will ever see another agent's shared key
- (excluding the Enemy, who might transmit his).
- The Server, of course, knows all shared keys.*)
-goal thy
- "!!evs. [| evs : otway; A ~= Enemy; A ~= Friend j |] ==> \
-\ Key (shrK A) ~: parts (sees (Friend j) evs)";
-br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
-by (ALLGOALS Asm_simp_tac);
-qed "Friend_not_see_shrK";
-
-
-(*Not for Addsimps -- it can cause goals to blow up!*)
-goal thy
- "!!evs. evs : otway ==> \
-\ (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) = \
-\ (A=B | A=Enemy)";
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
- addIs [impOfSubs (subset_insertI RS analz_mono)]
- addss (!simpset)) 1);
-qed "shrK_mem_analz";
-
-
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future.
@@ -220,9 +205,8 @@
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt))
- (insert (Key (shrK C)) (sees Enemy evs))) ==>
- Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
+ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
+ Key K : analz (sees Enemy evs)
A more general formula must be proved inductively.
@@ -243,9 +227,9 @@
by (best_tac (!claset addSEs partsEs
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 1);
-(*OR5*)
-by (fast_tac (!claset addss (!simpset)) 1);
+ addss (!simpset)) 2);
+(*Base case and OR5*)
+by (Auto_tac());
result();
@@ -254,6 +238,9 @@
Delsimps [image_insert];
Addsimps [image_insert RS sym];
+Delsimps [image_Un];
+Addsimps [image_Un RS sym];
+
goal thy "insert (Key (newK x)) (sees A evs) = \
\ Key `` (newK``{x}) Un (sees A evs)";
by (Fast_tac 1);
@@ -294,25 +281,22 @@
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
- "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
-\ (K : nE | Key K : analz (insert KsC sEe)) ==> \
-\ (Key K : analz (insert KsC (Key``nE Un sEe))) = \
-\ (K : nE | Key K : analz (insert KsC sEe))";
+ "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
+\ (K : nE | Key K : analz sEe) ==> \
+\ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
val lemma = result();
+
goal thy
"!!evs. evs : otway ==> \
-\ ALL K E. (Key K : analz (insert (Key (shrK C)) \
-\ (Key``(newK``E) Un (sees Enemy evs)))) = \
-\ (K : newK``E | \
-\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
+\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
+\ (K : newK``E | Key K : analz (sees Enemy evs))";
be otway.induct 1;
bd OR2_analz_sees_Enemy 4;
bd OR4_analz_sees_Enemy 6;
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
-by (ALLGOALS (*Takes 40 secs*)
+by (ALLGOALS (*Takes 35 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
@@ -321,14 +305,14 @@
by (enemy_analz_tac 5);
(*OR3*)
by (Fast_tac 4);
-(*OR2*) (** LEVEL 11 **)
+(*OR2*) (** LEVEL 7 **)
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
(insert_commute RS ssubst) 3);
by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
(insert_commute RS ssubst) 3);
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
by (enemy_analz_tac 3);
-(*Fake case*) (** LEVEL 6 **)
+(*Fake case*) (** LEVEL 11 **)
by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")]
(insert_commute RS ssubst) 2);
by (enemy_analz_tac 2);
@@ -339,12 +323,8 @@
goal thy
"!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key (newK evt)) \
-\ (insert (Key (shrK C)) \
-\ (sees Enemy evs))) = \
-\ (K = newK evt | \
-\ Key K : analz (insert (Key (shrK C)) \
-\ (sees Enemy evs)))";
+\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
+\ (K = newK evt | Key K : analz (sees Enemy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -371,9 +351,8 @@
"!!evs. [| Says Server (Friend j) \
\ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \
\ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \
-\ evs : otway; Friend i ~= C; Friend j ~= C \
-\ |] ==> \
-\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
+\ i ~: leaked; j ~: leaked; evs : otway |] ==> \
+\ K ~: analz (sees Enemy evs)";
be rev_mp 1;
be otway.induct 1;
bd OR2_analz_sees_Enemy 4;
@@ -383,14 +362,14 @@
by (REPEAT_FIRST (resolve_tac [conjI, impI]));
by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
-by (ALLGOALS
+by (ALLGOALS
(asm_full_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addSEs [less_irrefl]) 3);
-(*Fake*) (** LEVEL 8 **)
+(*Fake*) (** LEVEL 10 **)
by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
by (enemy_analz_tac 1);
(*OR4*)
@@ -411,9 +390,9 @@
(** First, two lemmas for the Fake, OR2 and OR4 cases **)
goal thy
- "!!evs. [| X : synth (analz (sees Enemy evs)); \
-\ Crypt X' (shrK C) : parts{X}; \
-\ C ~= Enemy; evs : otway |] \
+ "!!evs. [| X : synth (analz (sees Enemy evs)); \
+\ Crypt X' (shrK C) : parts{X}; \
+\ C ~= Enemy; C ~: Friend``leaked; evs : otway |] \
\ ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
addDs [impOfSubs parts_insert_subset_Un]
@@ -433,9 +412,9 @@
(*The Key K uniquely identifies a pair of senders in the message encrypted by
C, but if C=Enemy then he could send all sorts of nonsense.*)
goal thy
- "!!evs. evs : otway ==> \
-\ EX A B. ALL C. \
-\ C ~= Enemy --> \
+ "!!evs. evs : otway ==> \
+\ EX A B. ALL C. \
+\ C ~= Enemy & C ~: Friend``leaked --> \
\ (ALL S S' X. Says S S' X : set_of_list evs --> \
\ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
by (Simp_tac 1);
--- a/src/HOL/Auth/Shared.ML Mon Sep 09 17:33:23 1996 +0200
+++ b/src/HOL/Auth/Shared.ML Mon Sep 09 17:34:24 1996 +0200
@@ -20,6 +20,12 @@
open Shared;
+(*Holds because Friend is injective: thus cannot prove for all f*)
+goal thy "(Friend x : Friend``A) = (x:A)";
+by (Auto_tac());
+qed "Friend_image_eq";
+Addsimps [Friend_image_eq];
+
Addsimps [Un_insert_left, Un_insert_right];
(*By default only o_apply is built-in. But in the presence of eta-expansion
@@ -96,19 +102,20 @@
Addsimps [shrK_notin_image_newK];
-(*Agents see their own shrKs!*)
-goal thy "Key (shrK A) : analz (sees A evs)";
+(*Agents see their own shared keys!*)
+goal thy "Key (shrK A) : sees A evs";
by (list.induct_tac "evs" 1);
-by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
by (agent.induct_tac "A" 1);
-by (auto_tac (!claset addIs [range_eqI], !simpset));
-qed "analz_own_shrK";
+by (Auto_tac ());
+qed "sees_own_shrK";
-bind_thm ("parts_own_shrK",
- [analz_subset_parts, analz_own_shrK] MRS subsetD);
+(*Enemy sees leaked shrKs!*)
+goal thy "!!i. i: leaked ==> Key (shrK (Friend i)) : sees Enemy evs";
+by (list.induct_tac "evs" 1);
+by (Auto_tac ());
+qed "Enemy_sees_leaked";
-Addsimps [analz_own_shrK, parts_own_shrK];
-
+AddSIs [sees_own_shrK, Enemy_sees_leaked];
(** Specialized rewrite rules for (sees A (Says...#evs)) **)