--- a/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.ML Fri Aug 21 16:14:34 1998 +0200
@@ -16,9 +16,6 @@
Tidied by lcp.
*)
-proof_timing:=true;
-HOL_quantifiers := false;
-
AddEs spies_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
--- a/src/HOL/Auth/NS_Public.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/NS_Public.ML Fri Aug 21 16:14:34 1998 +0200
@@ -7,9 +7,6 @@
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
*)
-set proof_timing;
-HOL_quantifiers := false;
-
AddEs spies_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
--- a/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML Fri Aug 21 16:14:34 1998 +0200
@@ -11,8 +11,6 @@
Proc. Royal Soc. 426 (1989)
*)
-HOL_quantifiers := false;
-
AddEs spies_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
--- a/src/HOL/Auth/NS_Shared.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Fri Aug 21 16:14:34 1998 +0200
@@ -10,8 +10,6 @@
Proc. Royal Soc. 426 (1989)
*)
-HOL_quantifiers := false;
-
AddEs spies_partsEs;
AddDs [impOfSubs analz_subset_parts];
AddDs [impOfSubs Fake_parts_insert];
--- a/src/HOL/Auth/NS_Shared.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Aug 21 16:14:34 1998 +0200
@@ -71,8 +71,7 @@
(*This message models possible leaks of session keys.
The two Nonces identify the protocol run: the rule insists upon
the true senders in order to make them accurate.*)
- Oops "[| evso: ns_shared; A ~= Spy;
- Says B A (Crypt K (Nonce NB)) : set evso;
+ Oops "[| evso: ns_shared; Says B A (Crypt K (Nonce NB)) : set evso;
Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
: set evso |]
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
--- a/src/HOL/Auth/OtwayRees.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Fri Aug 21 16:14:34 1998 +0200
@@ -92,8 +92,7 @@
(*Nobody can have used non-existent keys!*)
-Goal "evs : otway ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*Fake*)
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
@@ -114,7 +113,7 @@
(*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|}|} : set evs; \
-\ evs : otway |] \
+\ evs : otway |] \
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -144,23 +143,22 @@
(** Session keys are not used to encrypt other session keys **)
(*The equality makes the induction hypothesis easier to apply*)
-Goal "evs : otway ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
-\ (Key K : analz (Key``KK Un (spies evs))) = \
-\ (K : KK | Key K : analz (spies evs))";
+Goal "evs : otway ==> ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (spies evs))) = \
+\ (K : KK | Key K : analz (spies evs))";
by (etac otway.induct 1);
by analz_spies_tac;
by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+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 : otway; KAB ~: range shrK |] ==> \
-\ Key K : analz (insert (Key KAB) (spies evs)) = \
-\ (K = KAB | Key K : analz (spies evs))";
+Goal "[| evs : otway; KAB ~: range shrK |] \
+\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \
+\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
qed "analz_insert_freshK";
@@ -168,8 +166,8 @@
(*** The Key K uniquely identifies the Server's message. **)
Goal "evs : otway ==> \
-\ EX B' NA' NB' X'. ALL B NA NB X. \
-\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
+\ EX B' NA' NB' X'. ALL B NA NB X. \
+\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
by (etac otway.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
--- a/src/HOL/Auth/OtwayRees.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Aug 21 16:14:34 1998 +0200
@@ -72,7 +72,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evso: otway; B ~= Spy;
+ Oops "[| evso: 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"
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 16:14:34 1998 +0200
@@ -63,7 +63,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run. B is not assumed to know shrK A.*)
- Oops "[| evso: otway; B ~= Spy;
+ Oops "[| evso: 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|}|}
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 21 16:14:34 1998 +0200
@@ -69,7 +69,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run.*)
- Oops "[| evso: otway; B ~= Spy;
+ Oops "[| evso: 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"
--- a/src/HOL/Auth/ROOT.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/ROOT.ML Fri Aug 21 16:14:34 1998 +0200
@@ -11,6 +11,7 @@
writeln"Root file for HOL/Auth";
set proof_timing;
goals_limit := 1;
+HOL_quantifiers := false;
(*Shared-key protocols*)
time_use_thy "NS_Shared";
--- a/src/HOL/Auth/Recur.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Recur.ML Fri Aug 21 16:14:34 1998 +0200
@@ -9,6 +9,11 @@
Pretty.setdepth 30;
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
+
(** Possibility properties: traces that reach the end
ONE theorem would be more elegant and faster!
By induction on a list of agents (no repetitions)
@@ -104,8 +109,7 @@
val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
-Goal "Says C' B {|Crypt K X, X', RA|} : set evs \
-\ ==> RA : analz (spies evs)";
+Goal "Says C' B {|Crypt K X, X', RA|} : set evs ==> RA : analz (spies evs)";
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
qed "RA4_analz_spies";
@@ -121,11 +125,11 @@
(*For proving the easier theorems about X ~: parts (spies evs).*)
fun parts_induct_tac i =
- etac recur.induct i THEN
- forward_tac [RA2_parts_spies] (i+3) THEN
- forward_tac [respond_imp_responses] (i+4) THEN
- forward_tac [RA4_parts_spies] (i+5) THEN
- prove_simple_subgoals_tac i;
+ EVERY [etac recur.induct i,
+ forward_tac [RA4_parts_spies] (i+5),
+ forward_tac [respond_imp_responses] (i+4),
+ forward_tac [RA2_parts_spies] (i+3),
+ prove_simple_subgoals_tac i];
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
@@ -136,16 +140,15 @@
Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [parts_insert2, parts_insert_spies])));
+by Auto_tac;
(*RA3*)
-by (blast_tac (claset() addDs [Key_in_parts_respond]) 1);
+by (auto_tac (claset() addDs [Key_in_parts_respond],
+ simpset() addsimps [parts_insert_spies]));
qed "Spy_see_shrK";
Addsimps [Spy_see_shrK];
Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
+by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -156,16 +159,15 @@
(** Nobody can have used non-existent keys! **)
(*The special case of H={} has the same proof*)
-Goal "[| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \
+Goal "[| K : keysFor (parts (insert RB H)); RB : responses evs |] \
\ ==> K : range shrK | K : keysFor (parts H)";
by (etac rev_mp 1);
-by (etac (respond_imp_responses RS responses.induct) 1);
+by (etac responses.induct 1);
by Auto_tac;
qed_spec_mp "Key_in_keysFor_parts";
-Goal "evs : recur ==> \
-\ Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
+Goal "evs : recur ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
by (parts_induct_tac 1);
(*RA3*)
by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
@@ -244,8 +246,7 @@
(*Everything that's hashed is already in past traffic. *)
Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \
-\ evs : recur; A ~: bad |] \
-\ ==> X : parts (spies evs)";
+\ evs : recur; A ~: bad |] ==> X : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3 requires a further induction*)
@@ -267,15 +268,14 @@
\ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
\ --> B=B' & P=P'";
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
by (etac responses.induct 3);
by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib])));
by (clarify_tac (claset() addSEs partsEs) 1);
(*RA1,2: creation of new Nonce. Move assertion into global context*)
by (ALLGOALS (expand_case_tac "NA = ?y"));
by (REPEAT_FIRST (ares_tac [exI]));
-by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]
- addSEs spies_partsEs) 1));
+by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1));
val lemma = result();
Goalw [HPair_def]
@@ -342,10 +342,10 @@
qed "respond_certificate";
-Goal "!!K'. (PB,RB,KXY) : respond evs \
-\ ==> EX A' B'. ALL A B N. \
-\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
-\ --> (A'=A & B'=B) | (A'=B & B'=A)";
+Goal "(PB,RB,KXY) : respond evs \
+\ ==> EX A' B'. ALL A B N. \
+\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
+\ --> (A'=A & B'=B) | (A'=B & B'=A)";
by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib])));
(*Base case*)
@@ -354,19 +354,18 @@
by (expand_case_tac "K = KBC" 1);
by (dtac respond_Key_in_parts 1);
by (blast_tac (claset() addSIs [exI]
- addSEs partsEs
addDs [Key_in_parts_respond]) 1);
by (expand_case_tac "K = KAB" 1);
by (REPEAT (ares_tac [exI] 2));
by (ex_strip_tac 1);
by (dtac respond_certificate 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
val lemma = result();
Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
-\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
-\ (PB,RB,KXY) : respond evs |] \
-\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
+\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
+\ (PB,RB,KXY) : respond evs |] \
+\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -390,11 +389,11 @@
[shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib])));
(** LEVEL 5 **)
-by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 1);
by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
by (ALLGOALS Clarify_tac);
by (blast_tac (claset() addSDs [resp_analz_insert]
- addIs [impOfSubs analz_subset_parts]) 2);
+ addIs [impOfSubs analz_subset_parts]) 2);
by (blast_tac (claset() addSDs [respond_certificate]) 1);
by (Asm_full_simp_tac 1);
(*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
@@ -456,7 +455,7 @@
\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(*RA3*)
by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1);
qed_spec_mp "Hash_auth_sender";
@@ -473,7 +472,7 @@
\ Crypt (shrK A) Y : parts {RC}";
by (etac rev_mp 1);
by (parts_induct_tac 1);
-by (Fake_parts_insert_tac 1);
+by (Blast_tac 1);
(*RA4*)
by (Blast_tac 4);
(*RA3*)
--- a/src/HOL/Auth/Recur.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Aug 21 16:14:34 1998 +0200
@@ -92,7 +92,17 @@
RA|} : set evs4 |]
==> Says B A RA # evs4 : recur"
-(**No "oops" message can easily be expressed. Each session key is
- associated--in two separate messages--with two nonces.
-***)
end
+
+ (*No "oops" message can easily be expressed. Each session key is
+ associated--in two separate messages--with two nonces. This is
+ one try, but it isn't that useful. Re domino attack, note that
+ Recur.ML proves that each session key is secure provided the two
+ peers are, even if there are compromised agents elsewhere in
+ the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts,
+ etc.
+
+ Oops "[| evso: recur; Says Server B RB : set evso;
+ RB : responses evs'; Key K : parts {RB} |]
+ ==> Notes Spy {|Key K, RB|} # evso : recur"
+ *)
--- a/src/HOL/Auth/TLS.ML Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/TLS.ML Fri Aug 21 16:14:34 1998 +0200
@@ -163,8 +163,7 @@
little point in doing so: the loss of their private keys is a worse
breach of security.*)
Goalw [certificate_def]
- "[| certificate B KB : parts (spies evs); evs : tls |] \
-\ ==> pubK B = KB";
+ "[| certificate B KB : parts (spies evs); evs : tls |] ==> pubK B = KB";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
@@ -193,7 +192,7 @@
(*** Properties of items found in Notes ***)
Goal "[| Notes A {|Agent B, X|} : set evs; evs : tls |] \
-\ ==> Crypt (pubK B) X : parts (spies evs)";
+\ ==> Crypt (pubK B) X : parts (spies evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
by (blast_tac (claset() addIs [parts_insertI]) 1);
@@ -201,8 +200,8 @@
(*C may be either A or B*)
Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
-\ evs : tls \
-\ |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
+\ evs : tls |] \
+\ ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (ALLGOALS Clarify_tac);
@@ -215,8 +214,8 @@
(*Compared with the theorem above, both premise and conclusion are stronger*)
Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
-\ evs : tls \
-\ |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
+\ evs : tls |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
by (etac rev_mp 1);
by (parts_induct_tac 1);
(*ServerAccepts*)
@@ -230,7 +229,7 @@
Goal "[| X : parts (spies evs); \
\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \
\ evs : tls; A ~: bad |] \
-\ ==> Says A B X : set evs";
+\ ==> Says A B X : set evs";
by (etac rev_mp 1);
by (hyp_subst_tac 1);
by (parts_induct_tac 1);
@@ -242,7 +241,7 @@
\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
\ certificate A KA : parts (spies evs); \
\ evs : tls; A ~: bad |] \
-\ ==> Says A B X : set evs";
+\ ==> Says A B X : set evs";
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
qed "TrustCertVerify";
@@ -275,12 +274,13 @@
Addsimps [no_Notes_A_PRF];
-Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); \
-\ evs : tls |] \
-\ ==> Nonce PMS : parts (spies evs)";
+Goal "[| Nonce (PRF (PMS,NA,NB)) : parts (spies evs); evs : tls |] \
+\ ==> Nonce PMS : parts (spies evs)";
by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
+(*SpyKeys*)
+by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 1);
(*Six others, all trivial or by freshness*)
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]
addSEs spies_partsEs) 1));
@@ -321,9 +321,8 @@
**)
(*In A's internal Note, PMS determines A and B.*)
-Goal "evs : tls \
-\ ==> EX A' B'. ALL A B. \
-\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
+Goal "evs : tls ==> EX A' B'. ALL A B. \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
by (parts_induct_tac 1);
by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
@@ -344,9 +343,9 @@
(*Key compromise lemma needed to prove analz_image_keys.
No collection of keys can help the spy get new private keys.*)
-Goal "evs : tls ==> \
-\ ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
-\ (priK B : KK | B : bad)";
+Goal "evs : tls \
+\ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
+\ (priK B : KK | B : bad)";
by (etac tls.induct 1);
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
@@ -416,7 +415,7 @@
by (hyp_subst_tac 1);
by (analz_induct_tac 1);
(*SpyKeys*)
-by (blast_tac (claset() addSEs spies_partsEs) 3);
+by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 3);
(*Fake*)
by (Fake_parts_insert_tac 2);
(** LEVEL 6 **)
@@ -512,9 +511,9 @@
(*If A created PMS then nobody other than the Spy would send a message
using a clientK generated from that PMS.*)
Goal "[| evs : tls; A' ~= Spy |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
-\ A = A'";
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
+\ A = A'";
by (analz_induct_tac 1); (*8 seconds*)
by (ALLGOALS Clarify_tac);
(*ClientFinished, ClientResume: by unicity of PMS*)
@@ -531,9 +530,9 @@
(*If A created PMS and has not leaked her clientK to the Spy,
then nobody has.*)
Goal "evs : tls \
-\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
-\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
+\ ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs)";
by (etac tls.induct 1);
(*This roundabout proof sequence avoids looping in simplification*)
by (ALLGOALS Simp_tac);
@@ -554,9 +553,9 @@
(*If A created PMS for B, then nobody other than B or the Spy would
send a message using a serverK generated from that PMS.*)
Goal "[| evs : tls; A ~: bad; B ~: bad; B' ~= Spy |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
-\ B = B'";
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs --> \
+\ B = B'";
by (analz_induct_tac 1); (*9 seconds*)
by (ALLGOALS Clarify_tac);
(*ServerResume, ServerFinished: by unicity of PMS*)
@@ -690,10 +689,10 @@
***)
Goal "[| M = PRF(PMS,NA,NB); evs : tls; A ~: bad; B ~: bad |] \
-\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
-\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \
-\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
+\ ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
+\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) --> \
+\ Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
by (hyp_subst_tac 1);
by (analz_induct_tac 1); (*15 seconds*)
by (ALLGOALS Clarify_tac);
@@ -716,7 +715,7 @@
\ Notes A {|Agent B, Nonce PMS|} : set evs; \
\ Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs; \
\ evs : tls; A ~: bad; B ~: bad |] \
-\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
+\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
by (blast_tac (claset() addIs [lemma]
addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
qed "TrustClientMsg";
@@ -733,8 +732,8 @@
\ certificate A KA : parts (spies evs); \
\ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
\ : set evs; \
-\ evs : tls; A ~: bad; B ~: bad |] \
-\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
+\ evs : tls; A ~: bad; B ~: bad |] \
+\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify]
addDs [Says_imp_spies RS parts.Inj]) 1);
qed "AuthClientFinished";
--- a/src/HOL/Auth/TLS.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/TLS.thy Fri Aug 21 16:14:34 1998 +0200
@@ -88,7 +88,7 @@
SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
"[| evsSK: tls;
- Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
+ {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
==> Notes Spy {| Nonce (PRF(M,NA,NB)),
Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"
--- a/src/HOL/Auth/Yahalom.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Aug 21 16:14:34 1998 +0200
@@ -60,7 +60,7 @@
(*This message models possible leaks of session keys. The Nonces
identify the protocol run. Quoting Server here ensures they are
correct.*)
- Oops "[| evso: yahalom; A ~= Spy;
+ Oops "[| evso: yahalom;
Says Server A {|Crypt (shrK A)
{|Agent B, Key K, Nonce NA, Nonce NB|},
X|} : set evso |]
--- a/src/HOL/Auth/Yahalom2.thy Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Fri Aug 21 16:14:34 1998 +0200
@@ -64,7 +64,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
- Oops "[| evso: yahalom; A ~= Spy;
+ Oops "[| evso: yahalom;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} : set evso |]