src/HOL/Auth/OtwayRees.ML
changeset 3543 82f33248d89d
parent 3519 ab0a9fbed4c0
child 3674 65ec38fbb265
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:23:03 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:26:02 1997 +0200
     1.3 @@ -209,10 +209,8 @@
     1.4  val lemma = result();
     1.5  
     1.6  goal thy 
     1.7 - "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
     1.8 -\            : set evs;                                            \ 
     1.9 -\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    1.10 -\            : set evs;                                            \
    1.11 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    1.12 +\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
    1.13  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    1.14  by (prove_unique_tac lemma 1);
    1.15  qed "unique_session_keys";
    1.16 @@ -277,8 +275,8 @@
    1.17  (*Crucial property: If the encrypted message appears, and A has used NA
    1.18    to start a run, then it originated with the Server!*)
    1.19  goal thy 
    1.20 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
    1.21 -\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
    1.22 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                      \
    1.23 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)           \
    1.24  \        --> Says A B {|NA, Agent A, Agent B,                          \
    1.25  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    1.26  \             : set evs -->                                            \
    1.27 @@ -295,8 +293,8 @@
    1.28  (*OR4*)
    1.29  by (REPEAT (Safe_step_tac 2));
    1.30  by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
    1.31 -by (fast_tac (!claset addSIs [Crypt_imp_OR1]
    1.32 -                      addEs  sees_Spy_partsEs) 2);
    1.33 +by (blast_tac (!claset addSIs [Crypt_imp_OR1]
    1.34 +                       addEs  sees_Spy_partsEs) 2);
    1.35  (*OR3*)  (** LEVEL 5 **)
    1.36  by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
    1.37  by (step_tac (!claset delrules [disjCI, impCE]) 1);