Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tidying up: removing redundant assumptions, etc.
authorpaulson
Thu, 07 Nov 1996 10:19:15 +0100
changeset 2166 d276a806cc10
parent 2165 63dfe7f19cad
child 2167 5819e85ad261
Tidying up: removing redundant assumptions, etc.
src/HOL/Auth/OtwayRees.ML file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayRees_AN.ML file | annotate | diff | comparison | revisions
src/HOL/Auth/OtwayRees_Bad.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/OtwayRees.ML	Thu Nov 07 10:15:57 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 07 10:19:15 1996 +0100
@@ -440,7 +440,7 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
 \        ==> Says Server B                                                 \
 \              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
 \                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
@@ -454,8 +454,7 @@
                           analz_insert_Key_newK] @ pushes)
                setloop split_tac [expand_if])));
 (*OR3*)
-by (fast_tac (!claset addSIs [parts_insertI]
-                      addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
                       addss (!simpset addsimps [parts_insert2])) 3);
 (*OR4, OR2, Fake*) 
 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
--- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 07 10:15:57 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 07 10:19:15 1996 +0100
@@ -144,23 +144,6 @@
 qed "Says_imp_old_keys";
 
 
-(*** 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)";
-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 : otway lost ==> \
@@ -342,7 +325,7 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
 \        ==> Says Server B                                                 \
 \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
 \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
@@ -357,8 +340,7 @@
                           analz_insert_Key_newK] @ pushes)
                setloop split_tac [expand_if])));
 (*OR3*)
-by (fast_tac (!claset addSIs [parts_insertI]
-                      addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
                       addss (!simpset addsimps [parts_insert2])) 2);
 (*OR4, Fake*) 
 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 07 10:15:57 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 07 10:19:15 1996 +0100
@@ -325,12 +325,12 @@
 
 (*Crucial security property, but not itself enough to guarantee correctness!*)
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway;  evt : otway |]        \
-\    ==> Says Server B \
-\          {|NA, Crypt {|NA, Key K|} (shrK A), \
-\            Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
-\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
-\        Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
+\        ==> Says Server B                                            \
+\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
+\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
+\            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by analz_Fake_tac;
 by (ALLGOALS
@@ -339,8 +339,7 @@
                           analz_insert_Key_newK] @ pushes)
                setloop split_tac [expand_if])));
 (*OR3*)
-by (fast_tac (!claset addSIs [parts_insertI]
-                      addEs [Says_imp_old_keys RS less_irrefl]
+by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
                       addss (!simpset addsimps [parts_insert2])) 3);
 (*OR4, OR2, Fake*) 
 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
isabelle