--- a/src/HOL/Auth/NS_Shared.ML Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Mon Oct 28 12:55:24 1996 +0100
@@ -50,22 +50,22 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
(*For reasoning about the encrypted portion of message NS3*)
-goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
-\ X : parts (sees lost Spy evs)";
+goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \
+\ ==> X : parts (sees lost Spy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
qed "NS3_msg_in_parts_sees_Spy";
goal thy
- "!!evs. Says S A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs ==> \
-\ K : parts (sees lost Spy evs)";
+ "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : 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";
val parts_Fake_tac =
dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
- forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 8;
+ forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
@@ -82,47 +82,29 @@
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key!*)
+(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. [| evs : ns_shared lost; A ~: lost |] \
-\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
+ "!!evs. evs : ns_shared 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 : ns_shared 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 : ns_shared 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);
-
-AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
-
+goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \
+\ evs : ns_shared lost |] ==> A:lost";
+by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
+qed "Spy_see_shrK_D";
-goal thy
- "!!evs. evs : ns_shared lost ==> \
-\ (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
-by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
- addss (!simpset)) 1);
-qed "shrK_mem_analz";
-
-Addsimps [shrK_mem_analz];
-
+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! ***)
@@ -256,12 +238,7 @@
\ Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \
\ : set_of_list evs";
by (etac rev_mp 1);
-by (etac ns_shared.induct 1);
-by parts_Fake_tac;
-(*Fake case*)
-by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]
- addss (!simpset)) 2);
+by (parts_induct_tac 1);
by (Auto_tac());
qed "A_trust_NS2";
@@ -287,6 +264,13 @@
qed "Says_S_message_form";
+(*For proofs involving analz. We again instantiate the variable to "lost".*)
+val analz_Fake_tac =
+ forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
+ forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN
+ Full_simp_tac 7 THEN
+ REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac);
+
(****
The following is to prove theorems of the form
@@ -320,45 +304,13 @@
(** Session keys are not used to encrypt other session keys **)
-(*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. *)
-goal thy
- "!!evs. evs: ns_shared lost ==> \
-\ Crypt {|NA, Agent B, Key K, X|} (shrK A) \
-\ : parts (sees lost Spy evs) & A ~: lost \
-\ --> (EX evt: ns_shared lost. K = newK evt)";
-by (parts_induct_tac 1);
-by (Auto_tac());
-val lemma = result() RS mp;
-
-
-(*EITHER describes the form of Key K when the following message is sent,
- OR reduces it to the Fake case.*)
-goal thy
- "!!evs. [| Says S A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
-\ : set_of_list evs; \
-\ evs : ns_shared lost |] \
-\ ==> (EX evt: ns_shared lost. K = newK evt) \
-\ | Key K : analz (sees lost Spy evs)";
-by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
-by (forward_tac [lemma] 1);
-by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-by (Fast_tac 1);
-qed "Reveal_message_form";
-
(*The equality makes the induction hypothesis easier to apply*)
goal thy
"!!evs. evs : ns_shared lost ==> \
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
\ (K : newK``E | Key K : analz (sees lost Spy evs))";
by (etac ns_shared.induct 1);
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by (dtac Reveal_message_form 8);
-by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac));
+by analz_Fake_tac;
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
by (ALLGOALS
(asm_simp_tac
@@ -366,8 +318,8 @@
@ pushes)
setloop split_tac [expand_if])));
(** LEVEL 6 **)
-(*Reveal case 2, NS3, Fake*)
-by (EVERY (map spy_analz_tac [7,5,2]));
+(*NS3, Fake*)
+by (EVERY (map spy_analz_tac [5,2]));
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
(*NS3, NS2, Base*)
by (REPEAT (Fast_tac 3));
@@ -393,10 +345,8 @@
\ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
\ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by (REPEAT_FIRST (eresolve_tac [conjE, bexE, disjE] ORELSE' hyp_subst_tac));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
-by (step_tac (!claset delrules [conjI]) 1);
+by (Step_tac 1);
(*NS3*)
by (ex_strip_tac 2);
by (Fast_tac 2);
@@ -438,9 +388,7 @@
\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac ns_shared.induct 1);
-by (forward_tac [Reveal_message_form] 8);
-by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
+by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
@@ -450,9 +398,9 @@
by (fast_tac (!claset addIs [parts_insertI]
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset)) 2);
-(*Revl case 2, OR4, OR2, Fake*)
+(*OR4, OR2, Fake*)
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
-(*NS3 and Revl subcases*) (**LEVEL 7 **)
+(*NS3 and Oops subcases*) (**LEVEL 7 **)
by (step_tac (!claset delrules [impCE]) 1);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
be conjE 2;
@@ -555,11 +503,11 @@
val lemma = result();
goal thy
- "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs); \
\ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \
-\ : set_of_list evs; \
+\ : set_of_list evs; \
\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
+\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
\ ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
--- a/src/HOL/Auth/NS_Shared.thy Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Mon Oct 28 12:55:24 1996 +0100
@@ -67,10 +67,11 @@
==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
(*This message models possible leaks of session keys.
- The two Nonces identify the protocol run.*)
- Revl "[| evs: ns_shared lost; A ~= Spy;
- Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
- Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+ The two Nonces identify the protocol run: the rule insists upon
+ the true senders in order to make them accurate.*)
+ Oops "[| evs: ns_shared lost; A ~= Spy;
+ Says B A (Crypt (Nonce NB) K) : set_of_list evs;
+ Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
: set_of_list evs |]
==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
--- a/src/HOL/Auth/OtwayRees_AN.ML Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Mon Oct 28 12:55:24 1996 +0100
@@ -59,16 +59,15 @@
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "OR4_analz_sees_Spy";
-goal thy "!!evs. Says B' A (Crypt {|N,Agent A,B,K|} K') : set_of_list evs ==> \
-\ K : parts (sees lost Spy evs)";
+goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, 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
+(*OR4_analz_sees_Spy lets us treat those cases using the same
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 Spy. *)
+ proofs, since Fake messages originate from the Spy. *)
bind_thm ("OR4_parts_sees_Spy",
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
@@ -77,7 +76,7 @@
harder to complete, since simplification does less for us.*)
val parts_Fake_tac =
forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
- forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 7;
+ forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
fun parts_induct_tac i = SELECT_GOAL
@@ -95,34 +94,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! ***)
@@ -134,7 +126,7 @@
The Union over C is essential for the induction! *)
goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
@@ -224,39 +216,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, Agent A, B, 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.*)
goal thy
- "!!evs. [| Says B' A (Crypt {|N, Agent A, B, 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]) 1);
-by (fast_tac (!claset addSDs [Says_Crypt_lost]) 1);
-qed "Reveal_message_form";
+ "!!evs. [| Says Server B \
+\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
+\ Crypt {|NB, Agent A, Agent B, 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")] 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);
(****
@@ -280,16 +260,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*)
(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, Fake*)
-by (EVERY (map spy_analz_tac [6, 4, 2]));
-(*Reveal case 1, OR3, Base*)
+(*OR4, Fake*)
+by (EVERY (map spy_analz_tac [4,2]));
+(*Oops, OR3, Base*)
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
qed_spec_mp "analz_image_newK";
@@ -306,8 +285,6 @@
(*** 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. \
@@ -387,21 +364,6 @@
qed "A_trust_OR4";
-(*Describes the form of K and NA when the Server sends this message.*)
-goal thy
- "!!evs. [| Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, 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 **)
@@ -412,40 +374,31 @@
\ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \
\ Crypt {|NB, Agent A, Agent B, 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,
analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
-(** LEVEL 4 **)
(*OR3*)
by (fast_tac (!claset addSIs [parts_insertI]
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset addsimps [parts_insert2])) 2);
-(*Reveal case 2, OR4, Fake*)
+(*OR4, 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));
+(*Oops*)
by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
val lemma = result() RS mp RS mp RSN(2,rev_notE);
goal thy
"!!evs. [| Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
-\ Says A Spy {|NA, K|} ~: set_of_list evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
+\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
+\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : 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);
by (fast_tac (!claset addSEs [lemma]) 1);
@@ -455,9 +408,9 @@
goal thy
"!!evs. [| C ~: {A,B,Server}; \
\ Says Server B \
-\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
-\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
-\ Says A Spy {|NA, K|} ~: set_of_list evs; \
+\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \
+\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : 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);
--- a/src/HOL/Auth/OtwayRees_AN.thy Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Mon Oct 28 12:55:24 1996 +0100
@@ -51,7 +51,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 {|X,
Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
: set_of_list evs;
@@ -59,12 +59,13 @@
: set_of_list evs |]
==> Says B A 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 (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A))
- : set_of_list evs;
- Says A B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
- ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
+ (*This message models possible leaks of session keys. The nonces
+ identify the protocol run. B is not assumed to know shrK A.*)
+ Oops "[| evs: otway lost; B ~= Spy;
+ Says Server B
+ {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A),
+ Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
+ : set_of_list evs |]
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Mon Oct 28 12:55:24 1996 +0100
@@ -68,11 +68,11 @@
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,
@@ -87,46 +87,46 @@
val parts_Fake_tac =
forward_tac [OR2_parts_sees_Spy] 4 THEN
forward_tac [OR4_parts_sees_Spy] 6 THEN
- forward_tac [Reveal_parts_sees_Spy] 7;
+ forward_tac [Oops_parts_sees_Spy] 7;
+
+(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
+fun parts_induct_tac i = SELECT_GOAL
+ (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
+ (*Fake message*)
+ TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2)) THEN
+ (*Base case*)
+ fast_tac (!claset addss (!simpset)) 1 THEN
+ ALLGOALS Asm_simp_tac) i;
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
sends messages containing X! **)
-(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
+(*Spy never sees another agent's shared key! (unless it's lost at start)*)
goal thy
- "!!evs. [| evs : otway; A ~: lost |] \
-\ ==> Key (shrK A) ~: parts (sees lost Spy evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
+ "!!evs. evs : otway \
+\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
+by (parts_induct_tac 1);
by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-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; \
-\ 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 \
+\ ==> (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 |] ==> 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! ***)
@@ -139,10 +139,7 @@
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
@@ -214,9 +211,7 @@
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
+by (parts_induct_tac 1);
(*OR1 and OR3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
(*Fake, OR2, OR4: these messages send unknown (X) components*)
@@ -242,7 +237,30 @@
Addsimps [new_keys_not_used, new_keys_not_analzd];
-(** Lemmas concerning the form of items passed in messages **)
+
+(*** Proofs involving analz ***)
+
+(*Describes the form of K and NA when the Server sends this message. Also
+ for Oops case.*)
+goal thy
+ "!!evs. [| Says Server B \
+\ {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+\ evs : otway |] \
+\ ==> (EX evt: otway. 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.*)
+val analz_Fake_tac =
+ dtac OR2_analz_sees_Spy 4 THEN
+ dtac OR4_analz_sees_Spy 6 THEN
+ forward_tac [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);
(****
@@ -258,40 +276,6 @@
(** Session keys are not used to encrypt other session keys **)
-(*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
- assumptions on A are needed to prevent its being a Faked message. (Based
- on NS_Shared/Says_S_message_form) *)
-goal thy
- "!!evs. evs: otway ==> \
-\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
-\ A ~: lost --> \
-\ (EX evt:otway. K = newK evt)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
-val lemma = result() RS mp;
-
-
-(*EITHER describes the form of Key K when the following message is sent,
- OR reduces it to the Fake case.*)
-goal thy
- "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX evt:otway. K = newK evt) | Key K : analz (sees lost Spy evs)";
-by (case_tac "A : lost" 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
- addss (!simpset)) 1);
-by (forward_tac [lemma] 1);
-by (fast_tac (!claset addEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
-by (Fast_tac 1);
-qed "Reveal_message_form";
-
-
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
"!!evs. (Key K : analz (Key``nE Un sEe)) --> \
@@ -307,21 +291,18 @@
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
\ (K : newK``E | Key K : analz (sees lost Spy evs))";
by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (dtac Reveal_message_form 7);
+by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, lemma]));
-by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
-by (ALLGOALS (*Takes 28 secs*)
+by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
(** LEVEL 7 **)
-(*Reveal case 2, OR4, OR2, Fake*)
-by (EVERY (map spy_analz_tac [7,5,3,2]));
-(*Reveal case 1, OR3, Base*)
-by (Auto_tac());
+(*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";
@@ -335,82 +316,13 @@
qed "analz_insert_Key_newK";
-(*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 |] \
-\ ==> (EX evt:otway. 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 addIs [less_SucI] addss (!simpset))));
-qed "Says_Server_message_form";
-
-
-(*Crucial security property, but not itself enough to guarantee correctness!
- The need for quantification over N, C seems to indicate the problem.
- Omitting the Reveal message from the description deprives us of even
- this clue. *)
-goal thy
- "!!evs. [| A ~: lost; B ~: lost; evs : otway; evt : otway |] \
-\ ==> Says Server B \
-\ {|NA, Crypt {|NA, Key K|} (shrK A), \
-\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
-\ (ALL N C. Says C Spy {|N, Key K|} ~: set_of_list evs) --> \
-\ Key K ~: analz (sees lost Spy evs)";
-by (etac otway.induct 1);
-by (dtac OR2_analz_sees_Spy 4);
-by (dtac OR4_analz_sees_Spy 6);
-by (dtac Reveal_message_form 7);
-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,
- analz_insert_Key_newK] @ pushes)
- setloop split_tac [expand_if])));
-(** LEVEL 6 **)
-(*Reveal case 1*)
-by (Fast_tac 5);
-(*OR3*)
-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*)
-by (rtac conjI 3);
-by (REPEAT (spy_analz_tac 1));
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-
-
-(*WEAK VERSION: NEED TO ELIMINATE QUANTIFICATION OVER N, C!!*)
-goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
-\ (ALL N C. Says C Spy {|N, K|} ~: set_of_list evs); \
-\ A ~: lost; B ~: lost; evs : otway |] \
-\ ==> K ~: analz (sees lost Spy evs)";
-by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
-by (fast_tac (!claset addSEs [lemma]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(*** Attempting to prove stronger properties ***)
-
-(** 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);
+(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway ==> \
-\ 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 ==> \
+\ 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);
@@ -426,16 +338,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 |] \
-\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
+\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
by (dtac lemma 1);
by (REPEAT (etac exE 1));
(*Duplicate the assumption*)
@@ -444,59 +351,91 @@
qed "unique_session_keys";
+(*Crucial security property, but not itself enough to guarantee correctness!*)
+goal thy
+ "!!evs. [| A ~: lost; B ~: lost; evs : otway; evt : otway |] \
+\ ==> Says Server B \
+\ {|NA, Crypt {|NA, Key K|} (shrK A), \
+\ Crypt {|NB, Key K|} (shrK B)|} : 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 (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 addSIs [parts_insertI]
+ addEs [Says_imp_old_keys RS less_irrefl]
+ addss (!simpset addsimps [parts_insert2])) 3);
+(*OR4, OR2, Fake*)
+by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
+(*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 B Spy {|NA, NB, K|} ~: set_of_list evs; \
+\ A ~: lost; B ~: lost; evs : otway |] \
+\ ==> K ~: analz (sees lost Spy evs)";
+by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
+by (fast_tac (!claset addSEs [lemma]) 1);
+qed "Spy_not_see_encrypted_key";
+
+
+(*** Attempting to prove stronger properties ***)
+
(*Only OR1 can have caused such a part of a message to appear.
I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
Perhaps it's because OR2 has two similar-looking encrypted messages in
this version.*)
goal thy
- "!!evs. [| A ~: lost; A ~= B; evs : otway |] \
-\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
+ "!!evs. [| A ~: lost; A ~= B; evs : otway |] \
+\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \
\ : parts (sees lost Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
+\ Says A B {|NA, Agent A, Agent B, \
\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
\ : set_of_list evs";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 2);
-by (Auto_tac());
+by (parts_induct_tac 1);
+by (Fast_tac 1);
qed_spec_mp "Crypt_imp_OR1";
-(*This key property is FALSE. Somebody could make a fake message to Server
+(*Crucial property: If the encrypted message appears, and A has used NA
+ to start a run, then it originated with the Server!*)
+(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
goal thy
"!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \
\ ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
+\ Says A B {|NA, Agent A, Agent B, \
\ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \
-\ : set_of_list evs --> \
-\ (EX B NB. Says Server B \
-\ {|NA, \
+\ : set_of_list evs --> \
+\ (EX B NB. Says Server B \
+\ {|NA, \
\ Crypt {|NA, Key K|} (shrK A), \
\ Crypt {|NB, Key K|} (shrK B)|} \
\ : set_of_list evs)";
-by (etac otway.induct 1);
-by parts_Fake_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Fake*)
-by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+by (parts_induct_tac 1);
(*OR1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset addSIs [parts_insertI]
addSEs partsEs
addEs [Says_imp_old_nonces RS less_irrefl]
addss (!simpset)) 1);
-(*OR3 and OR4*) (** LEVEL 5 **)
(*OR4*)
by (REPEAT (Safe_step_tac 2));
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
by (fast_tac (!claset addSIs [Crypt_imp_OR1]
addEs partsEs
addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
-(*OR3*) (** LEVEL 8 **)
+(*OR3*) (** LEVEL 5 **)
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
by (step_tac (!claset delrules [disjCI, impCE]) 1);
(*The hypotheses at this point suggest an attack in which nonce NA is used
@@ -511,7 +450,7 @@
Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
: set_of_list evsa
*)
-writeln "GIVE UP!";
+writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
(*Thus the key property A_can_trust probably fails too.*)
--- a/src/HOL/Auth/OtwayRees_Bad.thy Sun Oct 27 13:47:02 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Mon Oct 28 12:55:24 1996 +0100
@@ -61,21 +61,18 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.*)
- OR4 "[| evs: otway; A ~= B; B ~= Server;
+ OR4 "[| evs: otway; 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', Nonce NB, X''|}
: set_of_list evs |]
==> Says B A {|Nonce NA, X|} # evs : otway"
- (*This message models possible leaks of session keys. Alice's Nonce
- identifies the protocol run.*)
- Revl "[| evs: otway; 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; 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"
+ ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
end