src/HOL/Auth/OtwayRees.ML
changeset 2328 e984c12ce5b4
parent 2284 80ebd1a213fd
child 2375 14539397fc04
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Dec 05 19:03:38 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 06 10:36:31 1996 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  Pretty.setdepth 15;
     1.5  
     1.6  
     1.7 -(*Weak liveness: there are traces that reach the end*)
     1.8 +(*A "possibility property": there are traces that reach the end*)
     1.9  goal thy 
    1.10   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.11  \        ==> EX K. EX NA. EX evs: otway lost.          \
    1.12 @@ -364,9 +364,9 @@
    1.13    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
    1.14    over-simplified version of this protocol: see OtwayRees_Bad.*)
    1.15  goal thy 
    1.16 - "!!evs. [| A ~: lost;  evs : otway lost |]                            \
    1.17 + "!!evs. [| A ~: lost;  evs : otway lost |]                      \
    1.18  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
    1.19 -\             : parts (sees lost Spy evs) -->                       \
    1.20 +\             : parts (sees lost Spy evs) -->                    \
    1.21  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
    1.22  \             ~: parts (sees lost Spy evs)";
    1.23  by (parts_induct_tac 1);
    1.24 @@ -434,7 +434,7 @@
    1.25  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.26                        addEs  partsEs
    1.27                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.28 -qed "A_trust_OR4";
    1.29 +qed "A_trusts_OR4";
    1.30  
    1.31  
    1.32  (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
    1.33 @@ -590,10 +590,10 @@
    1.34  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
    1.35                        addEs  partsEs
    1.36                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.37 -qed "B_trust_OR3";
    1.38 +qed "B_trusts_OR3";
    1.39  
    1.40  
    1.41 -B_trust_OR3 RS Spy_not_see_encrypted_key;
    1.42 +B_trusts_OR3 RS Spy_not_see_encrypted_key;
    1.43  
    1.44  
    1.45  goal thy 
    1.46 @@ -624,6 +624,6 @@
    1.47  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
    1.48  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
    1.49  \            : set_of_list evs";
    1.50 -by (fast_tac (!claset addSDs  [A_trust_OR4]
    1.51 +by (fast_tac (!claset addSDs  [A_trusts_OR4]
    1.52                        addSEs [OR3_imp_OR2]) 1);
    1.53  qed "A_auths_B";