--- a/src/HOL/Auth/OtwayRees.ML Mon Oct 28 15:36:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Mon Oct 28 15:59:39 1996 +0100
@@ -16,6 +16,7 @@
proof_timing:=true;
HOL_quantifiers := false;
+Pretty.setdepth 15;
(*Weak liveness: there are traces that reach the end*)
@@ -54,21 +55,21 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
-\ X : analz (sees lost Spy evs)";
+goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
+\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR2_analz_sees_Spy";
-goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
-\ X : analz (sees lost Spy evs)";
+goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \
+\ ==> X : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
-\ K : parts (sees lost Spy evs)";
+goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
+\ ==> K : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-qed "Reveal_parts_sees_Spy";
+qed "Oops_parts_sees_Spy";
(*OR2_analz... and OR4_analz... let us treat those cases using the same
argument as for the Fake case. This is possible for most, but not all,
@@ -86,7 +87,7 @@
let val tac = forw_inst_tac [("lost","lost")]
in tac OR2_parts_sees_Spy 4 THEN
tac OR4_parts_sees_Spy 6 THEN
- tac Reveal_parts_sees_Spy 7
+ tac Oops_parts_sees_Spy 7
end;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
@@ -105,34 +106,27 @@
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. [| evs : otway lost; A ~: lost |] \
-\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+ "!!evs. evs : otway lost \
+\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
by (Auto_tac());
-qed "Spy_not_see_shrK";
-
-bind_thm ("Spy_not_analz_shrK",
- [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
-
-Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
+qed "Spy_see_shrK";
+Addsimps [Spy_see_shrK];
-(*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 lost Spy evs); \
-\ evs : otway lost; \
-\ A:lost ==> R \
-\ |] ==> R";
-by (rtac ccontr 1);
-by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
-by (swap_res_tac prems 2);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
-qed "Spy_see_shrK_E";
+goal thy
+ "!!evs. evs : otway lost \
+\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
+by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
+qed "Spy_analz_shrK";
+Addsimps [Spy_analz_shrK];
-bind_thm ("Spy_analz_shrK_E",
- analz_subset_parts RS subsetD RS Spy_see_shrK_E);
+goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : otway lost |] ==> A:lost";
+by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+qed "Spy_see_shrK_D";
-AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
+bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
+AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
(*** Future keys can't be seen or used! ***)
@@ -246,40 +240,27 @@
(*** Proofs involving analz ***)
-(*Describes the form of Key K when the following message is sent. The use of
- "parts" strengthens the induction hyp for proving the Fake case. The
- assumption A ~: lost prevents its being a Faked message. (Based
- on NS_Shared/Says_S_message_form) *)
-goal thy
- "!!evs. evs: otway lost ==> \
-\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
-\ A ~: lost --> \
-\ (EX evt: otway lost. K = newK evt)";
-by (parts_induct_tac 1);
-by (Auto_tac());
-qed_spec_mp "Reveal_message_lemma";
-
-(*EITHER describes the form of Key K when the following message is sent,
- OR reduces it to the Fake case.*)
-
+(*Describes the form of K and NA when the Server sends this message. Also
+ for Oops case.*)
goal thy
- "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \
-\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = newK evt) \
-\ | Key K : analz (sees lost Spy evs)";
-br (Reveal_message_lemma RS disjCI) 1;
-ba 1;
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 1);
-qed "Reveal_message_form";
+ "!!evs. [| Says Server B \
+\ {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ evs : otway lost |] \
+\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
+\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
+by (etac rev_mp 1);
+by (etac otway.induct 1);
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+qed "Says_Server_message_form";
(*For proofs involving analz. We again instantiate the variable to "lost".*)
val analz_Fake_tac =
dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Reveal_message_form 7;
+ forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
+ assume_tac 7 THEN Full_simp_tac 7 THEN
+ REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
@@ -289,7 +270,6 @@
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
-
****)
@@ -303,16 +283,15 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
-by (ALLGOALS (*Takes 28 secs*)
+by (ALLGOALS (*Takes 22 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
(** LEVEL 5 **)
-(*Reveal case 2, OR4, OR2, Fake*)
-by (EVERY (map spy_analz_tac [7,5,3,2]));
-(*Reveal case 1, OR3, Base*)
+(*OR4, OR2, Fake*)
+by (EVERY (map spy_analz_tac [5,3,2]));
+(*Oops, OR3, Base*)
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
qed_spec_mp "analz_image_newK";
@@ -329,15 +308,11 @@
(*** The Key K uniquely identifies the Server's message. **)
-fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
-
goal thy
- "!!evs. evs : otway lost ==> \
-\ EX A' B' NA' NB'. ALL A B NA NB. \
-\ Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
-\ A=A' & B=B' & NA=NA' & NB=NB'";
+ "!!evs. evs : otway lost ==> \
+\ EX B' NA' NB' X'. ALL B NA NB X. \
+\ Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list 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 (Step_tac 1);
@@ -353,16 +328,11 @@
val lemma = result();
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} \
+ "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} \
\ : set_of_list evs; \
-\ Says Server B' \
-\ {|NA', Crypt {|NA', K|} (shrK A'), \
-\ Crypt {|NB', K|} (shrK B')|} \
+\ Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|} \
\ : set_of_list evs; \
-\ evs : otway lost |] \
-\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
+\ evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (dtac lemma 1);
by (REPEAT (etac exE 1));
(*Duplicate the assumption*)
@@ -494,21 +464,6 @@
qed "A_trust_OR4";
-(*Describes the form of K and NA when the Server sends this message.*)
-goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
-\ (EX i. NA = Nonce i) & \
-\ (EX j. NB = Nonce j)";
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
-qed "Says_Server_message_form";
-
-
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
@@ -518,11 +473,10 @@
\ ==> Says Server B \
\ {|NA, Crypt {|NA, Key K|} (shrK A), \
\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
-\ Says A Spy {|NA, Key K|} ~: set_of_list evs --> \
+\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac otway.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
by (ALLGOALS
(asm_full_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
@@ -532,24 +486,18 @@
by (fast_tac (!claset addSIs [parts_insertI]
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 3);
-(*Reveal case 2, OR4, OR2, Fake*)
+(*OR4, OR2, Fake*)
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
-(*Reveal case 1*) (** LEVEL 6 **)
-by (case_tac "Aa : lost" 1);
-(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
-by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
-by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
-(*So now we have Aa ~: lost *)
-by (dtac A_trust_OR4 1);
-by (REPEAT (assume_tac 1));
-by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
+(*Oops*) (** LEVEL 5 **)
+by (fast_tac (!claset delrules [disjE]
+ addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
"!!evs. [| Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ Says A Spy {|NA, K|} ~: set_of_list evs; \
+\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost Spy evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -562,7 +510,7 @@
\ Says Server B \
\ {|NA, Crypt {|NA, K|} (shrK A), \
\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ Says A Spy {|NA, K|} ~: set_of_list evs; \
+\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \
\ A ~: lost; B ~: lost; evs : otway lost |] \
\ ==> K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -684,9 +632,9 @@
encrypted by a good agent C. NEEDED? INTERESTING?**)
goal thy
"!!evs. evs : otway lost ==> \
-\ EX A B. ALL C N. \
-\ C ~: lost --> \
-\ Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
+\ EX A B. ALL C N. \
+\ C ~: lost --> \
+\ Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
\ C=A | C=B";
by (Simp_tac 1); (*Miniscoping*)
by (etac otway.induct 1);
@@ -713,5 +661,3 @@
delrules [disjCI, disjE]
addss (!simpset))));
qed "key_identifies_senders";
-
-
--- a/src/HOL/Auth/OtwayRees.thy Mon Oct 28 15:36:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Mon Oct 28 15:59:39 1996 +0100
@@ -62,7 +62,7 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway lost; A ~= B; B ~= Server;
+ OR4 "[| evs: otway lost; A ~= B;
Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
: set_of_list evs;
Says B Server {|Nonce NA, Agent A, Agent B, X',
@@ -71,14 +71,11 @@
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway lost"
- (*This message models possible leaks of session keys. Alice's Nonce
- identifies the protocol run.*)
- Revl "[| evs: otway lost; A ~= Spy;
- Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
- : set_of_list evs;
- Says A B {|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+ (*This message models possible leaks of session keys. The nonces
+ identify the protocol run.*)
+ Oops "[| evs: otway lost; B ~= Spy;
+ Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
: set_of_list evs |]
- ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
end