Tidying up: removing redundant assumptions, etc.
authorpaulson
Thu Nov 07 10:19:15 1996 +0100 (1996-11-07)
changeset 2166d276a806cc10
parent 2165 63dfe7f19cad
child 2167 5819e85ad261
Tidying up: removing redundant assumptions, etc.
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Nov 07 10:15:57 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 07 10:19:15 1996 +0100
     1.3 @@ -440,7 +440,7 @@
     1.4      the premises, e.g. by having A=Spy **)
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
     1.8 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
     1.9  \        ==> Says Server B                                                 \
    1.10  \              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
    1.11  \                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
    1.12 @@ -454,8 +454,7 @@
    1.13                            analz_insert_Key_newK] @ pushes)
    1.14                 setloop split_tac [expand_if])));
    1.15  (*OR3*)
    1.16 -by (fast_tac (!claset addSIs [parts_insertI]
    1.17 -                      addEs [Says_imp_old_keys RS less_irrefl]
    1.18 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.19                        addss (!simpset addsimps [parts_insert2])) 3);
    1.20  (*OR4, OR2, Fake*) 
    1.21  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 07 10:15:57 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Nov 07 10:19:15 1996 +0100
     2.3 @@ -144,23 +144,6 @@
     2.4  qed "Says_imp_old_keys";
     2.5  
     2.6  
     2.7 -(*** Future nonces can't be seen or used! ***)
     2.8 -
     2.9 -goal thy "!!evs. evs : otway lost ==> \
    2.10 -\                length evs <= length evt --> \
    2.11 -\                Nonce (newN evt) ~: parts (sees lost Spy evs)";
    2.12 -by (parts_induct_tac 1);
    2.13 -by (REPEAT_FIRST (fast_tac (!claset 
    2.14 -                              addSEs partsEs
    2.15 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
    2.16 -                              addDs  [impOfSubs analz_subset_parts,
    2.17 -                                      impOfSubs parts_insert_subset_Un,
    2.18 -                                      Suc_leD]
    2.19 -                              addss (!simpset))));
    2.20 -qed_spec_mp "new_nonces_not_seen";
    2.21 -Addsimps [new_nonces_not_seen];
    2.22 -
    2.23 -
    2.24  (*Nobody can have USED keys that will be generated in the future.
    2.25    ...very like new_keys_not_seen*)
    2.26  goal thy "!!evs. evs : otway lost ==> \
    2.27 @@ -342,7 +325,7 @@
    2.28      the premises, e.g. by having A=Spy **)
    2.29  
    2.30  goal thy 
    2.31 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
    2.32 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
    2.33  \        ==> Says Server B                                                 \
    2.34  \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
    2.35  \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
    2.36 @@ -357,8 +340,7 @@
    2.37                            analz_insert_Key_newK] @ pushes)
    2.38                 setloop split_tac [expand_if])));
    2.39  (*OR3*)
    2.40 -by (fast_tac (!claset addSIs [parts_insertI]
    2.41 -                      addEs [Says_imp_old_keys RS less_irrefl]
    2.42 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    2.43                        addss (!simpset addsimps [parts_insert2])) 2);
    2.44  (*OR4, Fake*) 
    2.45  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
     3.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 07 10:15:57 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Nov 07 10:19:15 1996 +0100
     3.3 @@ -325,12 +325,12 @@
     3.4  
     3.5  (*Crucial security property, but not itself enough to guarantee correctness!*)
     3.6  goal thy 
     3.7 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway;  evt : otway |]        \
     3.8 -\    ==> Says Server B \
     3.9 -\          {|NA, Crypt {|NA, Key K|} (shrK A), \
    3.10 -\            Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
    3.11 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
    3.12 -\        Key K ~: analz (sees lost Spy evs)";
    3.13 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
    3.14 +\        ==> Says Server B                                            \
    3.15 +\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
    3.16 +\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
    3.17 +\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
    3.18 +\            Key K ~: analz (sees lost Spy evs)";
    3.19  by (etac otway.induct 1);
    3.20  by analz_Fake_tac;
    3.21  by (ALLGOALS
    3.22 @@ -339,8 +339,7 @@
    3.23                            analz_insert_Key_newK] @ pushes)
    3.24                 setloop split_tac [expand_if])));
    3.25  (*OR3*)
    3.26 -by (fast_tac (!claset addSIs [parts_insertI]
    3.27 -                      addEs [Says_imp_old_keys RS less_irrefl]
    3.28 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    3.29                        addss (!simpset addsimps [parts_insert2])) 3);
    3.30  (*OR4, OR2, Fake*) 
    3.31  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));