--- a/src/HOL/Auth/Message.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/Message.thy Thu Apr 12 12:45:05 2001 +0200
@@ -135,6 +135,8 @@
use "Message_lemmas.ML"
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+
lemma Fake_parts_insert_in_Un:
"[|Z \<in> parts (insert X H); X: synth (analz H)|]
==> Z \<in> synth (analz H) \<union> parts H";
--- a/src/HOL/Auth/Message_lemmas.ML Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/Message_lemmas.ML Thu Apr 12 12:45:05 2001 +0200
@@ -50,7 +50,7 @@
by Auto_tac;
qed "Friend_image_eq";
-Goal "(Key x \\<in> Key`A) = (x:A)";
+Goal "(Key x \\<in> Key`A) = (x\\<in>A)";
by Auto_tac;
qed "Key_image_eq";
@@ -82,12 +82,12 @@
by (Blast_tac 1);
qed "keysFor_Un";
-Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
+Goalw [keysFor_def] "keysFor (\\<Union>i\\<in>A. H i) = (\\<Union>i\\<in>A. keysFor (H i))";
by (Blast_tac 1);
qed "keysFor_UN";
(*Monotonicity*)
-Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
+Goalw [keysFor_def] "G\\<subseteq>H ==> keysFor(G) \\<subseteq> keysFor(H)";
by (Blast_tac 1);
qed "keysFor_mono";
@@ -154,7 +154,7 @@
MPair_parts is left as SAFE because it speeds up proofs.
The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*)
-Goal "H <= parts(H)";
+Goal "H \\<subseteq> parts(H)";
by (Blast_tac 1);
qed "parts_increasing";
@@ -167,13 +167,13 @@
qed "parts_empty";
Addsimps [parts_empty];
-Goal "X: parts{} ==> P";
+Goal "X\\<in> parts{} ==> P";
by (Asm_full_simp_tac 1);
qed "parts_emptyE";
AddSEs [parts_emptyE];
(*WARNING: loops if H = {Y}, therefore must not be repeated!*)
-Goal "X: parts H ==> EX Y:H. X: parts {Y}";
+Goal "X\\<in> parts H ==> \\<exists>Y\\<in>H. X\\<in> parts {Y}";
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_singleton";
@@ -181,11 +181,11 @@
(** Unions **)
-Goal "parts(G) Un parts(H) <= parts(G Un H)";
+Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)";
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
val parts_Un_subset1 = result();
-Goal "parts(G Un H) <= parts(G) Un parts(H)";
+Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)";
by (rtac subsetI 1);
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
@@ -207,17 +207,17 @@
by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
qed "parts_insert2";
-Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
+Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)";
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
val parts_UN_subset1 = result();
-Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
+Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))";
by (rtac subsetI 1);
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
val parts_UN_subset2 = result();
-Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
+Goal "parts(\\<Union>x\\<in>A. H x) = (\\<Union>x\\<in>A. parts(H x))";
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
qed "parts_UN";
@@ -227,13 +227,13 @@
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
parts_UN RS equalityD1 RS subsetD RS UN_E];
-Goal "insert X (parts H) <= parts(insert X H)";
+Goal "insert X (parts H) \\<subseteq> parts(insert X H)";
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
qed "parts_insert_subset";
(** Idempotence and transitivity **)
-Goal "X: parts (parts H) ==> X: parts H";
+Goal "X\\<in> parts (parts H) ==> X\\<in> parts H";
by (etac parts.induct 1);
by (ALLGOALS Blast_tac);
qed "parts_partsD";
@@ -244,19 +244,19 @@
qed "parts_idem";
Addsimps [parts_idem];
-Goal "[| X: parts G; G <= parts H |] ==> X: parts H";
+Goal "[| X\\<in> parts G; G \\<subseteq> parts H |] ==> X\\<in> parts H";
by (dtac parts_mono 1);
by (Blast_tac 1);
qed "parts_trans";
(*Cut*)
-Goal "[| Y: parts (insert X G); X: parts H |] \
-\ ==> Y: parts (G Un H)";
+Goal "[| Y\\<in> parts (insert X G); X\\<in> parts H |] \
+\ ==> Y\\<in> parts (G Un H)";
by (etac parts_trans 1);
by Auto_tac;
qed "parts_cut";
-Goal "X: parts H ==> parts (insert X H) = parts H";
+Goal "X\\<in> parts H ==> parts (insert X H) = parts H";
by (fast_tac (claset() addSDs [parts_cut]
addIs [parts_insertI]
addss (simpset())) 1);
@@ -326,7 +326,7 @@
(*In any message, there is an upper bound N on its greatest nonce.*)
-Goal "EX N. ALL n. N<=n --> Nonce n \\<notin> parts {msg}";
+Goal "\\<exists>N. \\<forall>n. N\\<le>n --> Nonce n \\<notin> parts {msg}";
by (induct_tac "msg" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
(*MPair case: blast_tac works out the necessary sum itself!*)
@@ -350,11 +350,11 @@
AddSEs [MPair_analz]; (*Making it safe speeds up proofs*)
-Goal "H <= analz(H)";
+Goal "H \\<subseteq> analz(H)";
by (Blast_tac 1);
qed "analz_increasing";
-Goal "analz H <= parts H";
+Goal "analz H \\<subseteq> parts H";
by (rtac subsetI 1);
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
@@ -391,11 +391,11 @@
(*Converse fails: we can analz more from the union than from the
separate parts, as a key in one might decrypt a message in the other*)
-Goal "analz(G) Un analz(H) <= analz(G Un H)";
+Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)";
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
qed "analz_Un";
-Goal "insert X (analz H) <= analz(insert X H)";
+Goal "insert X (analz H) \\<subseteq> analz(insert X H)";
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
qed "analz_insert";
@@ -447,7 +447,7 @@
qed "analz_insert_Crypt";
Goal "Key (invKey K) \\<in> analz H ==> \
-\ analz (insert (Crypt K X) H) <= \
+\ analz (insert (Crypt K X) H) \\<subseteq> \
\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (eres_inst_tac [("xa","x")] analz.induct 1);
@@ -455,7 +455,7 @@
val lemma1 = result();
Goal "Key (invKey K) \\<in> analz H ==> \
-\ insert (Crypt K X) (analz (insert X H)) <= \
+\ insert (Crypt K X) (analz (insert X H)) \\<subseteq> \
\ analz (insert (Crypt K X) H)";
by Auto_tac;
by (eres_inst_tac [("xa","x")] analz.induct 1);
@@ -487,7 +487,7 @@
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
(*This rule supposes "for the sake of argument" that we have the key.*)
-Goal "analz (insert (Crypt K X) H) <= \
+Goal "analz (insert (Crypt K X) H) \\<subseteq> \
\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (etac analz.induct 1);
@@ -506,7 +506,7 @@
(** Idempotence and transitivity **)
-Goal "X: analz (analz H) ==> X: analz H";
+Goal "X\\<in> analz (analz H) ==> X\\<in> analz H";
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
qed "analz_analzD";
@@ -517,13 +517,13 @@
qed "analz_idem";
Addsimps [analz_idem];
-Goal "[| X: analz G; G <= analz H |] ==> X: analz H";
+Goal "[| X\\<in> analz G; G \\<subseteq> analz H |] ==> X\\<in> analz H";
by (dtac analz_mono 1);
by (Blast_tac 1);
qed "analz_trans";
(*Cut; Lemma 2 of Lowe*)
-Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H";
+Goal "[| Y\\<in> analz (insert X H); X\\<in> analz H |] ==> Y\\<in> analz H";
by (etac analz_trans 1);
by (Blast_tac 1);
qed "analz_cut";
@@ -535,15 +535,15 @@
(*This rewrite rule helps in the simplification of messages that involve
the forwarding of unknown components (X). Without it, removing occurrences
of X can be very complicated. *)
-Goal "X: analz H ==> analz (insert X H) = analz H";
+Goal "X\\<in> analz H ==> analz (insert X H) = analz H";
by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
qed "analz_insert_eq";
(** A congruence rule for "analz" **)
-Goal "[| analz G <= analz G'; analz H <= analz H' \
-\ |] ==> analz (G Un H) <= analz (G' Un H')";
+Goal "[| analz G \\<subseteq> analz G'; analz H \\<subseteq> analz H' \
+\ |] ==> analz (G Un H) \\<subseteq> analz (G' Un H')";
by (Clarify_tac 1);
by (etac analz.induct 1);
by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
@@ -562,20 +562,19 @@
qed "analz_insert_cong";
(*If there are no pairs or encryptions then analz does nothing*)
-Goal "[| ALL X Y. {|X,Y|} \\<notin> H; ALL X K. Crypt K X \\<notin> H |] ==> \
-\ analz H = H";
+Goal "[| \\<forall>X Y. {|X,Y|} \\<notin> H; \\<forall>X K. Crypt K X \\<notin> H |] ==> analz H = H";
by Safe_tac;
by (etac analz.induct 1);
by (ALLGOALS Blast_tac);
qed "analz_trivial";
(*These two are obsolete (with a single Spy) but cost little to prove...*)
-Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
+Goal "X\\<in> analz (\\<Union>i\\<in>A. analz (H i)) ==> X\\<in> analz (\\<Union>i\\<in>A. H i)";
by (etac analz.induct 1);
by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
val lemma = result();
-Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
+Goal "analz (\\<Union>i\\<in>A. analz (H i)) = analz (\\<Union>i\\<in>A. H i)";
by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
qed "analz_UN_analz";
Addsimps [analz_UN_analz];
@@ -583,7 +582,7 @@
(**** Inductive relation "synth" ****)
-Goal "H <= synth(H)";
+Goal "H \\<subseteq> synth(H)";
by (Blast_tac 1);
qed "synth_increasing";
@@ -591,17 +590,17 @@
(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
-Goal "synth(G) Un synth(H) <= synth(G Un H)";
+Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)";
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
qed "synth_Un";
-Goal "insert X (synth H) <= synth(insert X H)";
+Goal "insert X (synth H) \\<subseteq> synth(insert X H)";
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
qed "synth_insert";
(** Idempotence and transitivity **)
-Goal "X: synth (synth H) ==> X: synth H";
+Goal "X\\<in> synth (synth H) ==> X\\<in> synth H";
by (etac synth.induct 1);
by (ALLGOALS Blast_tac);
qed "synth_synthD";
@@ -611,13 +610,13 @@
by (Blast_tac 1);
qed "synth_idem";
-Goal "[| X: synth G; G <= synth H |] ==> X: synth H";
+Goal "[| X\\<in> synth G; G \\<subseteq> synth H |] ==> X\\<in> synth H";
by (dtac synth_mono 1);
by (Blast_tac 1);
qed "synth_trans";
(*Cut; Lemma 2 of Lowe*)
-Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H";
+Goal "[| Y\\<in> synth (insert X H); X\\<in> synth H |] ==> Y\\<in> synth H";
by (etac synth_trans 1);
by (Blast_tac 1);
qed "synth_cut";
@@ -688,23 +687,23 @@
(** For reasoning about the Fake rule in traces **)
-Goal "X: G ==> parts(insert X H) <= parts G Un parts H";
+Goal "X\\<in> G ==> parts(insert X H) \\<subseteq> parts G Un parts H";
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
by (Blast_tac 1);
qed "parts_insert_subset_Un";
(*More specifically for Fake. Very occasionally we could do with a version
- of the form parts{X} <= synth (analz H) Un parts H *)
-Goal "X: synth (analz H) ==> \
-\ parts (insert X H) <= synth (analz H) Un parts H";
+ of the form parts{X} \\<subseteq> synth (analz H) Un parts H *)
+Goal "X\\<in> synth (analz H) ==> \
+\ parts (insert X H) \\<subseteq> synth (analz H) Un parts H";
by (dtac parts_insert_subset_Un 1);
by (Full_simp_tac 1);
by (Blast_tac 1);
qed "Fake_parts_insert";
(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*)
-Goal "X: synth (analz G) ==> \
-\ analz (insert X H) <= synth (analz G) Un analz (G Un H)";
+Goal "X\\<in> synth (analz G) ==> \
+\ analz (insert X H) \\<subseteq> synth (analz G) Un analz (G Un H)";
by (rtac subsetI 1);
by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1);
by (blast_tac (claset() addIs [impOfSubs analz_mono,
@@ -713,11 +712,11 @@
by (Blast_tac 1);
qed "Fake_analz_insert";
-Goal "(X: analz H & X: parts H) = (X: analz H)";
+Goal "(X\\<in> analz H & X\\<in> parts H) = (X\\<in> analz H)";
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
val analz_conj_parts = result();
-Goal "(X: analz H | X: parts H) = (X: parts H)";
+Goal "(X\\<in> analz H | X\\<in> parts H) = (X\\<in> parts H)";
by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
val analz_disj_parts = result();
--- a/src/HOL/Auth/NS_Shared.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Thu Apr 12 12:45:05 2001 +0200
@@ -20,8 +20,8 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake: "\<lbrakk>evs \<in> ns_shared; X \<in> synth (analz (spies evs))\<rbrakk>
- \<Longrightarrow> Says Spy B X # evs \<in> ns_shared"
+ Fake: "\<lbrakk>evsf \<in> ns_shared; X \<in> synth (analz (spies evsf))\<rbrakk>
+ \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
(*Alice initiates a protocol run, requesting to talk to any B*)
NS1: "\<lbrakk>evs1 \<in> ns_shared; Nonce NA \<notin> used evs1\<rbrakk>
@@ -74,10 +74,8 @@
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body [dest]
-declare MPair_parts [elim!] (*can speed up some proofs*)
-
-declare analz_subset_parts [THEN subsetD, dest]
-declare Fake_parts_insert [THEN subsetD, dest]
+declare Fake_parts_insert_in_Un [dest]
+declare analz_into_parts [dest]
declare image_eq_UN [simp] (*accelerates proofs involving nested images*)
@@ -123,7 +121,6 @@
apply blast+;
done
-
lemma Spy_analz_shrK [simp]:
"evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
@@ -310,8 +307,7 @@
Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
Says B A (Crypt K (Nonce NB)) \<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply analz_mono_contra
-apply simp_all
+apply (analz_mono_contra, simp_all)
apply blast (*Fake*)
(*NS2: contradiction from the assumptions
Key K \<notin> used evs2 and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
--- a/src/HOL/Auth/OtwayRees.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,411 +0,0 @@
-(* 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.
-
-Version that encrypts Nonce NB
-
-From page 244 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "B \\<noteq> Server \
-\ ==> \\<exists>K. \\<exists>evs \\<in> otway. \
-\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\ \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-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 \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> 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 \\<in> set evs; evs \\<in> otway |] ==> X \\<in> knows Spy evs";
-by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1);
-qed"Gets_imp_knows_Spy";
-AddSDs [Gets_imp_knows_Spy RS parts.Inj];
-
-
-(**** Inductive proofs about otway ****)
-
-(** For reasoning about the encrypted portion of messages **)
-
-Goal "[| Gets B {|N, Agent A, Agent B, X|} \\<in> set evs; evs \\<in> otway |] \
-\ ==> X \\<in> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
-qed "OR2_analz_knows_Spy";
-
-Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\<in> set evs; evs \\<in> otway |] \
-\ ==> X \\<in> 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|}|} \\<in> set evs \
-\ ==> K \\<in> parts (knows Spy evs)";
-by (Blast_tac 1);
-qed "Oops_parts_knows_Spy";
-
-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 \\<notin> parts (knows Spy evs).*)
-fun parts_induct_tac i =
- etac otway.induct i THEN
- ftac Oops_parts_knows_Spy (i+7) THEN
- ftac OR4_parts_knows_Spy (i+6) THEN
- ftac OR2_parts_knows_Spy (i+4) THEN
- prove_simple_subgoals_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees a good agent's shared key!*)
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*** Proofs involving analz ***)
-
-(*Describes the form of K and NA when the Server sends this message. Also
- for Oops case.*)
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ evs \\<in> otway |] \
-\ ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)";
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Simp_tac);
-by (ALLGOALS Blast_tac);
-qed "Says_Server_message_form";
-
-
-(*For proofs involving analz.*)
-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
- ftac 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 \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-****)
-
-
-(** Session keys are not used to encrypt other session keys **)
-
-(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs \\<in> otway ==> ALL K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac otway.induct 1);
-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));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-
-Goal "[| evs \\<in> otway; KAB \\<notin> range shrK |] \
-\ ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\<in> set evs; \
-\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\<in> set evs; \
-\ evs \\<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*Remaining cases: OR3 and OR4*)
-by (REPEAT (Blast_tac 1));
-qed "unique_session_keys";
-
-
-(**** Authenticity properties relating to NA ****)
-
-(*Only OR1 can have caused such a part of a message to appear.*)
-Goal "[| A \\<notin> bad; evs \\<in> otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ \\<in> set evs";
-by (parts_induct_tac 1);
-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|}|} \\<in> set evs; \
-\ A \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ \\<in> 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 "[| 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 \\<in> otway; A \\<notin> bad |] \
-\ ==> B = C";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake, OR1*)
-by (REPEAT (Blast_tac 1));
-qed "unique_NA";
-
-
-(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
- OR2 encrypts Nonce NB. It prevents the attack that can occur in the
- over-simplified version of this protocol: see OtwayRees_Bad.*)
-Goal "[| A \\<notin> bad; evs \\<in> otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
-\ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \
-\ \\<notin> parts (knows Spy evs)";
-by (parts_induct_tac 1);
-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 \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs --> \
-\ Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) \
-\ --> (\\<exists>NB. Says Server B \
-\ {|NA, \
-\ Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-(*OR1: it cannot be a new Nonce, contradiction.*)
-by (Blast_tac 1);
-(*OR4*)
-by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
-by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] addIs [unique_NA]) 1);
-qed_spec_mp "NA_Crypt_imp_Server_msg";
-
-
-(*Corollary: if A receives B's OR4 message and the nonce NA agrees
- then the key really did come from the Server! CANNOT prove this of the
- bad form of this protocol, even though we can prove
- Spy_not_see_encrypted_key*)
-Goal "[| Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
-\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
-\ A \\<notin> bad; evs \\<in> otway |] \
-\ ==> \\<exists>NB. Says Server B \
-\ {|NA, \
-\ Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
-qed "A_trusts_OR4";
-
-
-(** 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 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs --> \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac otway.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac (simpset() addcongs [conj_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- @ pushes @ split_ifs)));
-(*Oops*)
-by (blast_tac (claset() addSDs [unique_session_keys]) 4);
-(*OR4*)
-by (Blast_tac 3);
-(*OR3*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-Goal "[| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(*A's guarantee. The Oops premise quantifies over NB because A cannot know
- what it is.*)
-Goal "[| Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
-\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
-\ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
-qed "A_gets_good_key";
-
-
-(**** Authenticity properties relating to NB ****)
-
-(*Only OR2 can have caused such a part of a message to appear. We do not
- know anything about X: it does NOT have to have the right form.*)
-Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
-\ \\<in> parts (knows Spy evs); \
-\ B \\<notin> bad; evs \\<in> otway |] \
-\ ==> \\<exists>X. Says B Server \
-\ {|NA, Agent A, Agent B, X, \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Crypt_imp_OR2";
-
-
-(** The Nonce NB uniquely identifies B's message. **)
-
-Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \\<in> parts(knows Spy evs); \
-\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \\<in> parts(knows Spy evs); \
-\ evs \\<in> otway; B \\<notin> bad |] \
-\ ==> NC = NA & C = A";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-(*Fake, OR2*)
-by (REPEAT (Blast_tac 1));
-qed "unique_NB";
-
-(*If the encrypted message appears, and B has used Nonce NB,
- then it originated with the Server! Quite messy proof.*)
-Goal "[| B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Crypt (shrK B) {|NB, Key K|} \\<in> parts (knows Spy evs) \
-\ --> (ALL X'. Says B Server \
-\ {|NA, Agent A, Agent B, X', \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \
-\ \\<in> set evs \
-\ --> Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \
-\ \\<in> set evs)";
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-(*OR1: it cannot be a new Nonce, contradiction.*)
-by (Blast_tac 1);
-(*OR4*)
-by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2);
-(*OR3: needs AddSEs [MPair_parts] or it takes forever!*)
-by (blast_tac (claset() addDs [unique_NB]
- addEs [nonce_OR1_OR2_E]) 1);
-qed_spec_mp "NB_Crypt_imp_Server_msg";
-
-
-(*Guarantee for B: if it gets a message with matching NB then the Server
- has sent the correct message.*)
-Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ \\<in> set evs; \
-\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says Server B \
-\ {|NA, \
-\ Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
-qed "B_trusts_OR3";
-
-
-(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-Goal "[| Says B Server {|NA, Agent A, Agent B, X', \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ \\<in> set evs; \
-\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
-qed "B_gets_good_key";
-
-
-Goal "[| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ B \\<notin> bad; evs \\<in> otway |] \
-\ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X, \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 3);
-by (ALLGOALS Blast_tac);
-qed "OR3_imp_OR2";
-
-
-(*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 "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} \\<in> set evs; \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, \
-\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\
-\ \\<in> set evs";
-by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj]
- addSDs [A_trusts_OR4, OR3_imp_OR2]) 1);
-qed "A_auths_B";
--- a/src/HOL/Auth/OtwayRees.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Apr 12 12:45:05 2001 +0200
@@ -1,44 +1,49 @@
-(*
+(* 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
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 +
+theory OtwayRees = Shared:
-consts otway :: event list set
+consts otway :: "event list set"
inductive "otway"
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[] \\<in> otway"
-
- (** These rules allow agents to send messages to themselves **)
+ Nil: "[] \<in> otway"
(*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 "[| evsf \\<in> otway; X \\<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf : otway"
+ Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> otway"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> otway; Says A B X : set evsr |]
- ==> Gets B X # evsr : otway"
+ Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |]
+ ==> Gets B X # evsr \<in> otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1 \\<in> otway; Nonce NA \\<notin> used evs1 |]
- ==> Says A B {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+ OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
+ ==> Says A B {|Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 : otway"
(*Bob's response to Alice's message. Note that NB is encrypted.*)
- OR2 "[| evs2 \\<in> otway; Nonce NB \\<notin> used evs2;
+ OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
- ==> Says B Server
- {|Nonce NA, Agent A, Agent B, X,
+ ==> Says B Server
+ {|Nonce NA, Agent A, Agent B, X,
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
# evs2 : otway"
@@ -46,23 +51,23 @@
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs3 \\<in> otway; Key KAB \\<notin> used evs3;
- Gets Server
- {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
+ OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
+ 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|}|}
: set evs3 |]
- ==> Says Server B
- {|Nonce NA,
+ ==> Says Server B
+ {|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
# evs3 : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
- Need B \\<noteq> Server because we allow messages to self.*)
- OR4 "[| evs4 \\<in> otway; B \\<noteq> Server;
- Says B Server {|Nonce NA, Agent A, Agent B, X',
+ Need B \<noteq> Server because we allow messages to self.*)
+ OR4: "[| evs4 \<in> otway; B \<noteq> Server;
+ Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}
: set evs4;
@@ -72,9 +77,391 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evso \\<in> otway;
+ Oops: "[| evso \<in> otway;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
: set evso |]
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "B \<noteq> Server
+ ==> \<exists>K. \<exists>evs \<in> otway.
+ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] otway.Nil
+ [THEN otway.OR1, THEN otway.Reception,
+ THEN otway.OR2, THEN otway.Reception,
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply possibility
+done
+
+lemma Gets_imp_Says [dest!]:
+ "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule otway.induct)
+apply auto
+done
+
+
+(**** Inductive proofs about otway ****)
+
+(** For reasoning about the encrypted portion of messages **)
+
+lemma OR2_analz_knows_Spy:
+ "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemma OR4_analz_knows_Spy:
+ "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+(*These lemmas assist simplification by removing forwarded X-variables.
+ We can replace them by rewriting with parts_insert2 and proving using
+ dest: parts_cut, but the proofs become more difficult.*)
+lemmas OR2_parts_knows_Spy =
+ OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+
+(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
+ some reason proofs work without them!*)
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+
+(*** Proofs involving analz ***)
+
+(*Describes the form of K and NA when the Server sends this message. Also
+ for Oops case.*)
+lemma Says_Server_message_form:
+ "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ evs \<in> otway |]
+ ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
+apply (erule rev_mp, erule otway.induct, simp_all)
+apply blast
+done
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*The equality makes the induction hypothesis easier to apply*)
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> otway ==>
+ \<forall>K KK. KK <= -(range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply (drule_tac [4] OR2_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+done
+
+
+lemma analz_insert_freshK:
+ "[| evs \<in> otway; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
+ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+ evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule otway.induct, simp_all)
+(*Remaining cases: OR3 and OR4*)
+apply blast+
+done
+
+
+(**** Authenticity properties relating to NA ****)
+
+(*Only OR1 can have caused such a part of a message to appear.*)
+lemma Crypt_imp_OR1 [rule_format]:
+ "[| A \<notin> bad; evs \<in> otway |]
+ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
+ Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ \<in> set evs"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Crypt_imp_OR1_Gets:
+ "[| Gets B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ A \<notin> bad; evs \<in> otway |]
+ ==> Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ \<in> set evs"
+by (blast dest: Crypt_imp_OR1)
+
+
+(** The Nonce NA uniquely identifies A's message. **)
+
+lemma unique_NA:
+ "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
+ Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs);
+ evs \<in> otway; A \<notin> bad |]
+ ==> B = C"
+apply (erule rev_mp, erule rev_mp)
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+
+(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
+ OR2 encrypts Nonce NB. It prevents the attack that can occur in the
+ over-simplified version of this protocol: see OtwayRees_Bad.*)
+lemma no_nonce_OR1_OR2:
+ "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> otway |]
+ ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
+apply (erule rev_mp)
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+(*Crucial property: If the encrypted message appears, and A has used NA
+ to start a run, then it originated with the Server!*)
+lemma NA_Crypt_imp_Server_msg [rule_format]:
+ "[| A \<notin> bad; evs \<in> otway |]
+ ==> Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs -->
+ Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs)
+ --> (\<exists>NB. Says Server B
+ {|NA,
+ Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast
+(*OR1: it cannot be a new Nonce, contradiction.*)
+apply blast
+(*OR3*)
+apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
+(*OR4*)
+apply (blast intro!: Crypt_imp_OR1)
+done
+
+
+(*Corollary: if A receives B's OR4 message and the nonce NA agrees
+ then the key really did come from the Server! CANNOT prove this of the
+ bad form of this protocol, even though we can prove
+ Spy_not_see_encrypted_key*)
+lemma A_trusts_OR4:
+ "[| Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
+ A \<notin> bad; evs \<in> otway |]
+ ==> \<exists>NB. Says Server B
+ {|NA,
+ Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|}
+ \<in> set evs"
+by (blast intro!: NA_Crypt_imp_Server_msg)
+
+
+(** 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 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply (drule_tac [4] OR2_analz_knows_Spy)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
+apply spy_analz (*Fake*)
+(*OR3, OR4, Oops*)
+apply (blast dest: unique_session_keys)+
+done
+
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: Says_Server_message_form secrecy_lemma)
+
+
+(*A's guarantee. The Oops premise quantifies over NB because A cannot know
+ what it is.*)
+lemma A_gets_good_key:
+ "[| Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
+ \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
+
+
+
+(**** Authenticity properties relating to NB ****)
+
+(*Only OR2 can have caused such a part of a message to appear. We do not
+ know anything about X: it does NOT have to have the right form.*)
+lemma Crypt_imp_OR2:
+ "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> otway |]
+ ==> \<exists>X. Says B Server
+ {|NA, Agent A, Agent B, X,
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+
+(** The Nonce NB uniquely identifies B's message. **)
+
+lemma unique_NB:
+ "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs);
+ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs);
+ evs \<in> otway; B \<notin> bad |]
+ ==> NC = NA & C = A"
+apply (erule rev_mp, erule rev_mp)
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+(*Fake, OR2*)
+apply blast+
+done
+
+(*If the encrypted message appears, and B has used Nonce NB,
+ then it originated with the Server! Quite messy proof.*)
+lemma NB_Crypt_imp_Server_msg [rule_format]:
+ "[| B \<notin> bad; evs \<in> otway |]
+ ==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs)
+ --> (\<forall>X'. Says B Server
+ {|NA, Agent A, Agent B, X',
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}
+ \<in> set evs
+ --> Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|}
+ \<in> set evs)"
+apply simp
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast
+(*OR1: it cannot be a new Nonce, contradiction.*)
+(*OR2*)
+apply blast
+(*OR3: needs elim: MPair_parts or it takes forever!*)
+apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2)
+(*OR4*)
+apply (blast dest!: Crypt_imp_OR2)
+done
+
+
+(*Guarantee for B: if it gets a message with matching NB then the Server
+ has sent the correct message.*)
+lemma B_trusts_OR3:
+ "[| Says B Server {|NA, Agent A, Agent B, X',
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ \<in> set evs;
+ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ B \<notin> bad; evs \<in> otway |]
+ ==> Says Server B
+ {|NA,
+ Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|}
+ \<in> set evs"
+by (blast intro!: NB_Crypt_imp_Server_msg)
+
+
+(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+lemma B_gets_good_key:
+ "[| Says B Server {|NA, Agent A, Agent B, X',
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ \<in> set evs;
+ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)
+
+
+lemma OR3_imp_OR2:
+ "[| Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ B \<notin> bad; evs \<in> otway |]
+ ==> \<exists>X. Says B Server {|NA, Agent A, Agent B, X,
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule otway.induct, simp_all)
+apply (blast dest!: Crypt_imp_OR2)+
+done
+
+
+(*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.*)
+lemma A_auths_B:
+ "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
+ Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> \<exists>NB X. Says B Server {|NA, Agent A, Agent B, X,
+ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
+ \<in> set evs"
+by (blast dest!: A_trusts_OR4 OR3_imp_OR2)
+
end
--- a/src/HOL/Auth/OtwayRees_AN.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,285 +0,0 @@
-(* Title: HOL/Auth/OtwayRees_AN
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "otway" for the Otway-Rees protocol.
-
-Abadi-Needham version: minimal encryption, explicit messages
-
-From page 11 of
- Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
- IEEE Trans. SE 22 (1), 1996
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "B \\<noteq> Server \
-\ ==> \\<exists>K. \\<exists>evs \\<in> otway. \
-\ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
-\ \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-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 \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> 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 \\<in> set evs; evs \\<in> otway |] ==> X \\<in> 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 "[| Gets B {|X, Crypt(shrK B) X'|} \\<in> set evs; evs \\<in> otway |] \
-\ ==> X \\<in> 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|}|} \\<in> set evs \
-\ ==> K \\<in> parts (knows Spy evs)";
-by (Blast_tac 1);
-qed "Oops_parts_knows_Spy";
-
-bind_thm ("OR4_parts_knows_Spy",
- OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-
-(*For proving the easier theorems about X \\<notin> parts (knows Spy evs).*)
-fun parts_induct_tac i =
- etac otway.induct i THEN
- ftac Oops_parts_knows_Spy (i+7) THEN
- ftac OR4_parts_knows_Spy (i+6) THEN
- prove_simple_subgoals_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees a good agent's shared key!*)
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*** Proofs involving analz ***)
-
-(*Describes the form of K and NA when the Server sends this message.*)
-Goal "[| Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs; \
-\ evs \\<in> otway |] \
-\ ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)";
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "Says_Server_message_form";
-
-
-(*For proofs involving analz.*)
-val analz_knows_Spy_tac =
- dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN
- ftac 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 \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-****)
-
-
-(** Session keys are not used to encrypt other session keys **)
-
-(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs \\<in> otway ==> \
-\ ALL K KK. KK <= -(range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac otway.induct 1);
-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));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-
-Goal "[| evs \\<in> otway; KAB \\<notin> range shrK |] ==> \
-\ Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-Goal "[| Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} \
-\ \\<in> set evs; \
-\ Says Server B' \
-\ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|}, \
-\ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|} \
-\ \\<in> set evs; \
-\ evs \\<in> otway |] \
-\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*Remaining cases: OR3 and OR4*)
-by (REPEAT (Blast_tac 1));
-qed "unique_session_keys";
-
-
-
-(**** Authenticity properties relating to NA ****)
-
-(*If the encrypted message appears then it originated with the Server!*)
-Goal "[| A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
-\ --> (\\<exists>NB. Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-(*OR3*)
-by (Blast_tac 1);
-qed_spec_mp "NA_Crypt_imp_Server_msg";
-
-
-(*Corollary: if A receives B's OR4 message then it originated with the Server.
- Freshness may be inferred from nonce NA.*)
-Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
-\ \\<in> set evs; \
-\ A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> \\<exists>NB. Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1);
-qed "A_trusts_OR4";
-
-
-(** 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 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs --> \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac otway.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac (simpset() addcongs [conj_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- @ pushes @ split_ifs)));
-(*Oops*)
-by (blast_tac (claset() addSDs [unique_session_keys]) 4);
-(*OR4*)
-by (Blast_tac 3);
-(*OR3*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-Goal "[| Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs; \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (ftac Says_Server_message_form 1 THEN assume_tac 1);
-by (blast_tac (claset() addSEs [lemma]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(*A's guarantee. The Oops premise quantifies over NB because A cannot know
- what it is.*)
-Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
-\ \\<in> set evs; \
-\ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
-qed "A_gets_good_key";
-
-
-(**** Authenticity properties relating to NB ****)
-
-(*If the encrypted message appears then it originated with the Server!*)
-Goal "[| B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \\<in> parts (knows Spy evs) \
-\ --> (\\<exists>NA. Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-(*OR3*)
-by (Blast_tac 1);
-qed_spec_mp "NB_Crypt_imp_Server_msg";
-
-
-(*Guarantee for B: if it gets a well-formed certificate then the Server
- has sent the correct message in round 3.*)
-Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs; \
-\ B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> \\<exists>NA. Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
-qed "B_trusts_OR3";
-
-
-(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
-Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ \\<in> set evs; \
-\ ALL NA. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Key K \\<notin> 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 Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Apr 12 12:45:05 2001 +0200
@@ -5,7 +5,7 @@
Inductive relation "otway" for the Otway-Rees protocol.
-Simplified version with minimal encryption but explicit messages
+Abadi-Needham simplified version: minimal encryption, explicit messages
Note that the formalization does not even assume that nonces are fresh.
This is because the protocol does not rely on uniqueness of nonces for
@@ -17,61 +17,298 @@
IEEE Trans. SE 22 (1), 1996
*)
-OtwayRees_AN = Shared +
+theory OtwayRees_AN = Shared:
-consts otway :: event list set
+consts otway :: "event list set"
inductive "otway"
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[]: otway"
+ Nil: "[] \<in> otway"
(*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 \\<in> otway; X \\<in> synth (analz (knows Spy evs)) |]
- ==> Says Spy B X # evs \\<in> otway"
+ Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> otway"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> otway; Says A B X \\<in>set evsr |]
- ==> Gets B X # evsr \\<in> otway"
+ Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |]
+ ==> Gets B X # evsr \<in> otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1 \\<in> otway |]
- ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \\<in> otway"
+ OR1: "evs1 \<in> otway
+ ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 \<in> otway"
(*Bob's response to Alice's message.*)
- OR2 "[| evs2 \\<in> otway;
- Gets B {|Agent A, Agent B, Nonce NA|} \\<in>set evs2 |]
+ OR2: "[| evs2 \<in> otway;
+ Gets B {|Agent A, Agent B, Nonce NA|} \<in>set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- # evs2 \\<in> otway"
+ # evs2 \<in> 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 \\<in> otway; Key KAB \\<notin> used evs3;
+ OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
- \\<in>set evs3 |]
- ==> Says Server B
+ \<in>set evs3 |]
+ ==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
- # evs3 \\<in> otway"
+ # evs3 \<in> otway"
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
- Need B \\<noteq> Server because we allow messages to self.*)
- OR4 "[| evs4 \\<in> otway; B \\<noteq> Server;
- Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \\<in>set evs4;
+ Need B \<noteq> Server because we allow messages to self.*)
+ OR4: "[| evs4 \<in> otway; B \<noteq> Server;
+ Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \<in>set evs4;
Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
- \\<in>set evs4 |]
- ==> Says B A X # evs4 \\<in> otway"
+ \<in>set evs4 |]
+ ==> Says B A X # evs4 \<in> otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. B is not assumed to know shrK A.*)
- Oops "[| evso \\<in> otway;
- Says Server B
- {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
+ Oops: "[| evso \<in> otway;
+ Says Server B
+ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
- \\<in>set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> otway"
+ \<in>set evso |]
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "B \<noteq> Server
+ ==> \<exists>K. \<exists>evs \<in> otway.
+ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|})
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] otway.Nil
+ [THEN otway.OR1, THEN otway.Reception,
+ THEN otway.OR2, THEN otway.Reception,
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply possibility
+done
+
+lemma Gets_imp_Says [dest!]:
+ "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
+by (erule rev_mp, erule otway.induct, auto)
+
+
+(**** Inductive proofs about otway ****)
+
+(** For reasoning about the encrypted portion of messages **)
+
+lemma OR4_analz_knows_Spy:
+ "[| Gets B {|X, Crypt(shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule otway.induct, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+
+(*** Proofs involving analz ***)
+
+(*Describes the form of K and NA when the Server sends this message.*)
+lemma Says_Server_message_form:
+ "[| Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs;
+ evs \<in> otway |]
+ ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
+apply (erule rev_mp)
+apply (erule otway.induct)
+apply simp_all
+apply blast
+done
+
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*The equality makes the induction hypothesis easier to apply*)
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> otway ==>
+ \<forall>K KK. KK <= -(range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+done
+
+lemma analz_insert_freshK:
+ "[| evs \<in> otway; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}
+ \<in> set evs;
+ Says Server B'
+ {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},
+ Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}
+ \<in> set evs;
+ evs \<in> otway |]
+ ==> A=A' & B=B' & NA=NA' & NB=NB'"
+apply (erule rev_mp, erule rev_mp, erule otway.induct)
+apply simp_all
+(*Remaining cases: OR3 and OR4*)
+apply blast+
+done
+
+
+(**** Authenticity properties relating to NA ****)
+
+(*If the encrypted message appears then it originated with the Server!*)
+lemma NA_Crypt_imp_Server_msg [rule_format]:
+ "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+ --> (\<exists>NB. Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs)"
+apply (erule otway.induct, force)
+apply (simp_all add: ex_disj_distrib)
+(*Fake, OR3*)
+apply blast+;
+done
+
+
+(*Corollary: if A receives B's OR4 message then it originated with the Server.
+ Freshness may be inferred from nonce NA.*)
+lemma A_trusts_OR4:
+ "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
+ A \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> \<exists>NB. Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs"
+by (blast intro!: NA_Crypt_imp_Server_msg)
+
+
+(** 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 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs -->
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
+apply spy_analz (*Fake*)
+(*OR3, OR4, Oops*)
+apply (blast dest: unique_session_keys)+
+done
+
+
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs;
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: Says_Server_message_form secrecy_lemma)
+
+
+(*A's guarantee. The Oops premise quantifies over NB because A cannot know
+ what it is.*)
+lemma A_gets_good_key:
+ "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \<in> set evs;
+ \<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
+
+
+
+(**** Authenticity properties relating to NB ****)
+
+(*If the encrypted message appears then it originated with the Server!*)
+
+lemma NB_Crypt_imp_Server_msg [rule_format]:
+ "[| B \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} \<in> parts (knows Spy evs)
+ --> (\<exists>NA. Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs)"
+apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
+(*Fake, OR3*)
+apply blast+;
+done
+
+
+
+(*Guarantee for B: if it gets a well-formed certificate then the Server
+ has sent the correct message in round 3.*)
+lemma B_trusts_OR3:
+ "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs;
+ B \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> \<exists>NA. Says Server B
+ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
+ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs"
+by (blast intro!: NB_Crypt_imp_Server_msg)
+
+
+(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+lemma B_gets_good_key:
+ "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
+ \<in> set evs;
+ \<forall>NA. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)
end
--- a/src/HOL/Auth/OtwayRees_Bad.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,261 +0,0 @@
-(* Title: HOL/Auth/OtwayRees_Bad
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "otway" for the Otway-Rees protocol.
-
-The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-
-This file illustrates the consequences of such errors. We can still prove
-impressive-looking properties such as Spy_not_see_encrypted_key, yet the
-protocol is open to a middleperson attack. Attempting to prove some key lemmas
-indicates the possibility of this attack.
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "B \\<noteq> Server \
-\ ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway. \
-\ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
-\ \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-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 \\<in> set evs; evs \\<in> otway |] ==> \\<exists>A. Says A B X \\<in> 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 \\<in> set evs; evs \\<in> otway |] ==> X \\<in> 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 "[| Gets B {|N, Agent A, Agent B, X|} \\<in> set evs; evs \\<in> otway |] \
-\ ==> X \\<in> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
-qed "OR2_analz_knows_Spy";
-
-Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} \\<in> set evs; evs \\<in> otway |] \
-\ ==> X \\<in> 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|}|} \\<in> set evs \
-\ ==> K \\<in> parts (knows Spy evs)";
-by (Blast_tac 1);
-qed "Oops_parts_knows_Spy";
-
-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 \\<notin> parts (knows Spy evs).*)
-fun parts_induct_tac i =
- etac otway.induct i THEN
- ftac Oops_parts_knows_Spy (i+7) THEN
- ftac OR4_parts_knows_Spy (i+6) THEN
- ftac OR2_parts_knows_Spy (i+4) THEN
- prove_simple_subgoals_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees a good agent's shared key!*)
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> otway ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*** Proofs involving analz ***)
-
-(*Describes the form of K and NA when the Server sends this message. Also
- for Oops case.*)
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ evs \\<in> otway |] \
-\ ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)";
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Simp_tac);
-by (ALLGOALS Blast_tac);
-qed "Says_Server_message_form";
-
-
-(*For proofs involving analz.*)
-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
- ftac 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 \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-****)
-
-
-(** Session keys are not used to encrypt other session keys **)
-
-(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs \\<in> otway ==> \
-\ \\<forall>K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac otway.induct 1);
-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));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-
-Goal "[| evs \\<in> otway; KAB \\<notin> range shrK |] ==> \
-\ Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \\<in> set evs; \
-\ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \\<in> set evs; \
-\ evs \\<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac otway.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*Remaining cases: OR3 and OR4*)
-by (REPEAT (Blast_tac 1));
-qed "unique_session_keys";
-
-
-(** 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 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs --> \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac otway.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac (simpset() addcongs [conj_cong]
- addsimps [analz_insert_eq, analz_insert_freshK]
- @ pushes @ split_ifs)));
-(*Oops*)
-by (blast_tac (claset() addSDs [unique_session_keys]) 4);
-(*OR4*)
-by (Blast_tac 3);
-(*OR3*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-Goal "[| Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs; \
-\ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> otway |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (ftac Says_Server_message_form 1 THEN assume_tac 1);
-by (blast_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.
- The premise A \\<noteq> B prevents OR2's similar-looking cryptogram from being
- picked up. Original Otway-Rees doesn't need it.*)
-Goal "[| A \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \\<in> parts (knows Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \\<in> set evs";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed_spec_mp "Crypt_imp_OR1";
-
-
-(*Crucial property: If the encrypted message appears, and A has used NA
- to start a run, then it originated with the Server!
- The premise A \\<noteq> 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 \\<notin> bad; A \\<noteq> B; evs \\<in> otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} \\<in> parts (knows Spy evs) --> \
-\ Says A B {|NA, Agent A, Agent B, \
-\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
-\ \\<in> set evs --> \
-\ (\\<exists>B NB. Says Server B \
-\ {|NA, \
-\ Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} \\<in> set evs)";
-by (parts_induct_tac 1);
-(*Fake*)
-by (Blast_tac 1);
-(*OR1: it cannot be a new Nonce, contradiction.*)
-by (Blast_tac 1);
-(*OR3 and OR4*)
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
-by (ALLGOALS Clarify_tac);
-(*OR4*)
-by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
-(*OR3*) (** LEVEL 5 **)
-(*The hypotheses at this point suggest an attack in which nonce NB is used
- in two different roles:
- 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|}|}
- \\<in> set evs3;
- Says A B
- {|Nonce NB, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
- \\<in> set evs3;
-*)
-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 Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Apr 12 12:45:05 2001 +0200
@@ -8,75 +8,304 @@
The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
Burrows, Abadi and Needham. A Logic of Authentication.
Proc. Royal Soc. 426 (1989)
+
+This file illustrates the consequences of such errors. We can still prove
+impressive-looking properties such as Spy_not_see_encrypted_key, yet the
+protocol is open to a middleperson attack. Attempting to prove some key lemmas
+indicates the possibility of this attack.
*)
-OtwayRees_Bad = Shared +
-
-consts otway :: event list set
+theory OtwayRees_Bad = Shared:
-inductive otway
- intrs
+consts otway :: "event list set"
+inductive "otway"
+ intros
(*Initial trace is empty*)
- Nil "[] \\<in> otway"
+ Nil: "[] \<in> otway"
(*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 "[| evsf \\<in> otway; X \\<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \\<in> otway"
+ Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> otway"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> otway; Says A B X \\<in> set evsr |]
- ==> Gets B X # evsr \\<in> otway"
+ Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |]
+ ==> Gets B X # evsr \<in> otway"
(*Alice initiates a protocol run*)
- OR1 "[| evs1 \\<in> otway; Nonce NA \\<notin> used evs1 |]
- ==> Says A B {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
- # evs1 \\<in> otway"
+ OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
+ ==> Says A B {|Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
+ # evs1 \<in> otway"
- (*Bob's response to Alice's message.
+ (*Bob's response to Alice's message.
This variant of the protocol does NOT encrypt NB.*)
- OR2 "[| evs2 \\<in> otway; Nonce NB \\<notin> used evs2;
- Gets B {|Nonce NA, Agent A, Agent B, X|} \\<in> set evs2 |]
- ==> Says B Server
+ OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
+ Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
+ ==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- # evs2 \\<in> otway"
+ # evs2 \<in> otway"
(*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
forwarding to Alice.*)
- OR3 "[| evs3 \\<in> otway; Key KAB \\<notin> used evs3;
- Gets Server
- {|Nonce NA, Agent A, Agent B,
- Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
- Nonce NB,
+ OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
+ Gets Server
+ {|Nonce NA, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
+ Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- \\<in> set evs3 |]
- ==> Says Server B
- {|Nonce NA,
+ \<in> set evs3 |]
+ ==> Says Server B
+ {|Nonce NA,
Crypt (shrK A) {|Nonce NA, Key KAB|},
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
- # evs3 \\<in> otway"
+ # evs3 \<in> otway"
(*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 \\<in> otway; B ~= Server;
+ OR4: "[| evs4 \<in> otway; B ~= Server;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
- \\<in> set evs4;
+ \<in> set evs4;
Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- \\<in> set evs4 |]
- ==> Says B A {|Nonce NA, X|} # evs4 \\<in> otway"
+ \<in> set evs4 |]
+ ==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evso \\<in> otway;
+ Oops: "[| evso \<in> otway;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
- \\<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> otway"
+ \<in> set evso |]
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "B \<noteq> Server
+ ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway.
+ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
+ \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] otway.Nil
+ [THEN otway.OR1, THEN otway.Reception,
+ THEN otway.OR2, THEN otway.Reception,
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply possibility
+done
+
+lemma Gets_imp_Says [dest!]:
+ "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule otway.induct)
+apply auto
+done
+
+
+(**** Inductive proofs about otway ****)
+
+
+(** For reasoning about the encrypted portion of messages **)
+
+lemma OR2_analz_knows_Spy:
+ "[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemma OR4_analz_knows_Spy:
+ "[| Gets B {|N, X, Crypt (shrK B) X'|} \<in> set evs; evs \<in> otway |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemma Oops_parts_knows_Spy:
+ "Says Server B {|NA, X, Crypt K' {|NB,K|}|} \<in> set evs
+ ==> K \<in> parts (knows Spy evs)"
+by blast
+
+(*Forwarding lemma: see comments in OtwayRees.thy*)
+lemmas OR2_parts_knows_Spy =
+ OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+
+(*** Proofs involving analz ***)
+
+(*Describes the form of K and NA when the Server sends this message. Also
+ for Oops case.*)
+lemma Says_Server_message_form:
+ "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ evs \<in> otway |]
+ ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
+apply (erule rev_mp)
+apply (erule otway.induct, simp_all)
+apply blast
+done
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*The equality makes the induction hypothesis easier to apply*)
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> otway ==>
+ \<forall>K KK. KK <= -(range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply (drule_tac [4] OR2_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+done
+
+lemma analz_insert_freshK:
+ "[| evs \<in> otway; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
+ Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
+ evs \<in> otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule otway.induct, simp_all)
+(*Remaining cases: OR3 and OR4*)
+apply blast+
+done
+
+
+(** 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 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs -->
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule otway.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (drule_tac [6] OR4_analz_knows_Spy)
+apply (drule_tac [4] OR2_analz_knows_Spy)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
+apply spy_analz (*Fake*)
+(*OR3, OR4, Oops*)
+apply (blast dest: unique_session_keys)+
+done
+
+
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: Says_Server_message_form secrecy_lemma)
+
+
+(*** Attempting to prove stronger properties ***)
+
+(*Only OR1 can have caused such a part of a message to appear.
+ The premise A \<noteq> B prevents OR2's similar-looking cryptogram from being
+ picked up. Original Otway-Rees doesn't need it.*)
+lemma Crypt_imp_OR1 [rule_format]:
+ "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
+ Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+
+(*Crucial property: If the encrypted message appears, and A has used NA
+ to start a run, then it originated with the Server!
+ The premise A \<noteq> 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.*)
+lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
+ ==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
+ Says A B {|NA, Agent A, Agent B,
+ Crypt (shrK A) {|NA, Agent A, Agent B|}|}
+ \<in> set evs -->
+ (\<exists>B NB. Says Server B
+ {|NA,
+ Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
+apply (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy)
+apply simp_all
+(*Fake*)
+apply blast
+(*OR1: it cannot be a new Nonce, contradiction.*)
+apply blast
+(*OR3 and OR4*)
+apply (simp_all add: ex_disj_distrib)
+(*OR4*)
+prefer 2 apply (blast intro!: Crypt_imp_OR1)
+(*OR3*)
+apply clarify
+(*The hypotheses at this point suggest an attack in which nonce NB is used
+ in two different roles:
+ 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|}|}
+ \<in> set evs3
+ Says A B
+ {|Nonce NB, Agent A, Agent B,
+ Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
+ \<in> set evs3;
+*)
+
+
+(*Thus the key property A_can_trust probably fails too.*)
+oops
end
--- a/src/HOL/Auth/WooLam.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-(* Title: HOL/Auth/WooLam
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "woolam" for the Woo-Lam protocol.
-
-Simplified version from page 11 of
- Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
- IEEE Trans. S.E. 22(1), 1996, pages 6-15.
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "\\<exists>NB. \\<exists>evs \\<in> woolam. \
-\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS
- woolam.WL4 RS woolam.WL5) 2);
-by possibility_tac;
-result();
-
-
-(**** Inductive proofs about woolam ****)
-
-(** For reasoning about the encrypted portion of messages **)
-
-Goal "Says A' B X \\<in> set evs ==> X \\<in> analz (spies evs)";
-by (etac (Says_imp_spies RS analz.Inj) 1);
-qed "WL4_analz_spies";
-
-bind_thm ("WL4_parts_spies",
- WL4_analz_spies RS (impOfSubs analz_subset_parts));
-
-(*For proving the easier theorems about X \\<notin> parts (spies evs) *)
-fun parts_induct_tac i =
- etac woolam.induct i THEN
- ftac WL4_parts_spies (i+5) THEN
- prove_simple_subgoals_tac 1;
-
-
-(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs \\<in> woolam ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> woolam ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)";
-by Auto_tac;
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(**** Autheticity properties for Woo-Lam ****)
-
-
-(*** WL4 ***)
-
-(*If the encrypted message appears then it originated with Alice*)
-Goal "[| Crypt (shrK A) (Nonce NB) \\<in> parts (spies evs); \
-\ A \\<notin> bad; evs \\<in> woolam |] \
-\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "NB_Crypt_imp_Alice_msg";
-
-(*Guarantee for Server: if it gets a message containing a certificate from
- Alice, then she originated that certificate. But we DO NOT know that B
- ever saw it: the Spy may have rerouted the message to the Server.*)
-Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; evs \\<in> woolam |] \
-\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs";
-by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1);
-qed "Server_trusts_WL4";
-
-AddDs [Server_trusts_WL4];
-
-
-(*** WL5 ***)
-
-(*Server sent WL5 only if it received the right sort of message*)
-Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\<in> set evs; \
-\ evs \\<in> woolam |] \
-\ ==> \\<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Server_sent_WL5";
-
-AddDs [Server_sent_WL5];
-
-(*If the encrypted message appears then it originated with the Server!*)
-Goal "[| Crypt (shrK B) {|Agent A, NB|} \\<in> parts (spies evs); \
-\ B \\<notin> bad; evs \\<in> woolam |] \
-\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "NB_Crypt_imp_Server_msg";
-
-(*Guarantee for B. If B gets the Server's certificate then A has encrypted
- the nonce using her key. This event can be no older than the nonce itself.
- But A may have sent the nonce to some other agent and it could have reached
- the Server via the Spy.*)
-Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> woolam |] \
-\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs";
-by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1);
-qed "B_trusts_WL5";
-
-
-(*B only issues challenges in response to WL1. Not used.*)
-Goal "[| Says B A (Nonce NB) \\<in> set evs; B \\<noteq> Spy; evs \\<in> woolam |] \
-\ ==> \\<exists>A'. Says A' B (Agent A) \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "B_said_WL2";
-
-
-(**CANNOT be proved because A doesn't know where challenges come from...
-Goal "[| A \\<notin> bad; B \\<noteq> Spy; evs \\<in> woolam |] \
-\ ==> Crypt (shrK A) (Nonce NB) \\<in> parts (spies evs) & \
-\ Says B A (Nonce NB) \\<in> set evs \
-\ --> Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs";
-by (parts_induct_tac 1);
-by (Blast_tac 1);
-by Safe_tac;
-**)
--- a/src/HOL/Auth/WooLam.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/WooLam.thy Thu Apr 12 12:45:05 2001 +0200
@@ -14,52 +14,166 @@
Computer Security Foundations Workshop, 1996.
*)
-WooLam = Shared +
+theory WooLam = Shared:
-consts woolam :: event list set
+consts woolam :: "event list set"
inductive woolam
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[] \\<in> woolam"
+ Nil: "[] \<in> woolam"
(** These rules allow agents to send messages to themselves **)
(*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 "[| evsf \\<in> woolam; X \\<in> synth (analz (spies evsf)) |]
- ==> Says Spy B X # evsf \\<in> woolam"
+ Fake: "[| evsf \<in> woolam; X \<in> synth (analz (spies evsf)) |]
+ ==> Says Spy B X # evsf \<in> woolam"
(*Alice initiates a protocol run*)
- WL1 "[| evs1 \\<in> woolam |]
- ==> Says A B (Agent A) # evs1 \\<in> woolam"
+ WL1: "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
(*Bob responds to Alice's message with a challenge.*)
- WL2 "[| evs2 \\<in> woolam; Says A' B (Agent A) \\<in> set evs2 |]
- ==> Says B A (Nonce NB) # evs2 \\<in> woolam"
+ WL2: "[| evs2 \<in> woolam; Says A' B (Agent A) \<in> set evs2 |]
+ ==> Says B A (Nonce NB) # evs2 \<in> woolam"
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
her reply.*)
- WL3 "[| evs3 \\<in> woolam;
- Says A B (Agent A) \\<in> set evs3;
- Says B' A (Nonce NB) \\<in> set evs3 |]
- ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\<in> woolam"
+ WL3: "[| evs3 \<in> woolam;
+ Says A B (Agent A) \<in> set evs3;
+ Says B' A (Nonce NB) \<in> set evs3 |]
+ ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
(*Bob forwards Alice's response to the Server. NOTE: usually
the messages are shown in chronological order, for clarity.
But here, exchanging the two events would cause the lemma
WL4_analz_spies to pick up the wrong assumption!*)
- WL4 "[| evs4 \\<in> woolam;
- Says A' B X \\<in> set evs4;
- Says A'' B (Agent A) \\<in> set evs4 |]
- ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\<in> woolam"
+ WL4: "[| evs4 \<in> woolam;
+ Says A' B X \<in> set evs4;
+ Says A'' B (Agent A) \<in> set evs4 |]
+ ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
(*Server decrypts Alice's response for Bob.*)
- WL5 "[| evs5 \\<in> woolam;
+ WL5: "[| evs5 \<in> woolam;
Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
- \\<in> set evs5 |]
+ \<in> set evs5 |]
==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
- # evs5 \\<in> woolam"
+ # evs5 \<in> woolam"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare analz_into_parts [dest]
+declare Fake_parts_insert_in_Un [dest]
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "\<exists>NB. \<exists>evs \<in> woolam.
+ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] woolam.Nil
+ [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
+ THEN woolam.WL4, THEN woolam.WL5])
+apply possibility
+done
+
+(*Could prove forwarding lemmas for WL4, but we do not need them!*)
+
+(**** Inductive proofs about woolam ****)
+
+(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule woolam.induct, force, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> woolam|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+
+(**** Autheticity properties for Woo-Lam ****)
+
+(*** WL4 ***)
+
+(*If the encrypted message appears then it originated with Alice*)
+lemma NB_Crypt_imp_Alice_msg:
+ "[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> woolam |]
+ ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
+apply (erule rev_mp, erule woolam.induct, force, simp_all)
+apply blast+
+done
+
+(*Guarantee for Server: if it gets a message containing a certificate from
+ Alice, then she originated that certificate. But we DO NOT know that B
+ ever saw it: the Spy may have rerouted the message to the Server.*)
+lemma Server_trusts_WL4 [dest]:
+ "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
+ \<in> set evs;
+ A \<notin> bad; evs \<in> woolam |]
+ ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
+by (blast intro!: NB_Crypt_imp_Alice_msg)
+
+
+(*** WL5 ***)
+
+(*Server sent WL5 only if it received the right sort of message*)
+lemma Server_sent_WL5 [dest]:
+ "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs;
+ evs \<in> woolam |]
+ ==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
+ \<in> set evs"
+apply (erule rev_mp, erule woolam.induct, force, simp_all)
+apply blast+
+done
+
+(*If the encrypted message appears then it originated with the Server!*)
+lemma NB_Crypt_imp_Server_msg [rule_format]:
+ "[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
+ B \<notin> bad; evs \<in> woolam |]
+ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
+apply (erule rev_mp, erule woolam.induct, force, simp_all)
+apply blast+
+done
+
+(*Guarantee for B. If B gets the Server's certificate then A has encrypted
+ the nonce using her key. This event can be no older than the nonce itself.
+ But A may have sent the nonce to some other agent and it could have reached
+ the Server via the Spy.*)
+lemma B_trusts_WL5:
+ "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> woolam |]
+ ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
+by (blast dest!: NB_Crypt_imp_Server_msg)
+
+
+(*B only issues challenges in response to WL1. Not used.*)
+lemma B_said_WL2:
+ "[| Says B A (Nonce NB) \<in> set evs; B \<noteq> Spy; evs \<in> woolam |]
+ ==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
+apply (erule rev_mp, erule woolam.induct, force, simp_all)
+apply blast+
+done
+
+
+(**CANNOT be proved because A doesn't know where challenges come from...*)
+lemma "[| A \<notin> bad; B \<noteq> Spy; evs \<in> woolam |]
+ ==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
+ Says B A (Nonce NB) \<in> set evs
+ --> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
+apply (erule rev_mp, erule woolam.induct, force, simp_all)
+apply blast
+apply auto
+oops
end
--- a/src/HOL/Auth/Yahalom.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,626 +0,0 @@
-(* Title: HOL/Auth/Yahalom
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "yahalom" for the Yahalom protocol.
-
-From page 257 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-Pretty.setdepth 25;
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "A \\<noteq> Server \
-\ ==> \\<exists>X NB K. \\<exists>evs \\<in> yahalom. \
-\ Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (yahalom.Nil RS
- yahalom.YM1 RS yahalom.Reception RS
- yahalom.YM2 RS yahalom.Reception RS
- yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
-by possibility_tac;
-result();
-
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> \\<exists>A. Says A B X \\<in> set evs";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed "Gets_imp_Says";
-
-(*Must be proved separately for each protocol*)
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> X \\<in> 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 yahalom ****)
-
-
-(** For reasoning about the encrypted portion of messages **)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-Goal "[| Gets A {|Crypt (shrK A) Y, X|} \\<in> set evs; evs \\<in> yahalom |] \
-\ ==> X \\<in> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
-qed "YM4_analz_knows_Spy";
-
-bind_thm ("YM4_parts_knows_Spy",
- YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-
-(*For Oops*)
-Goal "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \\<in> set evs \
-\ ==> K \\<in> parts (knows Spy evs)";
-by (blast_tac (claset() addSDs [parts.Body,
- Says_imp_knows_Spy RS parts.Inj]) 1);
-qed "YM4_Key_parts_knows_Spy";
-
-(*For proving the easier theorems about X \\<notin> parts (knows Spy evs).*)
-fun parts_knows_Spy_tac i =
- EVERY
- [ftac YM4_Key_parts_knows_Spy (i+7),
- ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
- prove_simple_subgoals_tac i];
-
-(*Induction for regularity theorems. If induction formula has the form
- X \\<notin> analz (knows Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (knows Spy evs)) *)
-fun parts_induct_tac i =
- etac yahalom.induct i
- THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN parts_knows_Spy_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-Goal "evs \\<in> yahalom ==> \
-\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (knows Spy evs))";
-by (parts_induct_tac 1);
-(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*YM2-4: Because Key K is not fresh, etc.*)
-by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
-qed_spec_mp "new_keys_not_used";
-Addsimps [new_keys_not_used];
-
-(*Earlier, all protocol proofs declared this theorem.
- But few of them actually need it! (Another is Kerberos IV) *)
-bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
-
-
-(*Describes the form of K when the Server sends this message. Useful for
- Oops as well as main secrecy property.*)
-Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\ \\<in> set evs; evs \\<in> yahalom |] \
-\ ==> K \\<notin> range shrK";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "Says_Server_not_range";
-
-Addsimps [Says_Server_not_range];
-
-
-(*For proofs involving analz.*)
-val analz_knows_Spy_tac =
- ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;
-
-(****
- The following is to prove theorems of the form
-
- Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-****)
-
-(** Session keys are not used to encrypt other session keys **)
-
-Goal "evs \\<in> yahalom ==> \
-\ \\<forall>K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac yahalom.induct 1);
-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 addsimps [Says_Server_not_range])));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-Goal "[| evs \\<in> yahalom; KAB \\<notin> range shrK |] \
-\ ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \\<in> set evs; \
-\ Says Server A' \
-\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \\<in> set evs; \
-\ evs \\<in> yahalom |] \
-\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*YM4*)
-by (Blast_tac 2);
-(*YM3, by freshness*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-qed "unique_session_keys";
-
-
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs --> \
-\ Notes Spy {|na, nb, Key K|} \\<notin> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac yahalom.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps split_ifs @ pushes @
- [analz_insert_eq, analz_insert_freshK])));
-(*Oops*)
-by (blast_tac (claset() addDs [unique_session_keys]) 3);
-(*YM3*)
-by (blast_tac (claset() delrules [impCE]
- addSEs knows_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-
-(*Final version*)
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs; \
-\ Notes Spy {|na, nb, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSEs [lemma]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(** Security Guarantee for A upon receiving YM3 **)
-
-(*If the encrypted message appears then it originated with the Server*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\<in> parts (knows Spy evs); \
-\ A \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-qed "A_trusts_YM3";
-
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\<in> parts (knows Spy evs); \
-\ Notes Spy {|na, nb, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
-qed "A_gets_good_key";
-
-(** Security Guarantees for B upon receiving YM4 **)
-
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B. But this part says nothing about nonces.*)
-Goal "[| Crypt (shrK B) {|Agent A, Key K|} \\<in> parts (knows Spy evs); \
-\ B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>NA NB. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-(*YM3*)
-by (Blast_tac 1);
-qed "B_trusts_YM4_shrK";
-
-(*B knows, by the second part of A's message, that the Server distributed
- the key quoting nonce NB. This part says nothing about agent names.
- Secrecy of NB is crucial. Note that Nonce NB \\<notin> analz(knows Spy evs) must
- be the FIRST antecedent of the induction formula.*)
-Goal "evs \\<in> yahalom \
-\ ==> Nonce NB \\<notin> analz (knows Spy evs) --> \
-\ Crypt K (Nonce NB) \\<in> parts (knows Spy evs) --> \
-\ (\\<exists>A B NA. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-(*YM3 & Fake*)
-by (Blast_tac 2);
-by (Fake_parts_insert_tac 1);
-(*YM4*)
-(*A is uncompromised because NB is secure;
- A's certificate guarantees the existence of the Server message*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad]
- addDs [Says_imp_spies, analz.Inj,
- parts.Inj RS parts.Fst RS A_trusts_YM3]) 1);
-bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
-
-
-(**** Towards proving secrecy of Nonce NB ****)
-
-(** Lemmas about the predicate KeyWithNonce **)
-
-Goalw [KeyWithNonce_def]
- "Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
-\ \\<in> set evs ==> KeyWithNonce K NB evs";
-by (Blast_tac 1);
-qed "KeyWithNonceI";
-
-Goalw [KeyWithNonce_def]
- "KeyWithNonce K NB (Says S A X # evs) = \
-\ (Server = S & \
-\ (\\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
-\ | KeyWithNonce K NB evs)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "KeyWithNonce_Says";
-Addsimps [KeyWithNonce_Says];
-
-Goalw [KeyWithNonce_def]
- "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
-by (Simp_tac 1);
-qed "KeyWithNonce_Notes";
-Addsimps [KeyWithNonce_Notes];
-
-Goalw [KeyWithNonce_def]
- "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs";
-by (Simp_tac 1);
-qed "KeyWithNonce_Gets";
-Addsimps [KeyWithNonce_Gets];
-
-(*A fresh key cannot be associated with any nonce
- (with respect to a given trace). *)
-Goalw [KeyWithNonce_def]
- "Key K \\<notin> used evs ==> ~ KeyWithNonce K NB evs";
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-qed "fresh_not_KeyWithNonce";
-
-(*The Server message associates K with NB' and therefore not with any
- other nonce NB.*)
-Goalw [KeyWithNonce_def]
- "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
-\ \\<in> set evs; \
-\ NB \\<noteq> NB'; evs \\<in> yahalom |] \
-\ ==> ~ KeyWithNonce K NB evs";
-by (blast_tac (claset() addDs [unique_session_keys]) 1);
-qed "Says_Server_KeyWithNonce";
-
-
-(*The only nonces that can be found with the help of session keys are
- those distributed as nonce NB by the Server. The form of the theorem
- recalls analz_image_freshK, but it is much more complicated.*)
-
-
-(*As with analz_image_freshK, we take some pains to express the property
- as a logical equivalence so that the simplifier can apply it.*)
-Goal "P --> (X \\<in> analz (G Un H)) --> (X \\<in> analz H) ==> \
-\ P --> (X \\<in> analz (G Un H)) = (X \\<in> analz H)";
-by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
-val Nonce_secrecy_lemma = result();
-
-Goal "evs \\<in> yahalom ==> \
-\ (\\<forall>KK. KK <= - (range shrK) --> \
-\ (\\<forall>K \\<in> KK. ~ KeyWithNonce K NB evs) --> \
-\ (Nonce NB \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (Nonce NB \\<in> analz (knows Spy evs)))";
-by (etac yahalom.induct 1);
-by analz_knows_Spy_tac;
-by (REPEAT_FIRST (resolve_tac [impI RS allI]));
-by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
-(*For Oops, simplification proves NBa\\<noteq>NB. By Says_Server_KeyWithNonce,
- we get (~ KeyWithNonce K NB evs); then simplification can apply the
- induction hypothesis with KK = {K}.*)
-by (ALLGOALS (*4 seconds*)
- (asm_simp_tac
- (analz_image_freshK_ss
- addsimps split_ifs
- addsimps [all_conj_distrib, ball_conj_distrib, analz_image_freshK,
- KeyWithNonce_Says, KeyWithNonce_Notes, KeyWithNonce_Gets,
- fresh_not_KeyWithNonce, Says_Server_not_range,
- imp_disj_not1, (*Moves NBa\\<noteq>NB to the front*)
- Says_Server_KeyWithNonce])));
-(*Fake*)
-by (spy_analz_tac 1);
-(*YM4*) (** LEVEL 6 **)
-by (thin_tac "\\<forall>KK. ?P KK" 1);
-by (Clarify_tac 1);
-(*If A:bad then NBa is known, therefore NBa \\<noteq> NB. Previous two steps make
- the next step faster.*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_spies,
- Crypt_Spy_analz_bad]
- addDs [analz.Inj,
- parts.Inj RS parts.Fst RS A_trusts_YM3 RS KeyWithNonceI]) 1);
-qed_spec_mp "Nonce_secrecy";
-
-
-(*Version required below: if NB can be decrypted using a session key then it
- was distributed with that key. The more general form above is required
- for the induction to carry through.*)
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} \
-\ \\<in> set evs; \
-\ NB \\<noteq> NB'; KAB \\<notin> range shrK; evs \\<in> yahalom |] \
-\ ==> (Nonce NB \\<in> analz (insert (Key KAB) (knows Spy evs))) = \
-\ (Nonce NB \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps
- [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
-qed "single_Nonce_secrecy";
-
-
-(*** The Nonce NB uniquely identifies B's message. ***)
-
-Goal "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \\<in> parts (knows Spy evs); \
-\ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \\<in> parts (knows Spy evs); \
-\ evs \\<in> yahalom; B \\<notin> bad; B' \\<notin> bad |] \
-\ ==> NA' = NA & A' = A & B' = B";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-(*YM2, by freshness*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-qed "unique_NB";
-
-
-(*Variant useful for proving secrecy of NB. Because nb is assumed to be
- secret, we no longer must assume B, B' not bad.*)
-Goal "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ \\<in> set evs; \
-\ Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
-\ \\<in> set evs; \
-\ nb \\<notin> analz (knows Spy evs); evs \\<in> yahalom |] \
-\ ==> NA' = NA & A' = A & B' = B";
-by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad]
- addDs [Says_imp_spies, unique_NB, parts.Inj,
- analz.Inj]) 1);
-qed "Says_unique_NB";
-
-
-(** A nonce value is never used both as NA and as NB **)
-
-Goal "evs \\<in> yahalom \
-\ ==> Nonce NB \\<notin> analz (knows Spy evs) --> \
-\ Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \\<in> parts(knows Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, na, Nonce NB|} \\<notin> parts(knows Spy evs)";
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (blast_tac (claset() addDs [Gets_imp_knows_Spy RS analz.Inj]
- addSIs [parts_insertI]
- addSDs [parts.Body]) 1);
-bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
-
-(*more readable version cited in Yahalom paper*)
-standard (result() RS mp RSN (2,rev_mp));
-
-(*The Server sends YM3 only in response to YM2.*)
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \\<in> set evs; \
-\ evs \\<in> yahalom |] \
-\ ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed "Says_Server_imp_YM2";
-
-
-(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> (\\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \\<notin> set evs) --> \
-\ Says B Server \
-\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ \\<in> set evs --> \
-\ Nonce NB \\<notin> analz (knows Spy evs)";
-by (etac yahalom.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps split_ifs @ pushes @
- [new_keys_not_analzd, analz_insert_eq, analz_insert_freshK])));
-(*Prove YM3 by showing that no NB can also be an NA*)
-by (blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj]
- addSEs [no_nonce_YM1_YM2, MPair_parts]
- addDs [Gets_imp_Says, Says_unique_NB]) 4);
-(*YM2: similar freshness reasoning*)
-by (blast_tac (claset() addSDs [parts.Body]
- addDs [Gets_imp_Says,
- Says_imp_knows_Spy RS analz.Inj,
- impOfSubs analz_subset_parts]) 3);
-(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
-by (blast_tac (claset() addSIs [parts_insertI]
- addSEs knows_Spy_partsEs) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(** LEVEL 7: YM4 and Oops remain **)
-by (ALLGOALS (Clarify_tac THEN'
- full_simp_tac (simpset() addsimps [all_conj_distrib])));
-(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*)
-(*Case analysis on Aa:bad; PROOF FAILED problems;
- use Says_unique_NB to identify message components: Aa=A, Ba=B*)
-by (blast_tac (claset() addSDs [Says_unique_NB,
- parts.Inj RS parts.Fst RS A_trusts_YM3]
- addDs [Gets_imp_knows_Spy RS analz.Inj, Gets_imp_Says,
- Says_imp_spies, Says_Server_imp_YM2,
- Spy_not_see_encrypted_key]) 1);
-(** LEVEL 9 **)
-(*Oops case: if the nonce is betrayed now, show that the Oops event is
- covered by the quantified Oops assumption.*)
-by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1);
-by (case_tac "NB = NBa" 1);
-(*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (claset() addDs [Says_unique_NB]) 1);
-(*case NB \\<noteq> NBa*)
-by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
-by (blast_tac (claset() addSEs [no_nonce_YM1_YM2] (*to prove NB\\<noteq>NAa*)
- addDs [Says_imp_knows_Spy RS parts.Inj]) 1);
-bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
-
-
-(*B's session key guarantee from YM4. The two certificates contribute to a
- single conclusion about the Server's message. Note that the "Notes Spy"
- assumption must quantify over \\<forall>POSSIBLE keys instead of our particular K.
- If this run is broken and the spy substitutes a certificate containing an
- old key, B has no means of telling.*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ \\<in> set evs; \
-\ \\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addDs [Spy_not_see_NB, Says_unique_NB,
- Says_Server_imp_YM2, B_trusts_YM4_newK]) 1);
-qed "B_trusts_YM4";
-
-
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ \\<in> set evs; \
-\ \\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
-qed "B_gets_good_key";
-
-
-(*** Authenticating B to A ***)
-
-(*The encryption in message YM2 tells us it cannot be faked.*)
-Goal "evs \\<in> yahalom \
-\ ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} \\<in> parts (knows Spy evs) --> \
-\ B \\<notin> bad --> \
-\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ \\<in> set evs";
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
-
-(*If the server sends YM3 then B sent YM2*)
-Goal "evs \\<in> yahalom \
-\ ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ \\<in> set evs --> \
-\ B \\<notin> bad --> \
-\ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ \\<in> set evs";
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*YM4*)
-by (Blast_tac 2);
-(*YM3*)
-by (blast_tac (claset() addSDs [B_Said_YM2,
- Says_imp_knows_Spy RS parts.Inj]) 1);
-val lemma = result() RSN (2, rev_mp) RS mp |> standard;
-
-(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
-Goal "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]
- addEs knows_Spy_partsEs) 1);
-qed "YM3_auth_B_to_A";
-
-
-(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-
-(*Assuming the session key is secure, if both certificates are present then
- A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness.*)
-Goal "evs \\<in> yahalom \
-\ ==> Key K \\<notin> analz (knows Spy evs) --> \
-\ Crypt K (Nonce NB) \\<in> parts (knows Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Key K|} \\<in> parts (knows Spy evs) --> \
-\ B \\<notin> bad --> \
-\ (\\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs)";
-by (parts_induct_tac 1);
-(*Fake*)
-by (Fake_parts_insert_tac 1);
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1);
-(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
-by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-(*yes: apply unicity of session keys*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK,
- Crypt_Spy_analz_bad]
- addDs [Says_imp_knows_Spy RS parts.Inj,
- Says_imp_spies RS analz.Inj, unique_session_keys]) 1);
-qed_spec_mp "A_Said_YM3_lemma";
-
-(*If B receives YM4 then A has used nonce NB (and therefore is alive).
- Moreover, A associates K with NB (thus is talking about the same run).
- Other premises guarantee secrecy of K.*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\ \\<in> set evs; \
-\ (\\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \\<notin> set evs); \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (blast_tac (claset() addSIs [A_Said_YM3_lemma]
- addDs [Spy_not_see_encrypted_key, B_trusts_YM4,
- Gets_imp_Says, Says_imp_knows_Spy RS parts.Inj]) 1);
-qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/Yahalom.thy Thu Apr 12 12:45:05 2001 +0200
@@ -8,73 +8,633 @@
From page 257 of
Burrows, Abadi and Needham. A Logic of Authentication.
Proc. Royal Soc. 426 (1989)
+
+This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
*)
-Yahalom = Shared +
+theory Yahalom = Shared:
-consts yahalom :: event list set
+consts yahalom :: "event list set"
inductive "yahalom"
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[] \\<in> yahalom"
+ Nil: "[] \<in> yahalom"
(*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 "[| evsf \\<in> yahalom; X \\<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \\<in> yahalom"
+ Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> yahalom"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> yahalom; Says A B X \\<in> set evsr |]
- ==> Gets B X # evsr \\<in> yahalom"
+ Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs1 \\<in> yahalom; Nonce NA \\<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom"
+ YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
- YM2 "[| evs2 \\<in> yahalom; Nonce NB \\<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |]
+ YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
+ Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
==> Says B Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- # evs2 \\<in> yahalom"
+ # evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs3 \\<in> yahalom; Key KAB \\<notin> used evs3;
+ YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
Gets Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- \\<in> set evs3 |]
+ \<in> set evs3 |]
==> Says Server A
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
Crypt (shrK B) {|Agent A, Key KAB|}|}
- # evs3 \\<in> yahalom"
+ # evs3 \<in> yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
- A \\<noteq> Server is needed to prove Says_Server_not_range.*)
- YM4 "[| evs4 \\<in> yahalom; A \\<noteq> Server;
+ A \<noteq> Server is needed to prove Says_Server_not_range.*)
+ YM4: "[| evs4 \<in> yahalom; A \<noteq> Server;
Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
- \\<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom"
+ \<in> set evs4;
+ Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
- Oops "[| evso \\<in> yahalom;
+ Oops: "[| evso \<in> yahalom;
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
- X|} \\<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> yahalom"
+ X|} \<in> set evso |]
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
constdefs
- KeyWithNonce :: [key, nat, event list] => bool
+ KeyWithNonce :: "[key, nat, event list] => bool"
"KeyWithNonce K NB evs ==
- \\<exists>A B na X.
+ \<exists>A B na X.
Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
- \\<in> set evs"
+ \<in> set evs"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare Fake_parts_insert_in_Un [dest]
+declare analz_into_parts [dest]
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "A \<noteq> Server
+ ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
+ Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] yahalom.Nil
+ [THEN yahalom.YM1, THEN yahalom.Reception,
+ THEN yahalom.YM2, THEN yahalom.Reception,
+ THEN yahalom.YM3, THEN yahalom.Reception,
+ THEN yahalom.YM4])
+apply possibility
+done
+
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
+by (erule rev_mp, erule yahalom.induct, auto)
+
+(*Must be proved separately for each protocol*)
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
+
+
+(**** Inductive proofs about yahalom ****)
+
+(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+lemma YM4_analz_knows_Spy:
+ "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemmas YM4_parts_knows_Spy =
+ YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+
+(*For Oops*)
+lemma YM4_Key_parts_knows_Spy:
+ "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
+ ==> K \<in> parts (knows Spy evs)"
+by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
+lemma new_keys_not_used [rule_format, simp]:
+ "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3, YM4*)
+apply (blast dest!: keysFor_parts_insert)+
+done
+
+
+(*Earlier, all protocol proofs declared this theorem.
+ But only a few proofs need it, e.g. Yahalom and Kerberos IV.*)
+lemma new_keys_not_analzd:
+ "[|evs \<in> yahalom; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (knows Spy evs))"
+by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
+
+
+(*Describes the form of K when the Server sends this message. Useful for
+ Oops as well as main secrecy property.*)
+lemma Says_Server_not_range [simp]:
+ "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
+ \<in> set evs; evs \<in> yahalom |]
+ ==> K \<notin> range shrK"
+apply (erule rev_mp, erule yahalom.induct, simp_all)
+apply blast
+done
+
+
+(*For proofs involving analz.
+val analz_knows_Spy_tac =
+ ftac YM4_analz_knows_Spy 7 THEN assume_tac 7
+*)
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+(** Session keys are not used to encrypt other session keys **)
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> yahalom ==>
+ \<forall>K KK. KK <= - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+done
+
+lemma analz_insert_freshK:
+ "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+ Says Server A'
+ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+ evs \<in> yahalom |]
+ ==> A=A' & B=B' & na=na' & nb=nb'"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, simp_all)
+(*YM3, by freshness, and YM4*)
+apply blast+
+done
+
+
+(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs -->
+ Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_analz_knows_Spy)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
+apply spy_analz (*Fake*)
+apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
+done
+
+(*Final version*)
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs;
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: secrecy_lemma)
+
+
+(** Security Guarantee for A upon receiving YM3 **)
+
+(*If the encrypted message appears then it originated with the Server*)
+lemma A_trusts_YM3:
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+lemma A_gets_good_key:
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
+
+(** Security Guarantees for B upon receiving YM4 **)
+
+(*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B. But this part says nothing about nonces.*)
+lemma B_trusts_YM4_shrK:
+ "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NA NB. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K,
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+(*B knows, by the second part of A's message, that the Server distributed
+ the key quoting nonce NB. This part says nothing about agent names.
+ Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must
+ be the FIRST antecedent of the induction formula.*)
+lemma B_trusts_YM4_newK[rule_format]:
+ "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
+ Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
+ ==> \<exists>A B NA. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake, YM3*)
+apply blast
+apply blast
+(*YM4*)
+(*A is uncompromised because NB is secure
+ A's certificate guarantees the existence of the Server message*)
+apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
+ dest: Says_imp_spies
+ parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
+done
+
+
+(**** Towards proving secrecy of Nonce NB ****)
+
+(** Lemmas about the predicate KeyWithNonce **)
+
+lemma KeyWithNonceI:
+ "Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
+ \<in> set evs ==> KeyWithNonce K NB evs"
+by (unfold KeyWithNonce_def, blast)
+
+lemma KeyWithNonce_Says [simp]:
+ "KeyWithNonce K NB (Says S A X # evs) =
+ (Server = S &
+ (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
+ | KeyWithNonce K NB evs)"
+by (simp add: KeyWithNonce_def, blast)
+
+
+lemma KeyWithNonce_Notes [simp]:
+ "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
+by (simp add: KeyWithNonce_def)
+
+lemma KeyWithNonce_Gets [simp]:
+ "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
+by (simp add: KeyWithNonce_def)
+
+(*A fresh key cannot be associated with any nonce
+ (with respect to a given trace). *)
+lemma fresh_not_KeyWithNonce:
+ "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
+by (unfold KeyWithNonce_def, blast)
+
+(*The Server message associates K with NB' and therefore not with any
+ other nonce NB.*)
+lemma Says_Server_KeyWithNonce:
+ "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
+ \<in> set evs;
+ NB \<noteq> NB'; evs \<in> yahalom |]
+ ==> ~ KeyWithNonce K NB evs"
+by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
+
+
+(*The only nonces that can be found with the help of session keys are
+ those distributed as nonce NB by the Server. The form of the theorem
+ recalls analz_image_freshK, but it is much more complicated.*)
+
+
+(*As with analz_image_freshK, we take some pains to express the property
+ as a logical equivalence so that the simplifier can apply it.*)
+lemma Nonce_secrecy_lemma:
+ "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H) ==>
+ P --> (X \<in> analz (G Un H)) = (X \<in> analz H)"
+by (blast intro: analz_mono [THEN subsetD])
+
+lemma Nonce_secrecy:
+ "evs \<in> yahalom ==>
+ (\<forall>KK. KK <= - (range shrK) -->
+ (\<forall>K \<in> KK. ~ KeyWithNonce K NB evs) -->
+ (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) =
+ (Nonce NB \<in> analz (knows Spy evs)))"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_analz_knows_Spy)
+apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
+apply (simp_all del: image_insert image_Un
+ add: analz_image_freshK_simps split_ifs
+ all_conj_distrib ball_conj_distrib
+ analz_image_freshK fresh_not_KeyWithNonce
+ imp_disj_not1 (*Moves NBa\<noteq>NB to the front*)
+ Says_Server_KeyWithNonce)
+(*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce,
+ we get (~ KeyWithNonce K NB evs); then simplification can apply the
+ induction hypothesis with KK = {K}.*)
+(*Fake*)
+apply spy_analz
+(*YM4*) (** LEVEL 6 **)
+apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl)
+apply clarify
+(*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps make
+ the next step faster.*)
+apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
+ dest: analz.Inj
+ parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
+done
+
+
+(*Version required below: if NB can be decrypted using a session key then it
+ was distributed with that key. The more general form above is required
+ for the induction to carry through.*)
+lemma single_Nonce_secrecy:
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
+ \<in> set evs;
+ NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |]
+ ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
+ (Nonce NB \<in> analz (knows Spy evs))"
+by (simp_all del: image_insert image_Un imp_disjL
+ add: analz_image_freshK_simps split_ifs
+ Nonce_secrecy Says_Server_KeyWithNonce);
+
+
+(*** The Nonce NB uniquely identifies B's message. ***)
+
+lemma unique_NB:
+ "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
+ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
+ evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |]
+ ==> NA' = NA & A' = A & B' = B"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, and YM2 by freshness*)
+apply blast+
+done
+
+
+(*Variant useful for proving secrecy of NB. Because nb is assumed to be
+ secret, we no longer must assume B, B' not bad.*)
+lemma Says_unique_NB:
+ "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ \<in> set evs;
+ Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
+ \<in> set evs;
+ nb \<notin> analz (knows Spy evs); evs \<in> yahalom |]
+ ==> NA' = NA & A' = A & B' = B"
+by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
+ dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
+
+
+(** A nonce value is never used both as NA and as NB **)
+
+lemma no_nonce_YM1_YM2:
+ "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
+ Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
+ ==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake, YM2*)
+apply blast+
+done
+
+(*The Server sends YM3 only in response to YM2.*)
+lemma Says_Server_imp_YM2:
+ "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
+ evs \<in> yahalom |]
+ ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
+ \<in> set evs"
+apply (erule rev_mp, erule yahalom.induct)
+apply auto
+done
+
+
+(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
+lemma Spy_not_see_NB :
+ "[| Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Nonce NB \<notin> analz (knows Spy evs)"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_analz_knows_Spy)
+apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
+ analz_insert_freshK)
+(*Fake*)
+apply spy_analz
+(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
+apply blast
+(*YM2*)
+apply blast
+(*Prove YM3 by showing that no NB can also be an NA*)
+apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
+(** LEVEL 7: YM4 and Oops remain **)
+apply (clarify, simp add: all_conj_distrib)
+(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*)
+(*Case analysis on Aa:bad; PROOF FAILED problems
+ use Says_unique_NB to identify message components: Aa=A, Ba=B*)
+apply (blast dest!: Says_unique_NB
+ parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
+ dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
+ Spy_not_see_encrypted_key)
+(*Oops case: if the nonce is betrayed now, show that the Oops event is
+ covered by the quantified Oops assumption.*)
+apply (clarify, simp add: all_conj_distrib)
+apply (frule Says_Server_imp_YM2, assumption)
+apply (case_tac "NB = NBa")
+(*If NB=NBa then all other components of the Oops message agree*)
+apply (blast dest: Says_unique_NB)
+(*case NB \<noteq> NBa*)
+apply (simp add: single_Nonce_secrecy)
+apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
+done
+
+
+(*B's session key guarantee from YM4. The two certificates contribute to a
+ single conclusion about the Server's message. Note that the "Notes Spy"
+ assumption must quantify over \<forall>POSSIBLE keys instead of our particular K.
+ If this run is broken and the spy substitutes a certificate containing an
+ old key, B has no means of telling.*)
+lemma B_trusts_YM4:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K,
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+by (blast dest: Spy_not_see_NB Says_unique_NB
+ Says_Server_imp_YM2 B_trusts_YM4_newK)
+
+
+
+(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+lemma B_gets_good_key:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
+
+
+(*** Authenticating B to A ***)
+
+(*The encryption in message YM2 tells us it cannot be faked.*)
+lemma B_Said_YM2 [rule_format]:
+ "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
+ evs \<in> yahalom|]
+ ==> B \<notin> bad -->
+ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ \<in> set evs"
+apply (erule rev_mp, erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake*)
+apply blast
+done
+
+(*If the server sends YM3 then B sent YM2*)
+lemma YM3_auth_B_to_A_lemma:
+ "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ \<in> set evs; evs \<in> yahalom|]
+ ==> B \<notin> bad -->
+ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ \<in> set evs"
+apply (erule rev_mp, erule yahalom.induct, simp_all)
+(*YM3, YM4*)
+apply (blast dest!: B_Said_YM2)+
+done
+
+(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
+lemma YM3_auth_B_to_A:
+ "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ \<in> set evs"
+by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
+
+
+(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
+
+(*Assuming the session key is secure, if both certificates are present then
+ A has said NB. We can't be sure about the rest of A's message, but only
+ NB matters for freshness.*)
+lemma A_Said_YM3_lemma [rule_format]:
+ "evs \<in> yahalom
+ ==> Key K \<notin> analz (knows Spy evs) -->
+ Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
+ Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+ B \<notin> bad -->
+ (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake*)
+apply blast
+(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+apply (force dest!: Crypt_imp_keysFor)
+(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
+apply (simp add: ex_disj_distrib)
+(*yes: apply unicity of session keys*)
+apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
+ Crypt_Spy_analz_bad
+ dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
+done
+
+(*If B receives YM4 then A has used nonce NB (and therefore is alive).
+ Moreover, A associates K with NB (thus is talking about the same run).
+ Other premises guarantee secrecy of K.*)
+lemma YM4_imp_A_Said_YM3 [rule_format]:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+by (blast intro!: A_Said_YM3_lemma
+ dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
end
--- a/src/HOL/Auth/Yahalom2.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,378 +0,0 @@
-(* Title: HOL/Auth/Yahalom2
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
-
-This version trades encryption of NB for additional explicitness in YM3.
-
-From page 259 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body];
-AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert];
-
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "\\<exists>X NB K. \\<exists>evs \\<in> yahalom. \
-\ Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (yahalom.Nil RS
- yahalom.YM1 RS yahalom.Reception RS
- yahalom.YM2 RS yahalom.Reception RS
- yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
-by possibility_tac;
-result();
-
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> \\<exists>A. Says A B X \\<in> set evs";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed "Gets_imp_Says";
-
-(*Must be proved separately for each protocol*)
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> X \\<in> 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 yahalom ****)
-
-(** For reasoning about the encrypted portion of messages **)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-Goal "[| Gets A {|NB, Crypt (shrK A) Y, X|} \\<in> set evs; evs \\<in> yahalom |] \
-\ ==> X \\<in> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
-qed "YM4_analz_knows_Spy";
-
-bind_thm ("YM4_parts_knows_Spy",
- YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-
-(*For Oops*)
-Goal "Says Server A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} \\<in> set evs \
-\ ==> K \\<in> parts (knows Spy evs)";
-by (blast_tac (claset() addSDs [parts.Body,
- Says_imp_knows_Spy RS parts.Inj]) 1);
-qed "YM4_Key_parts_knows_Spy";
-
-(*For proving the easier theorems about X \\<notin> parts (knows Spy evs).*)
-fun parts_knows_Spy_tac i =
- EVERY
- [ftac YM4_Key_parts_knows_Spy (i+7),
- ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
- prove_simple_subgoals_tac i];
-
-(*Induction for regularity theorems. If induction formula has the form
- X \\<notin> analz (knows Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (knows Spy evs)) *)
-fun parts_induct_tac i =
- etac yahalom.induct i
- THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN parts_knows_Spy_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by Auto_tac;
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-Goal "evs \\<in> yahalom ==> \
-\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (knows Spy evs))";
-by (parts_induct_tac 1);
-(*YM4: Key K is not fresh!*)
-by (Blast_tac 3);
-(*YM3*)
-by (blast_tac (claset() addss (simpset())) 2);
-(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-qed_spec_mp "new_keys_not_used";
-Addsimps [new_keys_not_used];
-
-(*Earlier, ALL protocol proofs declared this theorem.
- But Yahalom and Kerberos IV are the only ones that need it!*)
-bind_thm ("new_keys_not_analzd",
- [analz_subset_parts RS keysFor_mono,
- new_keys_not_used] MRS contra_subsetD);
-
-(*Describes the form of K when the Server sends this message. Useful for
- Oops as well as main secrecy property.*)
-Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
-\ \\<in> set evs; \
-\ evs \\<in> yahalom |] \
-\ ==> K \\<notin> range shrK";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Says_Server_message_form";
-
-
-(*For proofs involving analz.*)
-val analz_knows_Spy_tac =
- dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN
- ftac Says_Server_message_form 8 THEN
- assume_tac 8 THEN
- REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8);
-
-
-(****
- The following is to prove theorems of the form
-
- Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-
-****)
-
-(** Session keys are not used to encrypt other session keys **)
-
-Goal "evs \\<in> yahalom ==> \
-\ \\<forall>K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac yahalom.induct 1);
-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));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-Goal "[| evs \\<in> yahalom; KAB \\<notin> range shrK |] ==> \
-\ Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-Goal "[| Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \\<in> set evs; \
-\ Says Server A' \
-\ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \\<in> set evs; \
-\ evs \\<in> yahalom |] \
-\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*YM3, by freshness*)
-by (Blast_tac 1);
-qed "unique_session_keys";
-
-
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
-\ \\<in> set evs --> \
-\ Notes Spy {|na, nb, Key K|} \\<notin> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac yahalom.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps split_ifs
- addsimps [new_keys_not_analzd, analz_insert_eq,
- analz_insert_freshK])));
-(*Oops*)
-by (blast_tac (claset() addDs [unique_session_keys]) 3);
-(*YM3*)
-by (Blast_tac 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RS mp RSN(2,rev_notE);
-
-
-(*Final version*)
-Goal "[| Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
-\ \\<in> set evs; \
-\ Notes Spy {|na, nb, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSEs [lemma] addDs [Says_Server_message_form]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(** Security Guarantee for A upon receiving YM3 **)
-
-(*If the encrypted message appears then it originated with the Server.
- May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} \
-\ \\<in> parts (knows Spy evs); \
-\ A \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>nb. Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "A_trusts_YM3";
-
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na|} \\<in> parts (knows Spy evs); \
-\ \\<forall>nb. Notes Spy {|na, nb, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
-qed "A_gets_good_key";
-
-
-(** Security Guarantee for B upon receiving YM4 **)
-
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B, and has associated it with NB.*)
-Goal "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
-\ \\<in> parts (knows Spy evs); \
-\ B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>NA. Says Server A \
-\ {|Nonce NB, \
-\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "B_trusts_YM4_shrK";
-
-
-(*With this protocol variant, we don't need the 2nd part of YM4 at all:
- Nonce NB is available in the first part.*)
-
-(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
- because we do not have to show that NB is secret. *)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
-\ X|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>NA. Says Server A \
-\ {|Nonce NB, \
-\ Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1);
-qed "B_trusts_YM4";
-
-
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
-\ X|} \
-\ \\<in> set evs; \
-\ \\<forall>na. Notes Spy {|na, Nonce NB, Key K|} \\<notin> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
-qed "B_gets_good_key";
-
-
-
-(*** Authenticating B to A ***)
-
-(*The encryption in message YM2 tells us it cannot be faked.*)
-Goal "[| Crypt (shrK B) {|Agent A, Nonce NA|} \\<in> parts (knows Spy evs); \
-\ B \\<notin> bad; evs \\<in> yahalom \
-\ |] ==> \\<exists>NB. Says B Server {|Agent B, Nonce NB, \
-\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (ALLGOALS Blast_tac);
-qed "B_Said_YM2";
-
-
-(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
-Goal "[| Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ \\<in> set evs; \
-\ B \\<notin> bad; evs \\<in> yahalom \
-\ |] ==> \\<exists>nb'. Says B Server {|Agent B, nb', \
-\ Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*YM3*)
-by (blast_tac (claset() addSDs [B_Said_YM2]) 3);
-(*Fake, YM2*)
-by (ALLGOALS Blast_tac);
-val lemma = result();
-
-(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
-Goal "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\==> \\<exists>nb'. Says B Server \
-\ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addSDs [A_trusts_YM3, lemma]) 1);
-qed "YM3_auth_B_to_A";
-
-
-(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-
-(*Assuming the session key is secure, if both certificates are present then
- A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness. Note that Key K \\<notin> analz (knows Spy evs) must be
- the FIRST antecedent of the induction formula.*)
-Goal "evs \\<in> yahalom \
-\ ==> Key K \\<notin> analz (knows Spy evs) --> \
-\ Crypt K (Nonce NB) \\<in> parts (knows Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
-\ \\<in> parts (knows Spy evs) --> \
-\ B \\<notin> bad --> \
-\ (\\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs)";
-by (parts_induct_tac 1);
-(*Fake*)
-by (Blast_tac 1);
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
-by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-(*Yes: apply unicity of session keys. [Ind. hyp. no longer needed!]*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK,
- Crypt_Spy_analz_bad]
- addDs [Says_imp_spies RS analz.Inj, unique_session_keys]) 1);
-qed_spec_mp "Auth_A_to_B_lemma";
-
-
-(*If B receives YM4 then A has used nonce NB (and therefore is alive).
- Moreover, A associates K with NB (thus is talking about the same run).
- Other premises guarantee secrecy of K.*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ (\\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \\<notin> set evs); \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (blast_tac (claset() addIs [Auth_A_to_B_lemma]
- addDs [Spy_not_see_encrypted_key, B_trusts_YM4_shrK]) 1);
-qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom2.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Thu Apr 12 12:45:05 2001 +0200
@@ -13,64 +13,389 @@
Proc. Royal Soc. 426 (1989)
*)
-Yahalom2 = Shared +
+theory Yahalom2 = Shared:
-consts yahalom :: event list set
+consts yahalom :: "event list set"
inductive "yahalom"
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[] \\<in> yahalom"
+ Nil: "[] \<in> yahalom"
(*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 "[| evsf \\<in> yahalom; X \\<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \\<in> yahalom"
+ Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> yahalom"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> yahalom; Says A B X \\<in> set evsr |]
- ==> Gets B X # evsr \\<in> yahalom"
+ Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs1 \\<in> yahalom; Nonce NA \\<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom"
+ YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
- YM2 "[| evs2 \\<in> yahalom; Nonce NB \\<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |]
- ==> Says B Server
+ YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
+ Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+ ==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
- # evs2 \\<in> yahalom"
+ # evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a certificate for forwarding to Bob.
Both agents are quoted in the 2nd certificate to prevent attacks!*)
- YM3 "[| evs3 \\<in> yahalom; Key KAB \\<notin> used evs3;
+ YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
Gets Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
- \\<in> set evs3 |]
+ \<in> set evs3 |]
==> Says Server A
- {|Nonce NB,
+ {|Nonce NB,
Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
- # evs3 \\<in> yahalom"
+ # evs3 \<in> yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4 "[| evs4 \\<in> yahalom;
+ YM4: "[| evs4 \<in> yahalom;
Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} \\<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom"
+ X|} \<in> set evs4;
+ Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
- Oops "[| evso \\<in> yahalom;
- Says Server A {|Nonce NB,
+ Oops: "[| evso \<in> yahalom;
+ Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
- X|} \\<in> set evso |]
- ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \\<in> yahalom"
+ X|} \<in> set evso |]
+ ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare Fake_parts_insert_in_Un [dest]
+declare analz_into_parts [dest]
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
+ Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] yahalom.Nil
+ [THEN yahalom.YM1, THEN yahalom.Reception,
+ THEN yahalom.YM2, THEN yahalom.Reception,
+ THEN yahalom.YM3, THEN yahalom.Reception,
+ THEN yahalom.YM4])
+apply possibility
+done
+
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
+by (erule rev_mp, erule yahalom.induct, auto)
+
+(*Must be proved separately for each protocol*)
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
+
+
+(**** Inductive proofs about yahalom ****)
+
+(** For reasoning about the encrypted portion of messages **)
+
+(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+lemma YM4_analz_knows_Spy:
+ "[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemmas YM4_parts_knows_Spy =
+ YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
+lemma new_keys_not_used [rule_format, simp]:
+ "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3, YM4*)
+apply (blast dest!: keysFor_parts_insert)+
+done
+
+
+(*Describes the form of K when the Server sends this message. Useful for
+ Oops as well as main secrecy property.*)
+lemma Says_Server_message_form:
+ "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
+ \<in> set evs; evs \<in> yahalom |]
+ ==> K \<notin> range shrK"
+by (erule rev_mp, erule yahalom.induct, simp_all)
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+(** Session keys are not used to encrypt other session keys **)
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> yahalom ==>
+ \<forall>K KK. KK <= - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
+ drule_tac [6] YM4_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+done
+
+lemma analz_insert_freshK:
+ "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server A
+ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
+ Says Server A'
+ {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|} \<in> set evs;
+ evs \<in> yahalom |]
+ ==> A=A' & B=B' & na=na' & nb=nb'"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, simp_all)
+(*YM3, by freshness*)
+apply blast
+done
+
+
+(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<in> set evs -->
+ Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
+ drule_tac [6] YM4_analz_knows_Spy)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
+apply spy_analz (*Fake*)
+apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
+done
+
+
+(*Final version*)
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server A
+ {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<in> set evs;
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: secrecy_lemma Says_Server_message_form)
+
+
+(** Security Guarantee for A upon receiving YM3 **)
+
+(*If the encrypted message appears then it originated with the Server.
+ May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
+lemma A_trusts_YM3:
+ "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>nb. Says Server A
+ {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+lemma A_gets_good_key:
+ "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
+ \<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
+
+
+(** Security Guarantee for B upon receiving YM4 **)
+
+(*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B, and has associated it with NB.*)
+lemma B_trusts_YM4_shrK:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+ \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NA. Says Server A
+ {|Nonce NB,
+ Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+
+(*With this protocol variant, we don't need the 2nd part of YM4 at all:
+ Nonce NB is available in the first part.*)
+
+(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
+ because we do not have to show that NB is secret. *)
+lemma B_trusts_YM4:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NA. Says Server A
+ {|Nonce NB,
+ Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}|}
+ \<in> set evs"
+by (blast dest!: B_trusts_YM4_shrK)
+
+
+(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+lemma B_gets_good_key:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
+ \<in> set evs;
+ \<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
+
+
+(*** Authenticating B to A ***)
+
+(*The encryption in message YM2 tells us it cannot be faked.*)
+lemma B_Said_YM2:
+ "[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NB. Says B Server {|Agent B, Nonce NB,
+ Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM2*)
+apply blast+
+done
+
+
+(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
+lemma YM3_auth_B_to_A_lemma:
+ "[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+ \<in> set evs;
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>nb'. Says B Server {|Agent B, nb',
+ Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, simp_all)
+(*Fake, YM2, YM3*)
+apply (blast dest!: B_Said_YM2)+
+done
+
+(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
+lemma YM3_auth_B_to_A:
+ "[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>nb'. Says B Server
+ {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs"
+by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
+
+
+
+(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
+
+(*Assuming the session key is secure, if both certificates are present then
+ A has said NB. We can't be sure about the rest of A's message, but only
+ NB matters for freshness. Note that Key K \<notin> analz (knows Spy evs) must be
+ the FIRST antecedent of the induction formula.*)
+
+(*This lemma allows a use of unique_session_keys in the next proof,
+ which otherwise is extremely slow.*)
+lemma secure_unique_session_keys:
+ "[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
+ Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
+ Key K \<notin> analz (knows Spy evs); evs \<in> yahalom |]
+ ==> A=A' & B=B'"
+by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad)
+
+
+lemma Auth_A_to_B_lemma [rule_format]:
+ "evs \<in> yahalom
+ ==> Key K \<notin> analz (knows Spy evs) -->
+ Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
+ Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
+ \<in> parts (knows Spy evs) -->
+ B \<notin> bad -->
+ (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake*)
+apply blast
+(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+apply (force dest!: Crypt_imp_keysFor)
+(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity
+ of session keys; if not, use ind. hyp.*)
+apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
+done
+
+
+(*If B receives YM4 then A has used nonce NB (and therefore is alive).
+ Moreover, A associates K with NB (thus is talking about the same run).
+ Other premises guarantee secrecy of K.*)
+lemma YM4_imp_A_Said_YM3 [rule_format]:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ (\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+by (blast intro: Auth_A_to_B_lemma
+ dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
end
--- a/src/HOL/Auth/Yahalom_Bad.ML Wed Apr 11 11:53:54 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,329 +0,0 @@
-(* Title: HOL/Auth/Yahalom
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Inductive relation "yahalom" for the Yahalom protocol.
-
-From page 257 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
-
-(*A "possibility property": there are traces that reach the end*)
-Goal "A \\<noteq> Server \
-\ ==> \\<exists>X NB K. \\<exists>evs \\<in> yahalom. \
-\ Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (yahalom.Nil RS
- yahalom.YM1 RS yahalom.Reception RS
- yahalom.YM2 RS yahalom.Reception RS
- yahalom.YM3 RS yahalom.Reception RS yahalom.YM4) 2);
-by possibility_tac;
-result();
-
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> \\<exists>A. Says A B X \\<in> set evs";
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed "Gets_imp_Says";
-
-(*Must be proved separately for each protocol*)
-Goal "[| Gets B X \\<in> set evs; evs \\<in> yahalom |] ==> X \\<in> 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 yahalom ****)
-
-
-(** For reasoning about the encrypted portion of messages **)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
-Goal "[| Gets A {|Crypt (shrK A) Y, X|} \\<in> set evs; evs \\<in> yahalom |] \
-\ ==> X \\<in> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1);
-qed "YM4_analz_knows_Spy";
-
-bind_thm ("YM4_parts_knows_Spy",
- YM4_analz_knows_Spy RS (impOfSubs analz_subset_parts));
-
-(*For proving the easier theorems about X \\<notin> parts (knows Spy evs).*)
-fun parts_knows_Spy_tac i =
- EVERY
- [ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6),
- prove_simple_subgoals_tac i];
-
-(*Induction for regularity theorems. If induction formula has the form
- X \\<notin> analz (knows Spy evs) --> ... then it shortens the proof by discarding
- needless information about analz (insert X (knows Spy evs)) *)
-fun parts_induct_tac i =
- etac yahalom.induct i
- THEN
- REPEAT (FIRSTGOAL analz_mono_contra_tac)
- THEN parts_knows_Spy_tac i;
-
-
-(** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
-
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> parts (knows Spy evs)) = (A \\<in> bad)";
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (ALLGOALS Blast_tac);
-qed "Spy_see_shrK";
-Addsimps [Spy_see_shrK];
-
-Goal "evs \\<in> yahalom ==> (Key (shrK A) \\<in> analz (knows Spy evs)) = (A \\<in> bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
-qed "Spy_analz_shrK";
-Addsimps [Spy_analz_shrK];
-
-AddSDs [Spy_see_shrK RSN (2, rev_iffD1),
- Spy_analz_shrK RSN (2, rev_iffD1)];
-
-
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-Goal "evs \\<in> yahalom ==> \
-\ Key K \\<notin> used evs --> K \\<notin> keysFor (parts (knows Spy evs))";
-by (parts_induct_tac 1);
-(*Fake*)
-by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
-(*YM2-4: Because Key K is not fresh, etc.*)
-by (REPEAT (blast_tac (claset() addSEs knows_Spy_partsEs) 1));
-qed_spec_mp "new_keys_not_used";
-Addsimps [new_keys_not_used];
-
-
-(*For proofs involving analz.*)
-val analz_knows_Spy_tac =
- ftac YM4_analz_knows_Spy 7 THEN assume_tac 7;
-
-(****
- The following is to prove theorems of the form
-
- Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) ==>
- Key K \\<in> analz (knows Spy evs)
-
- A more general formula must be proved inductively.
-****)
-
-(** Session keys are not used to encrypt other session keys **)
-
-Goal "evs \\<in> yahalom ==> \
-\ \\<forall>K KK. KK <= - (range shrK) --> \
-\ (Key K \\<in> analz (Key`KK Un (knows Spy evs))) = \
-\ (K \\<in> KK | Key K \\<in> analz (knows Spy evs))";
-by (etac yahalom.induct 1);
-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));
-(*Fake*)
-by (spy_analz_tac 1);
-qed_spec_mp "analz_image_freshK";
-
-Goal "[| evs \\<in> yahalom; KAB \\<notin> range shrK |] \
-\ ==> Key K \\<in> analz (insert (Key KAB) (knows Spy evs)) = \
-\ (K = KAB | Key K \\<in> analz (knows Spy evs))";
-by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
-qed "analz_insert_freshK";
-
-
-(*** The Key K uniquely identifies the Server's message. **)
-
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \\<in> set evs; \
-\ Says Server A' \
-\ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \\<in> set evs; \
-\ evs \\<in> yahalom |] \
-\ ==> A=A' & B=B' & na=na' & nb=nb'";
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-(*YM4*)
-by (Blast_tac 2);
-(*YM3, by freshness*)
-by (blast_tac (claset() addSEs knows_Spy_partsEs) 1);
-qed "unique_session_keys";
-
-
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-
-Goal "[| A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs --> \
-\ Key K \\<notin> analz (knows Spy evs)";
-by (etac yahalom.induct 1);
-by analz_knows_Spy_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps split_ifs @ pushes @
- [analz_insert_eq, analz_insert_freshK])));
-(*YM3*)
-by (blast_tac (claset() delrules [impCE]
- addSEs knows_Spy_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-val lemma = result() RS mp RSN(2,rev_notE);
-
-
-(*Final version*)
-Goal "[| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSEs [lemma]) 1);
-qed "Spy_not_see_encrypted_key";
-
-
-(** Security Guarantee for A upon receiving YM3 **)
-
-(*If the encrypted message appears then it originated with the Server*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\<in> parts (knows Spy evs); \
-\ A \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-qed "A_trusts_YM3";
-
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
-Goal "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \\<in> parts (knows Spy evs); \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
-qed "A_gets_good_key";
-
-(** Security Guarantees for B upon receiving YM4 **)
-
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B. But this part says nothing about nonces.*)
-Goal "[| Crypt (shrK B) {|Agent A, Key K|} \\<in> parts (knows Spy evs); \
-\ B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>NA NB. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (etac rev_mp 1);
-by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-(*YM3*)
-by (Blast_tac 1);
-qed "B_trusts_YM4_shrK";
-
-(** Up to now, the reasoning is similar to standard Yahalom. Now the
- doubtful reasoning occurs. We should not be assuming that an unknown
- key is secure, but the model allows us to: there is no Oops rule to
- let session keys go.*)
-
-(*B knows, by the second part of A's message, that the Server distributed
- the key quoting nonce NB. This part says nothing about agent names.
- Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
- the secrecy of NB.*)
-Goal "evs \\<in> yahalom \
-\ ==> Key K \\<notin> analz (knows Spy evs) --> \
-\ Crypt K (Nonce NB) \\<in> parts (knows Spy evs) --> \
-\ (\\<exists>A B NA. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs)";
-by (parts_induct_tac 1);
-by (ALLGOALS Clarify_tac);
-(*YM3 & Fake*)
-by (Blast_tac 2);
-by (Fake_parts_insert_tac 1);
-(*YM4*)
-(*A is uncompromised because NB is secure;
- A's certificate guarantees the existence of the Server message*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, Crypt_Spy_analz_bad]
- addDs [Says_imp_spies, analz.Inj,
- parts.Inj RS parts.Fst RS A_trusts_YM3]) 1);
-bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
-
-
-(*B's session key guarantee from YM4. The two certificates contribute to a
- single conclusion about the Server's message. *)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>na nb. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ \\<in> set evs";
-by (blast_tac (claset() addDs [B_trusts_YM4_newK, B_trusts_YM4_shrK,
- Spy_not_see_encrypted_key, unique_session_keys]) 1);
-qed "B_trusts_YM4";
-
-
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> Key K \\<notin> analz (knows Spy evs)";
-by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
-qed "B_gets_good_key";
-
-
-(*** Authenticating B to A: these proofs are not considered.
- They are irrelevant to showing the need for Oops. ***)
-
-
-(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-
-(*Assuming the session key is secure, if both certificates are present then
- A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness.*)
-Goal "evs \\<in> yahalom \
-\ ==> Key K \\<notin> analz (knows Spy evs) --> \
-\ Crypt K (Nonce NB) \\<in> parts (knows Spy evs) --> \
-\ Crypt (shrK B) {|Agent A, Key K|} \\<in> parts (knows Spy evs) --> \
-\ B \\<notin> bad --> \
-\ (\\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs)";
-by (parts_induct_tac 1);
-(*Fake*)
-by (Fake_parts_insert_tac 1);
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1);
-(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
-by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-(*yes: apply unicity of session keys*)
-by (blast_tac (claset() addSDs [Gets_imp_Says, A_trusts_YM3, B_trusts_YM4_shrK,
- Crypt_Spy_analz_bad]
- addDs [Says_imp_knows_Spy RS parts.Inj,
- Says_imp_spies RS analz.Inj, unique_session_keys]) 1);
-qed_spec_mp "A_Said_YM3_lemma";
-
-(*If B receives YM4 then A has used nonce NB (and therefore is alive).
- Moreover, A associates K with NB (thus is talking about the same run).
- Other premises guarantee secrecy of K.*)
-Goal "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, \
-\ Crypt K (Nonce NB)|} \\<in> set evs; \
-\ Says B Server \
-\ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|} \
-\ \\<in> set evs; \
-\ A \\<notin> bad; B \\<notin> bad; evs \\<in> yahalom |] \
-\ ==> \\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \\<in> set evs";
-by (blast_tac (claset() addSIs [A_Said_YM3_lemma]
- addDs [Spy_not_see_encrypted_key, B_trusts_YM4,
- Gets_imp_Says, Says_imp_knows_Spy RS parts.Inj]) 1);
-qed_spec_mp "YM4_imp_A_Said_YM3";
--- a/src/HOL/Auth/Yahalom_Bad.thy Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Thu Apr 12 12:45:05 2001 +0200
@@ -5,62 +5,354 @@
Inductive relation "yahalom" for the Yahalom protocol.
-Example of why Oops is necessary. This protocol can be attacked because it
-doesn't keep NB secret, but without Oops it can be "verified" anyway.
+Demonstrates of why Oops is necessary. This protocol can be attacked because
+it doesn't keep NB secret, but without Oops it can be "verified" anyway.
+The issues are discussed in lcp's LICS 2000 invited lecture.
*)
-Yahalom_Bad = Shared +
+theory Yahalom_Bad = Shared:
-consts yahalom :: event list set
+consts yahalom :: "event list set"
inductive "yahalom"
- intrs
+ intros
(*Initial trace is empty*)
- Nil "[] : yahalom"
+ Nil: "[] \<in> yahalom"
(*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 "[| evsf \\<in> yahalom; X \\<in> synth (analz (knows Spy evsf)) |]
- ==> Says Spy B X # evsf \\<in> yahalom"
+ Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |]
+ ==> Says Spy B X # evsf \<in> yahalom"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception "[| evsr \\<in> yahalom; Says A B X \\<in> set evsr |]
- ==> Gets B X # evsr \\<in> yahalom"
+ Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |]
+ ==> Gets B X # evsr \<in> yahalom"
(*Alice initiates a protocol run*)
- YM1 "[| evs1 \\<in> yahalom; Nonce NA \\<notin> used evs1 |]
- ==> Says A B {|Agent A, Nonce NA|} # evs1 \\<in> yahalom"
+ YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
+ ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
- YM2 "[| evs2 \\<in> yahalom; Nonce NB \\<notin> used evs2;
- Gets B {|Agent A, Nonce NA|} \\<in> set evs2 |]
- ==> Says B Server
+ YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
+ Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
+ ==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
- # evs2 \\<in> yahalom"
+ # evs2 \<in> yahalom"
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs3 \\<in> yahalom; Key KAB \\<notin> used evs3;
- Gets Server
+ YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
+ Gets Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
- \\<in> set evs3 |]
+ \<in> set evs3 |]
==> Says Server A
{|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
Crypt (shrK B) {|Agent A, Key KAB|}|}
- # evs3 \\<in> yahalom"
+ # evs3 \<in> yahalom"
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
- A \\<noteq> Server is needed to prove Says_Server_not_range.*)
- YM4 "[| evs4 \\<in> yahalom; A \\<noteq> Server;
+ A \<noteq> Server is needed to prove Says_Server_not_range.*)
+ YM4: "[| evs4 \<in> yahalom; A \<noteq> Server;
Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
- \\<in> set evs4;
- Says A B {|Agent A, Nonce NA|} \\<in> set evs4 |]
- ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \\<in> yahalom"
+ \<in> set evs4;
+ Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
+ ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare parts.Body [dest]
+declare Fake_parts_insert_in_Un [dest]
+declare analz_into_parts [dest]
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "A \<noteq> Server
+ ==> \<exists>X NB K. \<exists>evs \<in> yahalom.
+ Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] yahalom.Nil
+ [THEN yahalom.YM1, THEN yahalom.Reception,
+ THEN yahalom.YM2, THEN yahalom.Reception,
+ THEN yahalom.YM3, THEN yahalom.Reception,
+ THEN yahalom.YM4])
+apply possibility
+done
+
+lemma Gets_imp_Says:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
+by (erule rev_mp, erule yahalom.induct, auto)
+
+(*Must be proved separately for each protocol*)
+lemma Gets_imp_knows_Spy:
+ "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
+
+
+(**** Inductive proofs about yahalom ****)
+
+(** For reasoning about the encrypted portion of messages **)
+
+(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+lemma YM4_analz_knows_Spy:
+ "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ ==> X \<in> analz (knows Spy evs)"
+by blast
+
+lemmas YM4_parts_knows_Spy =
+ YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+
+
+(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees a good agent's shared key!*)
+lemma Spy_see_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_parts_knows_Spy, simp_all)
+apply blast+
+done
+
+lemma Spy_analz_shrK [simp]:
+ "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
+by auto
+
+lemma Spy_see_shrK_D [dest!]:
+ "[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
+by (blast dest: Spy_see_shrK)
+
+(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
+lemma new_keys_not_used [rule_format, simp]:
+ "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3, YM4*)
+apply (blast dest!: keysFor_parts_insert)+
+done
+
+
+(****
+ The following is to prove theorems of the form
+
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
+ Key K \<in> analz (knows Spy evs)
+
+ A more general formula must be proved inductively.
+****)
+
+(** Session keys are not used to encrypt other session keys **)
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> yahalom ==>
+ \<forall>K KK. KK <= - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+apply (erule yahalom.induct, force,
+ drule_tac [6] YM4_analz_knows_Spy)
+apply analz_freshK
+apply spy_analz
+done
+
+lemma analz_insert_freshK: "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
+ Key K \<in> analz (insert (Key KAB) (knows Spy evs)) =
+ (K = KAB | Key K \<in> analz (knows Spy evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(*** The Key K uniquely identifies the Server's message. **)
+
+lemma unique_session_keys:
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+ Says Server A'
+ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+ evs \<in> yahalom |]
+ ==> A=A' & B=B' & na=na' & nb=nb'"
+apply (erule rev_mp, erule rev_mp)
+apply (erule yahalom.induct, simp_all)
+(*YM3, by freshness, and YM4*)
+apply blast+
+done
+
+
+(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
+
+lemma secrecy_lemma:
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs -->
+ Key K \<notin> analz (knows Spy evs)"
+apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
+apply spy_analz (*Fake*)
+apply (blast dest: unique_session_keys) (*YM3*)
+done
+
+(*Final version*)
+lemma Spy_not_see_encrypted_key:
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest: secrecy_lemma)
+
- (*This message models possible leaks of session keys. The Nonces
- identify the protocol run. Quoting Server here ensures they are
- correct.*)
+(** Security Guarantee for A upon receiving YM3 **)
+
+(*If the encrypted message appears then it originated with the Server*)
+lemma A_trusts_YM3:
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+lemma A_gets_good_key:
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
+
+(** Security Guarantees for B upon receiving YM4 **)
+
+(*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B. But this part says nothing about nonces.*)
+lemma B_trusts_YM4_shrK:
+ "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NA NB. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy, simp_all)
+(*Fake, YM3*)
+apply blast+
+done
+
+(** Up to now, the reasoning is similar to standard Yahalom. Now the
+ doubtful reasoning occurs. We should not be assuming that an unknown
+ key is secure, but the model allows us to: there is no Oops rule to
+ let session keys become compromised.*)
+
+(*B knows, by the second part of A's message, that the Server distributed
+ the key quoting nonce NB. This part says nothing about agent names.
+ Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
+ the secrecy of NB.*)
+lemma B_trusts_YM4_newK [rule_format]:
+ "[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|]
+ ==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
+ (\<exists>A B NA. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K,
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs)"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake*)
+apply blast
+(*YM3*)
+apply blast
+(*A is uncompromised because NB is secure
+ A's certificate guarantees the existence of the Server message*)
+apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
+ dest: Says_imp_spies
+ parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
+done
+
+
+(*B's session key guarantee from YM4. The two certificates contribute to a
+ single conclusion about the Server's message. *)
+lemma B_trusts_YM4:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>na nb. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs"
+by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key
+ unique_session_keys)
+
+
+(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+lemma B_gets_good_key:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> analz (knows Spy evs)"
+by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
+
+
+(*** Authenticating B to A: these proofs are not considered.
+ They are irrelevant to showing the need for Oops. ***)
+
+
+(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
+
+(*Assuming the session key is secure, if both certificates are present then
+ A has said NB. We can't be sure about the rest of A's message, but only
+ NB matters for freshness.*)
+lemma A_Said_YM3_lemma [rule_format]:
+ "evs \<in> yahalom
+ ==> Key K \<notin> analz (knows Spy evs) -->
+ Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
+ Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
+ B \<notin> bad -->
+ (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
+apply (erule yahalom.induct, force,
+ frule_tac [6] YM4_parts_knows_Spy)
+apply (analz_mono_contra, simp_all)
+(*Fake*)
+apply blast
+(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+apply (force dest!: Crypt_imp_keysFor)
+(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
+apply (simp add: ex_disj_distrib)
+(*yes: apply unicity of session keys*)
+apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
+ Crypt_Spy_analz_bad
+ dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
+done
+
+(*If B receives YM4 then A has used nonce NB (and therefore is alive).
+ Moreover, A associates K with NB (thus is talking about the same run).
+ Other premises guarantee secrecy of K.*)
+lemma YM4_imp_A_Said_YM3 [rule_format]:
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
+apply (blast intro!: A_Said_YM3_lemma
+ dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
+done
end
--- a/src/HOL/IsaMakefile Wed Apr 11 11:53:54 2001 +0200
+++ b/src/HOL/IsaMakefile Thu Apr 12 12:45:05 2001 +0200
@@ -304,15 +304,13 @@
$(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event_lemmas.ML Auth/Event.thy \
Auth/Message_lemmas.ML Auth/Message.thy Auth/NS_Public.thy \
Auth/NS_Public_Bad.thy \
- Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \
- Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \
+ Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \
Auth/OtwayRees_Bad.thy Auth/Public_lemmas.ML Auth/Public.thy Auth/ROOT.ML \
Auth/Recur.ML Auth/Recur.thy Auth/Shared_lemmas.ML Auth/Shared.thy \
- Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \
+ Auth/TLS.ML Auth/TLS.thy Auth/WooLam.thy \
Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \
Auth/KerberosIV.ML Auth/KerberosIV.thy \
- Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy \
- Auth/Yahalom_Bad.ML Auth/Yahalom_Bad.thy
+ Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy
@$(ISATOOL) usedir $(OUT)/HOL Auth