Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument
--- a/src/HOL/Auth/NS_Public.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public.ML Thu Dec 19 11:58:39 1996 +0100
@@ -84,9 +84,9 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : ns_public ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!evs. evs : ns_public ==> \
+\ length evs <= i --> \
+\ Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
@@ -104,8 +104,8 @@
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz] @ pushes)
- setloop split_tac [expand_if]));
+ (!simpset addsimps [not_parts_not_analz]
+ setloop split_tac [expand_if]));
(**** Authenticity properties obtained from NS2 ****)
--- a/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:58:39 1996 +0100
@@ -25,15 +25,16 @@
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1 "[| evs: ns_public; A ~= B |]
- ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
- : ns_public"
+ ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
+ # evs : ns_public"
(*Bob responds to Alice's message with a further nonce*)
NS2 "[| evs: ns_public; A ~= B;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|})
- # evs : ns_public"
+ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)),
+ Agent B|})
+ # evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
--- a/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 19 11:58:39 1996 +0100
@@ -89,9 +89,8 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : ns_public ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : ns_public ==> \
+\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
@@ -109,7 +108,7 @@
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz] @ pushes)
+ (!simpset addsimps [not_parts_not_analz]
setloop split_tac [expand_if]));
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Dec 19 11:58:39 1996 +0100
@@ -29,15 +29,15 @@
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1 "[| evs: ns_public; A ~= B |]
- ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
- : ns_public"
+ ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
+ # evs : ns_public"
(*Bob responds to Alice's message with a further nonce*)
NS2 "[| evs: ns_public; A ~= B;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs
- : ns_public"
+ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs))|})
+ # evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
--- a/src/HOL/Auth/NS_Shared.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Thu Dec 19 11:58:39 1996 +0100
@@ -111,8 +111,7 @@
(*Nobody can have SEEN keys that will be generated in the future. *)
goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -124,10 +123,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : ns_shared lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : ns_shared lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -139,8 +138,7 @@
(*** Future nonces can't be seen or used! ***)
goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST
(fast_tac (!claset addSEs partsEs
@@ -156,8 +154,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
goal thy "!!evs. evs : ns_shared lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+\ length evs <= i --> \
+\ newK i ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*NS1 and NS2*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2]));
@@ -189,11 +187,10 @@
(*Describes the form of K, X and K' when the Server sends this message.*)
goal thy
"!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
-\ evs : ns_shared lost |] \
-\ ==> (EX evt: ns_shared lost. \
-\ K = Key(newK evt) & \
-\ X = (Crypt (shrK B) {|K, Agent A|}) & \
-\ K' = shrK A)";
+\ evs : ns_shared lost |] \
+\ ==> (EX i. K = Key(newK i) & \
+\ X = (Crypt (shrK B) {|K, Agent A|}) & \
+\ K' = shrK A)";
by (etac rev_mp 1);
by (etac ns_shared.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -222,9 +219,8 @@
goal thy
"!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \
\ : set_of_list evs; evs : ns_shared lost |] \
-\ ==> (EX evt: ns_shared lost. K = newK evt & \
-\ length evt < length evs & \
-\ X = (Crypt (shrK B) {|Key K, Agent A|})) \
+\ ==> (EX i. K = newK i & i < length evs & \
+\ X = (Crypt (shrK B) {|Key K, Agent A|})) \
\ | X : analz (sees lost Spy evs)";
by (case_tac "A : lost" 1);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
@@ -242,14 +238,14 @@
forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN
Full_simp_tac 7 THEN
- REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac);
+ REPEAT_FIRST (eresolve_tac [asm_rl, exE, disjE] ORELSE' hyp_subst_tac);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -261,7 +257,7 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : ns_shared lost ==> \
-\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
+\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \
\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by (etac ns_shared.induct 1);
by parts_Fake_tac;
@@ -285,23 +281,22 @@
by (etac ns_shared.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS
+by (ALLGOALS (*Takes 18 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
-(*NS3, Fake*)
+(*NS4, Fake*)
by (EVERY (map spy_analz_tac [5,2]));
+(*NS3, NS2, Base*)
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
-(*NS3, NS2, Base*)
-by (REPEAT (Fast_tac 3));
qed_spec_mp "analz_image_newK";
goal thy
"!!evs. evs : ns_shared lost ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -312,8 +307,8 @@
with a secure key **)
goal thy
- "!!evs. evs : ns_shared lost ==> \
-\ EX A' NA' B' X'. ALL A NA B X. \
+ "!!evs. evs : ns_shared lost ==> \
+\ EX A' NA' B' X'. ALL A NA B X. \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \
\ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
@@ -339,12 +334,7 @@
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
\ : set_of_list evs; \
\ evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL A.?P(A)")] asm_rl 1);
-by (fast_tac (!claset addSDs [ spec]
- delrules [conjI] addss (!simpset)) 1);
+by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -369,14 +359,14 @@
by (fast_tac (!claset addIs [parts_insertI]
addEs [Says_imp_old_keys RS less_irrefl]
addss (!simpset)) 2);
-(*OR4, OR2, Fake*)
-by (REPEAT_FIRST spy_analz_tac);
-(*NS3 and Oops subcases*) (**LEVEL 7 **)
+(*NS4, Fake*)
+by (EVERY (map spy_analz_tac [3,1]));
+(*NS3 and Oops subcases*) (**LEVEL 5 **)
by (step_tac (!claset delrules [impCE]) 1);
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
by (etac conjE 2);
by (mp_tac 2);
-(**LEVEL 11 **)
+(**LEVEL 9 **)
by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 2);
by (assume_tac 3);
by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 2);
@@ -460,7 +450,7 @@
by (Fast_tac 2);
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
(*Contradiction from the assumption
- Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *)
+ Crypt (newK(length evsa)) (Nonce NB) : parts (sees lost Spy evsa) *)
by (dtac Crypt_imp_invKey_keysFor 1);
(**LEVEL 10**)
by (Asm_full_simp_tac 1);
--- a/src/HOL/Auth/NS_Shared.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Thu Dec 19 11:58:39 1996 +0100
@@ -27,8 +27,8 @@
(*Alice initiates a protocol run, requesting to talk to any B*)
NS1 "[| evs: ns_shared lost; A ~= Server |]
- ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
- : ns_shared lost"
+ ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
+ # evs : ns_shared lost"
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
@@ -36,9 +36,10 @@
the sender field.*)
NS2 "[| evs: ns_shared lost; A ~= B; A ~= Server;
Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
- ==> Says Server A (Crypt (shrK A)
- {|Nonce NA, Agent B, Key (newK evs),
- (Crypt (shrK B) {|Key (newK evs), Agent A|})|})
+ ==> Says Server A
+ (Crypt (shrK A)
+ {|Nonce NA, Agent B, Key (newK(length evs)),
+ (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|})
# evs : ns_shared lost"
(*We can't assume S=Server. Agent A "remembers" her nonce.
@@ -53,7 +54,8 @@
from, but responds to A because she is mentioned inside.*)
NS4 "[| evs: ns_shared lost; A ~= B;
Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
- ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost"
+ ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs
+ : ns_shared lost"
(*Alice responds with Nonce NB if she has seen the key before.
Maybe should somehow check Nonce NA again.
--- a/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Thu Dec 19 11:58:39 1996 +0100
@@ -16,7 +16,6 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 15;
(*A "possibility property": there are traces that reach the end*)
@@ -132,9 +131,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway lost ==> \
+\ length evs <= i --> Key (newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -146,10 +144,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : otway lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -159,9 +157,9 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!evs. evs : otway lost ==> \
+\ length evs <= i --> \
+\ Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
@@ -175,10 +173,10 @@
Addsimps [new_nonces_not_seen];
(*Variant: old messages must contain old nonces!*)
-goal thy "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN evt) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> length evt < length evs";
+goal thy "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN i) : parts {X}; \
+\ evs : otway lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -188,9 +186,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway lost ==> \
+\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
by (parts_induct_tac 1);
(*OR1 and OR3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
@@ -218,9 +215,9 @@
for Oops case.*)
goal thy
"!!evs. [| Says Server B \
-\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
+\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
+\ evs : otway lost |] \
+\ ==> (EX n. K = Key(newK n)) & \
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -234,14 +231,14 @@
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
****)
@@ -257,10 +254,10 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 12 secs*)
+by (ALLGOALS (*Takes 11 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
(*OR4, OR2, Fake*)
by (EVERY (map spy_analz_tac [5,3,2]));
@@ -271,8 +268,8 @@
goal thy
"!!evs. evs : otway lost ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -442,8 +439,8 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
+ analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
--- a/src/HOL/Auth/OtwayRees.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Thu Dec 19 11:58:39 1996 +0100
@@ -29,9 +29,9 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
- ==> Says A B {|Nonce (newN evs), Agent A, Agent B,
+ ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B,
Crypt (shrK A)
- {|Nonce (newN evs), Agent A, Agent B|} |}
+ {|Nonce (newN(length evs)), Agent A, Agent B|} |}
# evs : otway lost"
(*Bob's response to Alice's message. Bob doesn't know who
@@ -41,8 +41,8 @@
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X,
- Crypt
- (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|}
+ Crypt (shrK B)
+ {|Nonce NA, Nonce(newN(length evs)), Agent A, Agent B|}|}
# evs : otway lost"
(*The Server receives Bob's message and checks that the three NAs
@@ -56,8 +56,8 @@
: set_of_list evs |]
==> Says Server B
{|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
- Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
+ Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
+ Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Thu Dec 19 11:58:39 1996 +0100
@@ -120,9 +120,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway lost ==> \
+\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -134,10 +133,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : otway lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : otway lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -147,9 +146,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway lost ==> \
+\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*Fake, OR4: these messages send unknown (X) components*)
by (EVERY
@@ -180,9 +178,8 @@
\ {|Crypt (shrK A) {|NA, Agent A, Agent B, K|}, \
\ Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
\ evs : otway lost |] \
-\ ==> (EX evt: otway lost. K = Key(newK evt)) & \
-\ (EX i. NA = Nonce i) & \
-\ (EX j. NB = Nonce j)";
+\ ==> (EX n. K = Key(newK n)) & \
+\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -194,14 +191,14 @@
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -218,12 +215,11 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 28 secs*)
+by (ALLGOALS (*Takes 18 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
-(** LEVEL 5 **)
(*OR4, Fake*)
by (EVERY (map spy_analz_tac [4,2]));
(*Oops, OR3, Base*)
@@ -233,8 +229,8 @@
goal thy
"!!evs. evs : otway lost ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -333,8 +329,8 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
+ analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Dec 19 11:58:39 1996 +0100
@@ -29,14 +29,15 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway lost; A ~= B; B ~= Server |]
- ==> Says A B {|Agent A, Agent B, Nonce (newN evs)|}
+ ==> Says A B {|Agent A, Agent B, Nonce (newN(length evs))|}
# evs : otway lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
OR2 "[| evs: otway lost; B ~= Server;
Says A' B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
- ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
+ ==> Says B Server {|Agent A, Agent B, Nonce NA,
+ Nonce (newN(length evs))|}
# evs : otway lost"
(*The Server receives Bob's message. Then he sends a new
@@ -45,8 +46,10 @@
Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set_of_list evs |]
==> Says Server B
- {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
- Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
+ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B,
+ Key(newK(length evs))|},
+ Crypt (shrK B) {|Nonce NB, Agent A, Agent B,
+ Key(newK(length evs))|}|}
# evs : otway lost"
(*Bob receives the Server's (?) message and compares the Nonces with
--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Dec 19 11:58:39 1996 +0100
@@ -132,9 +132,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -146,10 +145,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : otway \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : otway \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -159,9 +158,8 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ Nonce (newN evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST
(fast_tac (!claset addSEs partsEs
@@ -175,10 +173,10 @@
(*Variant: old messages must contain old nonces!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN evt) : parts {X}; \
-\ evs : otway \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN i) : parts {X}; \
+\ evs : otway \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -188,9 +186,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : otway ==> \
+\ length evs <= i --> newK i ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*OR1 and OR3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
@@ -219,8 +216,8 @@
goal thy
"!!evs. [| Says Server B \
\ {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs; \
-\ evs : otway |] \
-\ ==> (EX evt: otway. K = Key(newK evt)) & \
+\ evs : otway |] \
+\ ==> (EX n. K = Key(newK n)) & \
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
by (etac rev_mp 1);
by (etac otway.induct 1);
@@ -234,14 +231,14 @@
dtac OR4_analz_sees_Spy 6 THEN
forward_tac [Says_Server_message_form] 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
+ REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -267,12 +264,11 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, lemma]));
-by (ALLGOALS
+by (ALLGOALS (*Takes 18 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
-(** LEVEL 7 **)
(*OR4, OR2, Fake*)
by (EVERY (map spy_analz_tac [5,3,2]));
(*Oops, OR3, Base*)
@@ -282,8 +278,8 @@
goal thy
"!!evs. evs : otway ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -293,7 +289,7 @@
(*** The Key K uniquely identifies the Server's message. **)
goal thy
- "!!evs. evs : otway ==> \
+ "!!evs. evs : otway ==> \
\ EX B' NA' NB' X'. ALL B NA NB X. \
\ Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
\ B=B' & NA=NA' & NB=NB' & X=X'";
@@ -332,8 +328,8 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (ALLGOALS
- (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (asm_simp_tac (!simpset addsimps [not_parts_not_analz,
+ analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*OR3*)
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Thu Dec 19 11:58:39 1996 +0100
@@ -28,9 +28,9 @@
(*Alice initiates a protocol run*)
OR1 "[| evs: otway; A ~= B; B ~= Server |]
- ==> Says A B {|Nonce (newN evs), Agent A, Agent B,
+ ==> Says A B {|Nonce (newN(length evs)), Agent A, Agent B,
Crypt (shrK A)
- {|Nonce (newN evs), Agent A, Agent B|} |}
+ {|Nonce (newN(length evs)), Agent A, Agent B|} |}
# evs : otway"
(*Bob's response to Alice's message. Bob doesn't know who
@@ -39,7 +39,7 @@
OR2 "[| evs: otway; B ~= Server;
Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
==> Says B Server
- {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs),
+ {|Nonce NA, Agent A, Agent B, X, Nonce (newN(length evs)),
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
# evs : otway"
@@ -55,8 +55,8 @@
: set_of_list evs |]
==> Says Server B
{|Nonce NA,
- Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
- Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
+ Crypt (shrK A) {|Nonce NA, Key (newK(length evs))|},
+ Crypt (shrK B) {|Nonce NB, Key (newK(length evs))|}|}
# evs : otway"
(*Bob receives the Server's (?) message and compares the Nonces with
--- a/src/HOL/Auth/Public.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Public.ML Thu Dec 19 11:58:39 1996 +0100
@@ -27,15 +27,14 @@
(*** Basic properties of pubK ***)
(*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_pubK RS inj_eq];
-AddSDs [newN_length];
+AddIffs [inj_pubK RS inj_eq, inj_newN RS inj_eq];
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
-goal thy "Nonce (newN evs) ~: parts (initState lost B)";
+goal thy "Nonce (newN i) ~: parts (initState lost B)";
by (agent.induct_tac "B" 1);
by (Auto_tac ());
qed "newN_notin_initState";
--- a/src/HOL/Auth/Public.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Public.thy Thu Dec 19 11:58:39 1996 +0100
@@ -50,17 +50,16 @@
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-(*Agents generate "random" nonces. These are uniquely determined by
- the length of their argument, a trace.*)
+(*Agents generate "random" nonces, uniquely determined by their argument.*)
consts
- newN :: "event list => nat"
+ newN :: nat => nat
rules
(*Public keys are disjoint, and never clash with private keys*)
- inj_pubK "inj pubK"
- priK_neq_pubK "priK A ~= pubK B"
+ inj_pubK "inj pubK"
+ priK_neq_pubK "priK A ~= pubK B"
- newN_length "(newN evs = newN evt) ==> (length evs = length evt)"
+ inj_newN "inj newN"
end
--- a/src/HOL/Auth/Recur.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Recur.ML Thu Dec 19 11:58:39 1996 +0100
@@ -27,8 +27,8 @@
\ Agent Server|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.NA1 RS
- (respond.One RSN (4,recur.NA3))) 2);
+by (rtac (recur.Nil RS recur.RA1 RS
+ (respond.One RSN (4,recur.RA3))) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]));
result();
@@ -42,9 +42,9 @@
\ Agent Server|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS
- (respond.One RS respond.Cons RSN (4,recur.NA3)) RS
- recur.NA4) 2);
+by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
+ (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
+ recur.RA4) 2);
by (REPEAT
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
THEN
@@ -60,9 +60,9 @@
\ Agent Server|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (rtac (recur.Nil RS recur.NA1 RS recur.NA2 RS recur.NA2 RS
+by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
(respond.One RS respond.Cons RS respond.Cons RSN
- (4,recur.NA3)) RS recur.NA4 RS recur.NA4) 2);
+ (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
by (REPEAT (*SLOW: 37 seconds*)
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
THEN
@@ -104,30 +104,30 @@
(** For reasoning about the encrypted portion of messages **)
-val NA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
+val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
\ ==> RA : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
-qed "NA4_analz_sees_Spy";
+qed "RA4_analz_sees_Spy";
-(*NA2_analz... and NA4_analz... let us treat those cases using the same
+(*RA2_analz... and RA4_analz... let us treat those cases using the same
argument as for the Fake case. This is possible for most, but not all,
- proofs: Fake does not invent new nonces (as in NA2), and of course Fake
+ proofs: Fake does not invent new nonces (as in RA2), and of course Fake
messages originate from the Spy. *)
-bind_thm ("NA2_parts_sees_Spy",
- NA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
-bind_thm ("NA4_parts_sees_Spy",
- NA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("RA2_parts_sees_Spy",
+ RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
+bind_thm ("RA4_parts_sees_Spy",
+ RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
(*We instantiate the variable to "lost". Leaving it as a Var makes proofs
harder to complete, since simplification does less for us.*)
val parts_Fake_tac =
let val tac = forw_inst_tac [("lost","lost")]
- in tac NA2_parts_sees_Spy 4 THEN
+ in tac RA2_parts_sees_Spy 4 THEN
forward_tac [respond_imp_responses] 5 THEN
- tac NA4_parts_sees_Spy 6
+ tac RA4_parts_sees_Spy 6
end;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
@@ -159,10 +159,10 @@
"!!evs. evs : recur lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
-(*NA2*)
+(*RA2*)
by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
addss (!simpset)) 1);
-(*NA3*)
+(*RA3*)
by (fast_tac (!claset addDs [Key_in_parts_respond]
addss (!simpset addsimps [parts_insert_sees])) 1);
qed "Spy_see_shrK";
@@ -191,7 +191,7 @@
\ length evs <= i --> \
\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
-(*NA2*)
+(*RA2*)
by (best_tac (!claset addSEs partsEs
addSDs [parts_cut]
addDs [Suc_leD]
@@ -201,9 +201,9 @@
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset)) 1);
-(*For NA3*)
+(*For RA3*)
by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
-(*NA1-NA4*)
+(*RA1-RA4*)
by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
addss (!simpset)) 1));
qed_spec_mp "new_keys_not_seen";
@@ -235,7 +235,7 @@
goal thy "!!i. evs : recur lost ==> \
\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
-(*For NA3*)
+(*For RA3*)
by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
addDs [Nonce_in_parts_respond, parts_cut, Suc_leD]
@@ -245,7 +245,7 @@
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset)) 1);
-(*NA1, NA2, NA4*)
+(*RA1, RA2, RA4*)
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
addEs [leD RS notE]
@@ -279,13 +279,13 @@
goal thy "!!i. evs : recur lost ==> \
\ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-(*NA3*)
+(*RA3*)
by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD]
addss (!simpset addsimps [parts_insert_sees])) 4);
-(*NA2*)
+(*RA2*)
by (fast_tac (!claset addSEs partsEs
addDs [Suc_leD] addss (!simpset)) 3);
-(*Fake, NA1, NA4*)
+(*Fake, RA1, RA4*)
by (REPEAT
(best_tac
(!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
@@ -308,14 +308,14 @@
(*For proofs involving analz. We again instantiate the variable to "lost".*)
val analz_Fake_tac =
- dres_inst_tac [("lost","lost")] NA2_analz_sees_Spy 4 THEN
+ dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN
forward_tac [respond_imp_responses] 5 THEN
- dres_inst_tac [("lost","lost")] NA4_analz_sees_Spy 6;
+ dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
(** Session keys are not used to encrypt other session keys **)
-(*Version for "responses" relation. Handles case NA3 in the theorem below.
+(*Version for "responses" relation. Handles case RA3 in the theorem below.
Note that it holds for *any* set H (not just "sees lost Spy evs")
satisfying the inductive hypothesis.*)
goal thy
@@ -340,12 +340,12 @@
\ (K : newK``I | Key K : analz (sees lost Spy evs))";
by (etac recur.induct 1);
by analz_Fake_tac;
-be ssubst 4; (*NA2: DELETE needless definition of PA!*)
+be ssubst 4; (*RA2: DELETE needless definition of PA!*)
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
(*Base*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
-(*NA4, NA2, Fake*)
+(*RA4, RA2, Fake*)
by (REPEAT (spy_analz_tac 1));
val raw_analz_image_newK = result();
qed_spec_mp "analz_image_newK";
@@ -381,12 +381,12 @@
\ (Nonce (newN i) : parts {X} --> \
\ Hash X ~: parts (sees lost Spy evs))";
be recur.induct 1;
-be ssubst 4; (*NA2: DELETE needless definition of PA!*)
+be ssubst 4; (*RA2: DELETE needless definition of PA!*)
by parts_Fake_tac;
-(*NA3 requires a further induction*)
+(*RA3 requires a further induction*)
be responses.induct 5;
by (ALLGOALS Asm_simp_tac);
-(*NA2*)
+(*RA2*)
by (best_tac (!claset addDs [Suc_leD, parts_cut]
addEs [leD RS notE,
new_nonces_not_seen RSN(2,rev_notE)]
@@ -405,7 +405,7 @@
(** The Nonce NA uniquely identifies A's message.
- This theorem applies to rounds NA1 and NA2!
+ This theorem applies to rounds RA1 and RA2!
**)
goal thy
@@ -414,15 +414,15 @@
\ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs) --> B=B' & P=P'";
be recur.induct 1;
-be ssubst 4; (*NA2: DELETE needless definition of PA!*)
-(*For better simplification of NA2*)
+be ssubst 4; (*RA2: DELETE needless definition of PA!*)
+(*For better simplification of RA2*)
by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4);
by parts_Fake_tac;
-(*NA3 requires a further induction*)
+(*RA3 requires a further induction*)
be responses.induct 5;
by (ALLGOALS Asm_simp_tac);
by (step_tac (!claset addSEs partsEs) 1);
-(*NA3: inductive case*)
+(*RA3: inductive case*)
by (best_tac (!claset addss (!simpset)) 5);
(*Fake*)
by (best_tac (!claset addSIs [exI]
@@ -433,13 +433,13 @@
by (fast_tac (!claset addss (!simpset)) 1);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
-(*NA1: creation of new Nonce. Move assertion into global context*)
+(*RA1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
by (best_tac (!claset addSIs [exI]
addEs [Hash_new_nonces_not_seen]
addss (!simpset)) 1);
by (best_tac (!claset addss (!simpset)) 1);
-(*NA2: creation of new Nonce*)
+(*RA2: creation of new Nonce*)
by (expand_case_tac "NA = ?y" 1);
by (best_tac (!claset addSIs [exI]
addDs [parts_cut]
@@ -510,7 +510,7 @@
(*The Server does not send such messages. This theorem lets us avoid
- assuming B~=Server in NA4.*)
+ assuming B~=Server in RA4.*)
goal thy
"!!evs. evs : recur lost \
\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
@@ -557,7 +557,7 @@
qed "unique_session_keys";
-(** Crucial secrecy property: Spy does not see the keys sent in msg NA3
+(** Crucial secrecy property: Spy does not see the keys sent in msg RA3
Does not in itself guarantee security: an attack could violate
the premises, e.g. by having A=Spy **)
@@ -614,24 +614,24 @@
\ Key K ~: analz (sees lost Spy evs)";
by (etac recur.induct 1);
by analz_Fake_tac;
-be ssubst 4; (*NA2: DELETE needless definition of PA!*)
+be ssubst 4; (*RA2: DELETE needless definition of PA!*)
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
setloop split_tac [expand_if])));
-(*NA4*)
+(*RA4*)
by (spy_analz_tac 4);
(*Fake*)
by (spy_analz_tac 1);
by (step_tac (!claset delrules [impCE]) 1);
-(*NA2*)
+(*RA2*)
by (spy_analz_tac 1);
-(*NA3, case 2: K is an old key*)
+(*RA3, case 2: K is an old key*)
by (fast_tac (!claset addSDs [resp_analz_insert]
addSEs partsEs
addDs [Key_in_parts_respond]
addEs [Says_imp_old_keys RS less_irrefl]) 2);
-(*NA3, case 1: use lemma previously proved by induction*)
+(*RA3, case 1: use lemma previously proved by induction*)
by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
(2,rev_notE)]) 1);
bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
@@ -652,7 +652,7 @@
(**** Authenticity properties for Agents ****)
-(*Only NA1 or NA2 can have caused such a part of a message to appear.*)
+(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
goal thy
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
\ : parts (sees lost Spy evs); \
@@ -662,9 +662,9 @@
\ : set_of_list evs";
be rev_mp 1;
by (parts_induct_tac 1);
-(*NA3*)
+(*RA3*)
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2);
-(*NA2*)
+(*RA2*)
by ((REPEAT o CHANGED) (*Push in XA*)
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
by (best_tac (!claset addSEs partsEs
@@ -692,22 +692,22 @@
in a run, then it originated with the Server!*)
goal thy
"!!evs. [| A ~: lost; A ~= Spy; evs : recur lost |] \
-\ ==> Crypt (shrK A) {|Key K, Agent B, NA|} : parts (sees lost Spy evs) \
+\ ==> Crypt (shrK A) {|Key K, Agent A', NA|} : parts (sees lost Spy evs) \
\ --> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \
\ Agent A, Agent B, NA, P|} \
\ : set_of_list evs \
\ --> (EX C RC. Says Server C RC : set_of_list evs & \
-\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC})";
+\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC})";
by (parts_induct_tac 1);
-(*NA4*)
+(*RA4*)
by (best_tac (!claset addSEs [MPair_parts]
addSDs [Hash_auth_sender]
addSIs [disjI2]) 4);
-(*NA1: it cannot be a new Nonce, contradiction.*)
+(*RA1: it cannot be a new Nonce, contradiction.*)
by (fast_tac (!claset delrules [impCE]
addSEs [nonce_not_seen_now, MPair_parts]
addDs [parts.Body]) 1);
-(*NA2: it cannot be a new Nonce, contradiction.*)
+(*RA2: it cannot be a new Nonce, contradiction.*)
by ((REPEAT o CHANGED) (*Push in XA*)
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
by (deepen_tac (!claset delrules [impCE]
@@ -715,7 +715,7 @@
addSEs [MPair_parts]
addDs [parts_cut, parts.Body]
addss (!simpset)) 0 1);
-(*NA3*) (** LEVEL 5 **)
+(*RA3*) (** LEVEL 5 **)
by (REPEAT (safe_step_tac (!claset addSEs [responses_no_Hash_Server]
delrules [impCE]) 1));
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
@@ -727,13 +727,13 @@
then the key really did come from the Server!*)
goal thy
"!!evs. [| Says B' A RA : set_of_list evs; \
-\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA}; \
+\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \
\ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \
\ Agent A, Agent B, NA, P|} \
\ : set_of_list evs; \
\ A ~: lost; A ~= Spy; evs : recur lost |] \
\ ==> EX C RC. Says Server C RC : set_of_list evs & \
-\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RC}";
+\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC}";
by (best_tac (!claset addSIs [Crypt_imp_Server_msg]
addDs [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)]
addss (!simpset)) 1);
@@ -744,12 +744,12 @@
then the only other agent who knows the key is B.*)
goal thy
"!!evs. [| Says B' A RA : set_of_list evs; \
-\ Crypt (shrK A) {|Key K, Agent B, NA|} : parts {RA}; \
+\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \
\ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \
\ Agent A, Agent B, NA, P|} \
\ : set_of_list evs; \
-\ C ~: {A,B,Server}; \
-\ A ~: lost; B ~: lost; A ~= Spy; evs : recur lost |] \
+\ C ~: {A,A',Server}; \
+\ A ~: lost; A' ~: lost; A ~= Spy; evs : recur lost |] \
\ ==> Key K ~: analz (sees lost C evs)";
by (dtac Agent_trust 1 THEN REPEAT_FIRST assume_tac);
by (fast_tac (!claset addSEs [Agent_not_see_encrypted_key RSN(2,rev_notE)]) 1);
--- a/src/HOL/Auth/Recur.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Recur.thy Thu Dec 19 11:58:39 1996 +0100
@@ -77,7 +77,7 @@
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
- NA1 "[| evs: recur lost; A ~= B; A ~= Server;
+ RA1 "[| evs: recur lost; A ~= B; A ~= Server;
MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
@@ -85,7 +85,7 @@
XA should be the Hash of the remaining components with KA, but
Bob cannot check that.
P is the previous recur message from Alice's caller.*)
- NA2 "[| evs: recur lost; B ~= C; B ~= Server;
+ RA2 "[| evs: recur lost; B ~= C; B ~= Server;
Says A' B PA : set_of_list evs;
PA = {|XA, Agent A, Agent B, Nonce NA, P|};
MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
@@ -93,14 +93,14 @@
(*The Server receives and decodes Bob's message. Then he generates
a new session key and a response.*)
- NA3 "[| evs: recur lost; B ~= Server;
+ RA3 "[| evs: recur lost; B ~= Server;
Says B' Server PB : set_of_list evs;
(0,PB,RB) : respond (length evs) |]
==> Says Server B RB # evs : recur lost"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
- NA4 "[| evs: recur lost; A ~= B;
+ RA4 "[| evs: recur lost; A ~= B;
Says C' B {|Agent B,
Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
Agent B,
--- a/src/HOL/Auth/Shared.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Shared.ML Thu Dec 19 11:58:39 1996 +0100
@@ -26,62 +26,35 @@
(*** Basic properties of shrK and newK ***)
-goalw thy [newN_def] "!!evs. newN evs = newN evt ==> length evs = length evt";
-by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
-qed "newN_length";
-
-goalw thy [newK_def] "!!evs. newK evs = newK evt ==> length evs = length evt";
-by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
-qed "newK_length";
-
-goalw thy [newK_def] "newK evs ~= shrK A";
-by (rtac random_neq_shrK 1);
-qed "newK_neq_shrK";
-
-goalw thy [newK_def] "isSymKey (newK evs)";
-by (rtac isSym_random 1);
-qed "isSym_newK";
+(*Injectiveness and freshness of new keys and nonces*)
+AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq,
+ inj_newK RS inj_eq, inj_nPair RS inj_eq];
(* invKey (shrK A) = shrK A *)
bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
-(* invKey (random x) = random x *)
-bind_thm ("invKey_random", rewrite_rule [isSymKey_def] isSym_random);
-
-(* invKey (newK evs) = newK evs *)
+(* invKey (newK i) = newK i *)
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
-Addsimps [invKey_shrK, invKey_random, invKey_newK];
+Addsimps [invKey_shrK, invKey_newK];
-goal thy "!!K. random x = invKey K ==> random x = K";
-by (rtac (invKey_eq RS iffD1) 1);
-by (Simp_tac 1);
-val random_invKey = result();
-
-AddSDs [random_invKey, sym RS random_invKey];
-
-goal thy "!!K. newK evs = invKey K ==> newK evs = K";
+goal thy "!!K. newK i = invKey K ==> newK i = K";
by (rtac (invKey_eq RS iffD1) 1);
by (Simp_tac 1);
val newK_invKey = result();
AddSDs [newK_invKey, sym RS newK_invKey];
-(*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq, inj_random RS inj_eq];
-AddSDs [newN_length, newK_length];
-
-Addsimps [random_neq_shrK, random_neq_shrK RS not_sym,
- newK_neq_shrK, newK_neq_shrK RS not_sym];
+Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
-goal thy "Key (newK evs) ~: parts (initState lost B)";
+goal thy "Key (newK i) ~: parts (initState lost B)";
by (agent.induct_tac "B" 1);
by (Auto_tac ());
qed "newK_notin_initState";
-goal thy "Nonce (newN evs) ~: parts (initState lost B)";
+goal thy "Nonce (newN i) ~: parts (initState lost B)";
by (agent.induct_tac "B" 1);
by (Auto_tac ());
qed "newN_notin_initState";
@@ -105,12 +78,6 @@
qed "shrK_notin_image_newK";
Addsimps [shrK_notin_image_newK];
-goal thy "shrK A ~: random``E";
-by (agent.induct_tac "A" 1);
-by (Auto_tac ());
-qed "shrK_notin_image_random";
-Addsimps [shrK_notin_image_random];
-
(*** Function "sees" ***)
--- a/src/HOL/Auth/Shared.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Shared.thy Thu Dec 19 11:58:39 1996 +0100
@@ -44,24 +44,25 @@
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
-(*Agents generate "random" numbers for use as symmetric keys, as well as
- nonces.*)
+(*Agents generate random (symmetric) keys and nonces.
+ The numeric argument is typically the length of the current trace.
+ An injective pairing function allows multiple keys/nonces to be generated
+ in one protocol round. A typical candidate for npair(i,j) is
+ 2^j(2i+1)
+*)
consts
- random :: "nat*nat => nat"
-
-constdefs
- newN :: event list => nat
- "newN evs == random (length evs, 0)"
-
- newK :: event list => nat
- "newK evs == random (length evs, 1)"
+ nPair :: "nat*nat => nat"
+ newN :: "nat => nat"
+ newK :: "nat => key"
rules
inj_shrK "inj shrK"
- inj_random "inj random"
+ inj_nPair "inj nPair"
+ inj_newN "inj newN"
+ inj_newK "inj newK"
- random_neq_shrK "random ij ~= shrK A"
- isSym_random "isSymKey (random ij)"
+ newK_neq_shrK "newK i ~= shrK A"
+ isSym_newK "isSymKey (newK i)"
end
--- a/src/HOL/Auth/WooLam.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/WooLam.ML Thu Dec 19 11:58:39 1996 +0100
@@ -96,9 +96,8 @@
(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : woolam ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : woolam ==> \
+\ length evs <= i --> Nonce(newN(i)) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
--- a/src/HOL/Auth/WooLam.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/WooLam.thy Thu Dec 19 11:58:39 1996 +0100
@@ -37,7 +37,7 @@
(*Bob responds to Alice's message with a challenge.*)
WL2 "[| evs: woolam; A ~= B;
Says A' B (Agent A) : set_of_list evs |]
- ==> Says B A (Nonce (newN evs)) # evs : woolam"
+ ==> Says B A (Nonce (newN(length evs))) # evs : woolam"
(*Alice responds to Bob's challenge by encrypting NB with her key.
B is *not* properly determined -- Alice essentially broadcasts
--- a/src/HOL/Auth/Yahalom.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Thu Dec 19 11:58:39 1996 +0100
@@ -118,9 +118,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : yahalom lost ==> \
+\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -132,10 +131,10 @@
(*Variant: old messages must contain old keys!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
-\ evs : yahalom lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Key (newK i) : parts {X}; \
+\ evs : yahalom lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -144,7 +143,7 @@
(*Ready-made for the classical reasoner*)
-goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|} \
+goal thy "!!evs. [| Says A B {|Crypt K {|b,Key(newK(length evs)),na,nb|}, X|}\
\ : set_of_list evs; evs : yahalom lost |] \
\ ==> R";
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
@@ -155,9 +154,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : yahalom lost ==> \
+\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
by (parts_induct_tac 1);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
@@ -187,10 +185,10 @@
(*Describes the form of K when the Server sends this message. Useful for
Oops as well as main secrecy property.*)
goal thy
- "!!evs. [| Says Server A \
+ "!!evs. [| Says Server A \
\ {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
-\ evs : yahalom lost |] \
-\ ==> (EX evt: yahalom lost. K = Key(newK evt))";
+\ evs : yahalom lost |] \
+\ ==> EX i. K = Key(newK i)";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -202,14 +200,14 @@
forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((etac bexE ORELSE' hyp_subst_tac) 7);
+ REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
- Key K : analz (sees lost Spy evs)
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
+ Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -221,7 +219,7 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. evs : yahalom lost ==> \
-\ (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
+\ (Crypt (newK i) X) : parts (sees lost Spy evs) & \
\ Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
by (etac yahalom.induct 1);
by parts_Fake_tac;
@@ -244,12 +242,11 @@
by (etac yahalom.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS
+by (ALLGOALS (*Takes 11 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
-(** LEVEL 5 **)
(*YM4, Fake*)
by (EVERY (map spy_analz_tac [4, 2]));
(*Oops, YM3, Base*)
@@ -258,8 +255,8 @@
goal thy
"!!evs. evs : yahalom lost ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key(newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -295,11 +292,7 @@
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -331,14 +324,13 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*YM3*)
by (Fast_tac 2); (*uses Says_too_new_key*)
(*OR4, Fake*)
by (REPEAT_FIRST spy_analz_tac);
-(*Oops*) (** LEVEL 6 **)
+(*Oops*)
by (fast_tac (!claset delrules [disjE]
addDs [unique_session_keys]
addss (!simpset)) 1);
@@ -381,8 +373,8 @@
"!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
\ B ~: lost; evs : yahalom lost |] \
\ ==> EX NA NB. Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, \
-\ Nonce NA, Nonce NB|}, \
+\ {|Crypt (shrK A) {|Agent B, Key K, \
+\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set_of_list evs";
by (etac rev_mp 1);
@@ -394,9 +386,9 @@
(*** General properties of nonces ***)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+goal thy "!!evs. evs : yahalom lost ==> \
+\ length evs <= i --> \
+\ Nonce (newN i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
@@ -411,10 +403,10 @@
(*Variant: old messages must contain old nonces!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN evt) : parts {X}; \
-\ evs : yahalom lost \
-\ |] ==> length evt < length evs";
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN i) : parts {X}; \
+\ evs : yahalom lost \
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -427,11 +419,19 @@
val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
goal thy
- "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
+ "!!evs. evs : yahalom lost ==> \
+\ EX NA' A' B'. ALL NA A B. \
\ Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
\ --> B ~: lost --> NA = NA' & A = A' & B = B'";
-by (parts_induct_tac 1); (*100 seconds??*)
-by (simp_tac (!simpset addsimps [all_conj_distrib]) 1);
+by (etac yahalom.induct 1 THEN parts_Fake_tac);
+(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*)
+by (REPEAT (etac exE 2) THEN
+ best_tac (!claset addSIs [exI]
+ addDs [impOfSubs Fake_parts_insert]
+ addss (!simpset)) 2);
+(*Base case*)
+by (fast_tac (!claset addss (!simpset)) 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
(*YM2: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NB = ?y" 1);
by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
@@ -444,11 +444,7 @@
\ : parts (sees lost Spy evs); \
\ evs : yahalom lost; B ~: lost; B' ~: lost |] \
\ ==> NA' = NA & A' = A & B' = B";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
qed "unique_NB";
(*OLD VERSION
@@ -627,7 +623,7 @@
\ : set_of_list evs) | Nonce NB : analz (sees lost Spy evs)";
by (etac yahalom.induct 1);
by analz_Fake_tac;
-by (ALLGOALS (*28 seconds*)
+by (ALLGOALS (*22 seconds*)
(asm_simp_tac
(!simpset addsimps ([not_parts_not_analz,
analz_image_newK,
@@ -638,11 +634,10 @@
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*) (** LEVEL 4 **)
by (spy_analz_tac 1);
-(*YM1-YM3*) (*29 seconds*)
+(*YM1-YM3*) (*24 seconds*)
by (EVERY (map grind_tac [3,2,1]));
(*Oops*)
by (Full_simp_tac 2);
-by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2));
by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
by (grind_tac 2);
by (fast_tac (!claset delrules [bexI]
@@ -672,11 +667,11 @@
was distributed with that key. The more general form above is required
for the induction to carry through.*)
goal thy
- "!!evs. [| Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
-\ : set_of_list evs; \
-\ Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs)); \
-\ evs : yahalom lost |] \
+ "!!evs. [| Says Server A \
+\ {|Crypt (shrK A) {|Agent B, Key (newK i), na, Nonce NB'|}, X|} \
+\ : set_of_list evs; \
+\ Nonce NB : analz (insert (Key (newK i)) (sees lost Spy evs)); \
+\ evs : yahalom lost |] \
\ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
by (dtac Nonce_secrecy 1 THEN assume_tac 1);
--- a/src/HOL/Auth/Yahalom.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom.thy Thu Dec 19 11:58:39 1996 +0100
@@ -27,7 +27,8 @@
(*Alice initiates a protocol run*)
YM1 "[| evs: yahalom lost; A ~= B |]
- ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
+ ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs
+ : yahalom lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
@@ -35,7 +36,8 @@
Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says B Server
{|Agent B,
- Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
+ Crypt (shrK B)
+ {|Agent A, Nonce NA, Nonce (newN(length evs))|}|}
# evs : yahalom lost"
(*The Server receives Bob's message. He responds by sending a
@@ -45,9 +47,9 @@
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
: set_of_list evs |]
==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key (newK evs),
+ {|Crypt (shrK A) {|Agent B, Key (newK(length evs)),
Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
+ Crypt (shrK B) {|Agent A, Key (newK(length evs))|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and
--- a/src/HOL/Auth/Yahalom2.ML Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Thu Dec 19 11:58:39 1996 +0100
@@ -126,9 +126,8 @@
(*** Future keys can't be seen or used! ***)
(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= length evs' --> \
-\ Key (newK evs') ~: parts (sees lost Spy evs)";
+goal thy "!!i. evs : yahalom lost ==> \
+\ length evs <= i --> Key(newK i) ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
addDs [impOfSubs analz_subset_parts,
@@ -141,9 +140,9 @@
(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK evt) : parts {X}; \
+\ Key (newK i) : parts {X}; \
\ evs : yahalom lost \
-\ |] ==> length evt < length evs";
+\ |] ==> i < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
@@ -153,9 +152,8 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : yahalom lost ==> \
-\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!i. evs : yahalom lost ==> \
+\ length evs <= i --> newK i ~: keysFor(parts(sees lost Spy evs))";
by (parts_induct_tac 1);
by (dtac YM4_Key_parts_sees_Spy 5);
(*YM1, YM2 and YM3*)
@@ -189,7 +187,7 @@
"!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
\ : set_of_list evs; \
\ evs : yahalom lost |] \
-\ ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
+\ ==> (EX i. K = Key(newK i)) & A ~= B";
by (etac rev_mp 1);
by (etac yahalom.induct 1);
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
@@ -201,13 +199,13 @@
dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
assume_tac 7 THEN Full_simp_tac 7 THEN
- REPEAT ((eresolve_tac [bexE,conjE] ORELSE' hyp_subst_tac) 7);
+ REPEAT ((eresolve_tac [exE,conjE] ORELSE' hyp_subst_tac) 7);
(****
The following is to prove theorems of the form
- Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
+ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) ==>
Key K : analz (sees lost Spy evs)
A more general formula must be proved inductively.
@@ -223,10 +221,10 @@
by (etac yahalom.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 26 secs*)
+by (ALLGOALS (*Takes 11 secs*)
(asm_simp_tac
- (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
- @ pushes)
+ (!simpset addsimps [Un_assoc RS sym,
+ insert_Key_singleton, insert_Key_image, pushKey_newK]
setloop split_tac [expand_if])));
(*YM4, Fake*)
by (EVERY (map spy_analz_tac [4, 2]));
@@ -236,8 +234,8 @@
goal thy
"!!evs. evs : yahalom lost ==> \
-\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
-\ (K = newK evt | Key K : analz (sees lost Spy evs))";
+\ Key K : analz (insert (Key (newK i)) (sees lost Spy evs)) = \
+\ (K = newK i | Key K : analz (sees lost Spy evs))";
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
insert_Key_singleton]) 1);
by (Fast_tac 1);
@@ -273,11 +271,7 @@
\ : set_of_list evs; \
\ evs : yahalom lost |] \
\ ==> A=A' & B=B' & NA=NA' & NB=NB'";
-by (dtac lemma 1);
-by (REPEAT (etac exE 1));
-(*Duplicate the assumption*)
-by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
-by (fast_tac (!claset addSDs [spec]) 1);
+by (prove_unique_tac lemma 1);
qed "unique_session_keys";
@@ -296,8 +290,7 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz,
- analz_insert_Key_newK] @ pushes)
+ (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
setloop split_tac [expand_if])));
(*YM3*)
by (fast_tac (!claset addIs [parts_insertI]
--- a/src/HOL/Auth/Yahalom2.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Thu Dec 19 11:58:39 1996 +0100
@@ -31,13 +31,13 @@
(*Alice initiates a protocol run*)
YM1 "[| evs: yahalom lost; A ~= B |]
- ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom lost"
+ ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
YM2 "[| evs: yahalom lost; B ~= Server;
Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
- ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN evs)|}
+ ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
# evs : yahalom lost"
(*The Server receives Bob's message. He responds by sending a
@@ -48,8 +48,8 @@
: set_of_list evs |]
==> Says Server A
{|Nonce NB,
- Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
- Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
+ Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
+ Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
# evs : yahalom lost"
(*Alice receives the Server's (?) message, checks her Nonce, and