src/HOL/Auth/OtwayRees_AN.ML
changeset 2331 d6a56ff0d94e
parent 2284 80ebd1a213fd
child 2375 14539397fc04
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 06 10:47:10 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 06 10:49:15 1996 +0100
     1.3 @@ -18,10 +18,10 @@
     1.4  HOL_quantifiers := false;
     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 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
    1.13 +\        ==> EX K. EX NA. EX evs: otway lost.                                 \
    1.14  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    1.15  \             : set_of_list evs";
    1.16  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.17 @@ -120,8 +120,8 @@
    1.18  (*** Future keys can't be seen or used! ***)
    1.19  
    1.20  (*Nobody can have SEEN keys that will be generated in the future. *)
    1.21 -goal thy "!!evs. evs : otway lost ==> \
    1.22 -\                length evs <= length evs' --> \
    1.23 +goal thy "!!evs. evs : otway lost ==>             \
    1.24 +\                length evs <= length evs' -->    \
    1.25  \                Key (newK evs') ~: parts (sees lost Spy evs)";
    1.26  by (parts_induct_tac 1);
    1.27  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    1.28 @@ -147,7 +147,7 @@
    1.29  
    1.30  (*Nobody can have USED keys that will be generated in the future.
    1.31    ...very like new_keys_not_seen*)
    1.32 -goal thy "!!evs. evs : otway lost ==> \
    1.33 +goal thy "!!evs. evs : otway lost ==>          \
    1.34  \                length evs <= length evs' --> \
    1.35  \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
    1.36  by (parts_induct_tac 1);
    1.37 @@ -176,11 +176,11 @@
    1.38  (*Describes the form of K and NA when the Server sends this message.*)
    1.39  goal thy 
    1.40   "!!evs. [| Says Server B \
    1.41 -\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    1.42 +\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    1.43  \             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
    1.44 -\           evs : otway lost |]                                        \
    1.45 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
    1.46 -\            (EX i. NA = Nonce i) &                  \
    1.47 +\           evs : otway lost |]                                               \
    1.48 +\        ==> (EX evt: otway lost. K = Key(newK evt)) & \
    1.49 +\            (EX i. NA = Nonce i) &                    \
    1.50  \            (EX j. NB = Nonce j)";
    1.51  by (etac rev_mp 1);
    1.52  by (etac otway.induct 1);
    1.53 @@ -211,7 +211,7 @@
    1.54  
    1.55  (*The equality makes the induction hypothesis easier to apply*)
    1.56  goal thy  
    1.57 - "!!evs. evs : otway lost ==> \
    1.58 + "!!evs. evs : otway lost ==>                                         \
    1.59  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
    1.60  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
    1.61  by (etac otway.induct 1);
    1.62 @@ -231,7 +231,7 @@
    1.63  
    1.64  
    1.65  goal thy
    1.66 - "!!evs. evs : otway lost ==>                               \
    1.67 + "!!evs. evs : otway lost ==>                                          \
    1.68  \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
    1.69  \        (K = newK evt | Key K : analz (sees lost Spy evs))";
    1.70  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
    1.71 @@ -243,10 +243,10 @@
    1.72  (*** The Key K uniquely identifies the Server's  message. **)
    1.73  
    1.74  goal thy 
    1.75 - "!!evs. evs : otway lost ==>                      \
    1.76 + "!!evs. evs : otway lost ==>                              \
    1.77  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    1.78  \       Says Server B \
    1.79 -\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    1.80 +\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    1.81  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
    1.82  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.83  by (etac otway.induct 1);
    1.84 @@ -291,7 +291,7 @@
    1.85   "!!evs. [| A ~: lost;  evs : otway lost |]                 \
    1.86  \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
    1.87  \      : parts (sees lost Spy evs)                          \
    1.88 -\     --> (EX NB. Says Server B                                     \
    1.89 +\     --> (EX NB. Says Server B                                          \
    1.90  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    1.91  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    1.92  \                  : set_of_list evs)";
    1.93 @@ -318,7 +318,7 @@
    1.94  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.95                        addEs  partsEs
    1.96                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.97 -qed "A_trust_OR4";
    1.98 +qed "A_trusts_OR4";
    1.99  
   1.100  
   1.101  (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.102 @@ -407,4 +407,4 @@
   1.103  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.104                        addEs  partsEs
   1.105                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.106 -qed "B_trust_OR3";
   1.107 +qed "B_trusts_OR3";