Weaking of injectivity assumptions for newK and newN:
authorpaulson
Thu Nov 28 10:41:14 1996 +0100 (1996-11-28)
changeset 2264f298678bd54a
parent 2263 c741309167bf
child 2265 3123fef88dce
Weaking of injectivity assumptions for newK and newN:
they are no longer assumed injective over all traces, merely over the
length of a trace
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Wed Nov 27 20:36:33 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Nov 28 10:41:14 1996 +0100
     1.3 @@ -114,7 +114,8 @@
     1.4  \                length evs <= length evs' --> \
     1.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     1.6  by (parts_induct_tac 1);
     1.7 -by (ALLGOALS (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
     1.8 +by (ALLGOALS (fast_tac (!claset addEs [leD RS notE]
     1.9 +				addDs [impOfSubs analz_subset_parts,
    1.10                                         impOfSubs parts_insert_subset_Un,
    1.11                                         Suc_leD]
    1.12                                  addss (!simpset))));
    1.13 @@ -144,7 +145,8 @@
    1.14  by (REPEAT_FIRST
    1.15      (fast_tac (!claset addSEs partsEs
    1.16                         addSDs  [Says_imp_sees_Spy RS parts.Inj]
    1.17 -                       addDs  [impOfSubs analz_subset_parts,
    1.18 +                       addEs [leD RS notE]
    1.19 +				addDs  [impOfSubs analz_subset_parts,
    1.20                                 impOfSubs parts_insert_subset_Un, Suc_leD]
    1.21                         addss (!simpset))));
    1.22  qed_spec_mp "new_nonces_not_seen";
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Nov 27 20:36:33 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 28 10:41:14 1996 +0100
     2.3 @@ -136,7 +136,8 @@
     2.4  \                length evs <= length evs' --> \
     2.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     2.6  by (parts_induct_tac 1);
     2.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     2.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     2.9 +				    addDs [impOfSubs analz_subset_parts,
    2.10                                             impOfSubs parts_insert_subset_Un,
    2.11                                             Suc_leD]
    2.12                                      addss (!simpset))));
    2.13 @@ -165,7 +166,8 @@
    2.14  by (REPEAT_FIRST (fast_tac (!claset 
    2.15                                addSEs partsEs
    2.16                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    2.17 -                              addDs  [impOfSubs analz_subset_parts,
    2.18 +                              addEs [leD RS notE]
    2.19 +			      addDs  [impOfSubs analz_subset_parts,
    2.20                                        impOfSubs parts_insert_subset_Un,
    2.21                                        Suc_leD]
    2.22                                addss (!simpset))));
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Nov 27 20:36:33 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 28 10:41:14 1996 +0100
     3.3 @@ -124,7 +124,8 @@
     3.4  \                length evs <= length evs' --> \
     3.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     3.6  by (parts_induct_tac 1);
     3.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     3.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     3.9 +				    addDs [impOfSubs analz_subset_parts,
    3.10                                             impOfSubs parts_insert_subset_Un,
    3.11                                             Suc_leD]
    3.12                                      addss (!simpset))));
    3.13 @@ -135,7 +136,7 @@
    3.14  goal thy 
    3.15   "!!evs. [| Says A B X : set_of_list evs;  \
    3.16  \           Key (newK evt) : parts {X};    \
    3.17 -\           evs : otway lost                 \
    3.18 +\           evs : otway lost               \
    3.19  \        |] ==> length evt < length evs";
    3.20  by (rtac ccontr 1);
    3.21  by (dtac leI 1);
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed Nov 27 20:36:33 1996 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 28 10:41:14 1996 +0100
     4.3 @@ -136,7 +136,8 @@
     4.4  \                length evs <= length evs' --> \
     4.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     4.6  by (parts_induct_tac 1);
     4.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     4.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     4.9 +				    addDs [impOfSubs analz_subset_parts,
    4.10  					   impOfSubs parts_insert_subset_Un,
    4.11  					   Suc_leD]
    4.12                                  addss (!simpset))));
    4.13 @@ -165,6 +166,7 @@
    4.14  by (REPEAT_FIRST
    4.15      (fast_tac (!claset addSEs partsEs
    4.16  	               addSDs  [Says_imp_sees_Spy RS parts.Inj]
    4.17 +		       addEs [leD RS notE]
    4.18  		       addDs  [impOfSubs analz_subset_parts,
    4.19  			       impOfSubs parts_insert_subset_Un, Suc_leD]
    4.20  		       addss (!simpset))));
     5.1 --- a/src/HOL/Auth/Shared.ML	Wed Nov 27 20:36:33 1996 +0100
     5.2 +++ b/src/HOL/Auth/Shared.ML	Thu Nov 28 10:41:14 1996 +0100
     5.3 @@ -56,7 +56,8 @@
     5.4  
     5.5  
     5.6  (*Injectiveness and freshness of new keys and nonces*)
     5.7 -AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
     5.8 +AddIffs [inj_shrK RS inj_eq];
     5.9 +AddSDs  [newN_length, newK_length];
    5.10  
    5.11  (** Rewrites should not refer to  initState(Friend i) 
    5.12      -- not in normal form! **)
     6.1 --- a/src/HOL/Auth/Shared.thy	Wed Nov 27 20:36:33 1996 +0100
     6.2 +++ b/src/HOL/Auth/Shared.thy	Thu Nov 28 10:41:14 1996 +0100
     6.3 @@ -54,9 +54,9 @@
     6.4  rules
     6.5    inj_shrK      "inj shrK"
     6.6  
     6.7 -  inj_newN      "inj newN"
     6.8 +  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
     6.9 +  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
    6.10  
    6.11 -  inj_newK      "inj newK"
    6.12    newK_neq_shrK "newK evs ~= shrK A" 
    6.13    isSym_newK    "isSymKey (newK evs)"
    6.14  
     7.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Nov 27 20:36:33 1996 +0100
     7.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Nov 28 10:41:14 1996 +0100
     7.3 @@ -123,7 +123,8 @@
     7.4  \                length evs <= length evs' --> \
     7.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     7.6  by (parts_induct_tac 1);
     7.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     7.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     7.9 +				    addDs [impOfSubs analz_subset_parts,
    7.10                                             impOfSubs parts_insert_subset_Un,
    7.11                                             Suc_leD]
    7.12                                      addss (!simpset))));
     8.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 27 20:36:33 1996 +0100
     8.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Nov 28 10:41:14 1996 +0100
     8.3 @@ -131,7 +131,8 @@
     8.4  \                length evs <= length evs' --> \
     8.5  \                Key (newK evs') ~: parts (sees lost Spy evs)";
     8.6  by (parts_induct_tac 1);
     8.7 -by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
     8.8 +by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
     8.9 +				    addDs [impOfSubs analz_subset_parts,
    8.10                                             impOfSubs parts_insert_subset_Un,
    8.11                                             Suc_leD]
    8.12                                      addss (!simpset))));