src/HOL/Auth/OtwayRees_AN.ML
changeset 3516 470626799511
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 11 13:30:01 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 11 13:32:39 1997 +0200
     1.3 @@ -32,15 +32,6 @@
     1.4  
     1.5  (**** Inductive proofs about otway ****)
     1.6  
     1.7 -(*Monotonicity*)
     1.8 -goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
     1.9 -by (rtac subsetI 1);
    1.10 -by (etac otway.induct 1);
    1.11 -by (REPEAT_FIRST
    1.12 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.13 -                              :: otway.intrs))));
    1.14 -qed "otway_mono";
    1.15 -
    1.16  (*Nobody sends themselves messages*)
    1.17  goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    1.18  by (etac otway.induct 1);
    1.19 @@ -311,22 +302,6 @@
    1.20  qed "Spy_not_see_encrypted_key";
    1.21  
    1.22  
    1.23 -goal thy 
    1.24 - "!!evs. [| C ~: {A,B,Server};                                      \
    1.25 -\           Says Server B                                           \
    1.26 -\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.27 -\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.28 -\             : set evs;                                            \
    1.29 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    1.30 -\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
    1.31 -\        ==> Key K ~: analz (sees lost C evs)";
    1.32 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    1.33 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    1.34 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    1.35 -by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
    1.36 -qed "Agent_not_see_encrypted_key";
    1.37 -
    1.38 -
    1.39  (**** Authenticity properties relating to NB ****)
    1.40  
    1.41  (*If the encrypted message appears then it originated with the Server!*)