Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.
--- a/src/HOL/Auth/NS_Shared.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Tue Nov 05 11:20:52 1996 +0100
@@ -109,35 +109,23 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The length comparison, and Union over C, are essential for the
- induction! *)
-goal thy "!!evs. evs : ns_shared lost ==> \
+(*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') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*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 \
+\ evs : ns_shared lost \
\ |] ==> length evt < length evs";
by (rtac ccontr 1);
by (dtac leI 1);
@@ -147,38 +135,27 @@
-(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
+(*** Future nonces can't be seen or used! ***)
-goal thy "!!evs. evs : ns_shared lost ==> \
+goal thy "!!evs. evs : ns_shared lost ==> \
\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac ns_shared.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
- addcongs [disj_cong])));
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-val lemma = result();
-
-(*Variant needed below*)
-goal thy
- "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
+by (REPEAT_FIRST
+ (fast_tac (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un, Suc_leD]
+ addss (!simpset))));
+qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
(*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 ==> \
+goal thy "!!evs. evs : ns_shared lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: 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]));
@@ -196,13 +173,7 @@
by (ALLGOALS (deepen_tac (!claset addSDs [Says_imp_old_keys]
addIs [less_SucI, impOfSubs keysFor_mono]
addss (!simpset addsimps [le_def])) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : ns_shared lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,
--- a/src/HOL/Auth/OtwayRees.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Nov 05 11:20:52 1996 +0100
@@ -131,30 +131,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
+(*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') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -167,15 +156,12 @@
qed "Says_imp_old_keys";
-(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
+(*** Future nonces can't be seen or used! ***)
goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
- addcongs [disj_cong])));
+\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]
@@ -183,22 +169,14 @@
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
-(*Another 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";
+(*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";
by (rtac ccontr 1);
by (dtac leI 1);
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
@@ -208,9 +186,9 @@
(*Nobody can have USED keys that will be generated in the future.
...very like new_keys_not_seen*)
-goal thy "!!evs. evs : otway lost ==> \
+goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: 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]));
@@ -222,13 +200,7 @@
Suc_leD]
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,
@@ -283,12 +255,11 @@
by (etac otway.induct 1);
by analz_Fake_tac;
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (*Takes 22 secs*)
+by (ALLGOALS (*Takes 14 secs*)
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
-(** LEVEL 5 **)
(*OR4, OR2, Fake*)
by (EVERY (map spy_analz_tac [5,3,2]));
(*Oops, OR3, Base*)
--- a/src/HOL/Auth/OtwayRees_AN.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Nov 05 11:20:52 1996 +0100
@@ -119,30 +119,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
+(*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') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -155,15 +144,12 @@
qed "Says_imp_old_keys";
-(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
+(*** Future nonces can't be seen or used! ***)
goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
- addcongs [disj_cong])));
+\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
by (REPEAT_FIRST (fast_tac (!claset
addSEs partsEs
addSDs [Says_imp_sees_Spy RS parts.Inj]
@@ -171,14 +157,7 @@
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
@@ -186,7 +165,7 @@
...very like new_keys_not_seen*)
goal thy "!!evs. evs : otway lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: 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]));
@@ -198,13 +177,7 @@
Suc_leD]
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : otway lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,
--- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Nov 05 11:20:52 1996 +0100
@@ -131,30 +131,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
-goal thy "!!evs. evs : otway ==> \
+(*Nobody can have SEEN keys that will be generated in the future. *)
+goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
-\ Key (newK evs') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
+ impOfSubs parts_insert_subset_Un,
+ Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -167,35 +156,24 @@
qed "Says_imp_old_keys";
-(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
+(*** Future nonces can't be seen or used! ***)
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
-\ Nonce (newN evs') ~: (UN C. parts (sees lost C evs))";
-by (etac otway.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
- addcongs [disj_cong])));
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : otway; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+\ Nonce (newN evs') ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
+by (REPEAT_FIRST
+ (fast_tac (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un, Suc_leD]
+ addss (!simpset))));
+qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
-(*Another variant: old messages must contain old nonces!*)
+(*Variant: old messages must contain old nonces!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
+ "!!evs. [| Says A B X : set_of_list evs; \
\ Nonce (newN evt) : parts {X}; \
\ evs : otway \
\ |] ==> length evt < length evs";
@@ -210,7 +188,7 @@
...very like new_keys_not_seen*)
goal thy "!!evs. evs : otway ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: 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]));
@@ -222,13 +200,7 @@
Suc_leD]
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : otway; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,
--- a/src/HOL/Auth/Shared.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/Shared.ML Tue Nov 05 11:20:52 1996 +0100
@@ -155,7 +155,7 @@
qed "sees_subset_sees_Says";
(*Pushing Unions into parts. One of the agents A is B, and thus sees Y.
- Used to prove new_keys_not_seen.*)
+ Once used to prove new_keys_not_seen; now obsolete.*)
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
\ parts {Y} Un (UN A. parts (sees lost A evs))";
by (Step_tac 1);
@@ -202,7 +202,7 @@
by (ALLGOALS Fast_tac);
qed_spec_mp "seesD";
-Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Spy];
+Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
--- a/src/HOL/Auth/Yahalom.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Tue Nov 05 11:20:52 1996 +0100
@@ -118,30 +118,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
+(*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') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -168,31 +157,25 @@
...very like new_keys_not_seen*)
goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
-by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and YM4: these messages send unknown (X) components*)
-by (stac insert_commute 2);
-by (Simp_tac 2);
-(*YM4: the only way K could have been used is if it had been seen,
- contradicting new_keys_not_seen*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
+(*Fake and Oops: these messages send unknown (X) components*)
+by (EVERY
+ (map (fast_tac
+ (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
+ addss (!simpset))) [3,1]));
+(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
+by (fast_tac
+ (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
addEs [new_keys_not_seen RSN(2,rev_notE)]
- addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+ addDs [Suc_leD]) 1);
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,
@@ -413,31 +396,22 @@
goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evt --> \
-\ Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
-by (etac yahalom.induct 1);
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
- addcongs [disj_cong])));
-by (REPEAT_FIRST
- (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un, Suc_leD]
- addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> Nonce (newN evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_nonces_not_seen";
+\ Nonce (newN evt) ~: parts (sees lost Spy evs)";
+by (parts_induct_tac 1);
+by (REPEAT_FIRST (fast_tac (!claset
+ addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un,
+ Suc_leD]
+ addss (!simpset))));
+qed_spec_mp "new_nonces_not_seen";
Addsimps [new_nonces_not_seen];
-(*Another variant: old messages must contain old nonces!*)
+(*Variant: old messages must contain old nonces!*)
goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN evt) : parts {X}; \
+ "!!evs. [| Says A B X : set_of_list evs; \
+\ Nonce (newN evt) : parts {X}; \
\ evs : yahalom lost \
\ |] ==> length evt < length evs";
by (rtac ccontr 1);
--- a/src/HOL/Auth/Yahalom2.ML Mon Nov 04 17:23:37 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Tue Nov 05 11:20:52 1996 +0100
@@ -126,30 +126,19 @@
(*** Future keys can't be seen or used! ***)
-(*Nobody can have SEEN keys that will be generated in the future.
- This has to be proved anew for each protocol description,
- but should go by similar reasoning every time. Hardest case is the
- standard Fake rule.
- The Union over C is essential for the induction! *)
+(*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') ~: (UN C. parts (sees lost C evs))";
+\ Key (newK evs') ~: parts (sees lost Spy evs)";
by (parts_induct_tac 1);
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un,
Suc_leD]
addss (!simpset))));
-val lemma = result();
-
-(*Variant needed for the main theorem below*)
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> Key (newK evs') ~: parts (sees lost C evs)";
-by (fast_tac (!claset addDs [lemma]) 1);
-qed "new_keys_not_seen";
+qed_spec_mp "new_keys_not_seen";
Addsimps [new_keys_not_seen];
-(*Another variant: old messages must contain old keys!*)
+(*Variant: old messages must contain old keys!*)
goal thy
"!!evs. [| Says A B X : set_of_list evs; \
\ Key (newK evt) : parts {X}; \
@@ -166,31 +155,26 @@
...very like new_keys_not_seen*)
goal thy "!!evs. evs : yahalom lost ==> \
\ length evs <= length evs' --> \
-\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
+\ newK evs' ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
by (dresolve_tac [YM4_Key_parts_sees_Spy] 5);
(*YM1, YM2 and YM3*)
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
-(*Fake and YM4: these messages send unknown (X) components*)
-by (stac insert_commute 2);
-by (Simp_tac 2);
-(*YM4: the only way K could have been used is if it had been seen,
- contradicting new_keys_not_seen*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
+(*Fake and Oops: these messages send unknown (X) components*)
+by (EVERY
+ (map (fast_tac
+ (!claset addDs [impOfSubs analz_subset_parts,
+ impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono),
+ Suc_leD]
+ addss (!simpset))) [3,1]));
+(*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
+by (fast_tac
+ (!claset addSEs partsEs
+ addSDs [Says_imp_sees_Spy RS parts.Inj]
addEs [new_keys_not_seen RSN(2,rev_notE)]
- addss (!simpset)) 1));
-val lemma = result();
-
-goal thy
- "!!evs. [| evs : yahalom lost; length evs <= length evs' |] \
-\ ==> newK evs' ~: keysFor (parts (sees lost C evs))";
-by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
-qed "new_keys_not_used";
+ addDs [Suc_leD]) 1);
+qed_spec_mp "new_keys_not_used";
bind_thm ("new_keys_not_analzd",
[analz_subset_parts RS keysFor_mono,