Swapped arguments of Crypt (for clarity and because it is conventional)
authorpaulson
Fri Nov 29 18:03:21 1996 +0100 (1996-11-29)
changeset 228480ebd1a213fd
parent 2283 68829cf138fc
child 2285 b239c202c91f
Swapped arguments of Crypt (for clarity and because it is conventional)
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Nov 29 17:58:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Nov 29 18:03:21 1996 +0100
     1.3 @@ -58,9 +58,8 @@
     1.4  qed "keysFor_insert_MPair";
     1.5  
     1.6  goalw thy [keysFor_def]
     1.7 -    "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
     1.8 +    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
     1.9  by (Auto_tac());
    1.10 -by (Fast_tac 1);
    1.11  qed "keysFor_insert_Crypt";
    1.12  
    1.13  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    1.14 @@ -68,7 +67,7 @@
    1.15            keysFor_insert_Key, keysFor_insert_MPair,
    1.16            keysFor_insert_Crypt];
    1.17  
    1.18 -goalw thy [keysFor_def] "!!H. Crypt X K : H ==> invKey K : keysFor H";
    1.19 +goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.20  by (Fast_tac 1);
    1.21  qed "Crypt_imp_invKey_keysFor";
    1.22  
    1.23 @@ -234,8 +233,8 @@
    1.24  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.25  qed "parts_insert_Key";
    1.26  
    1.27 -goal thy "parts (insert (Crypt X K) H) = \
    1.28 -\         insert (Crypt X K) (parts (insert X H))";
    1.29 +goal thy "parts (insert (Crypt K X) H) = \
    1.30 +\         insert (Crypt K X) (parts (insert X H))";
    1.31  by (rtac equalityI 1);
    1.32  by (rtac subsetI 1);
    1.33  by (etac parts.induct 1);
    1.34 @@ -378,8 +377,8 @@
    1.35  
    1.36  (*Can pull out enCrypted message if the Key is not known*)
    1.37  goal thy "!!H. Key (invKey K) ~: analz H ==>  \
    1.38 -\              analz (insert (Crypt X K) H) = \
    1.39 -\              insert (Crypt X K) (analz H)";
    1.40 +\              analz (insert (Crypt K X) H) = \
    1.41 +\              insert (Crypt K X) (analz H)";
    1.42  by (rtac (analz_insert RSN (2, equalityI)) 1);
    1.43  by (rtac subsetI 1);
    1.44  by (etac analz.induct 1);
    1.45 @@ -387,16 +386,16 @@
    1.46  qed "analz_insert_Crypt";
    1.47  
    1.48  goal thy "!!H. Key (invKey K) : analz H ==>  \
    1.49 -\              analz (insert (Crypt X K) H) <= \
    1.50 -\              insert (Crypt X K) (analz (insert X H))";
    1.51 +\              analz (insert (Crypt K X) H) <= \
    1.52 +\              insert (Crypt K X) (analz (insert X H))";
    1.53  by (rtac subsetI 1);
    1.54  by (eres_inst_tac [("za","x")] analz.induct 1);
    1.55  by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.56  val lemma1 = result();
    1.57  
    1.58  goal thy "!!H. Key (invKey K) : analz H ==>  \
    1.59 -\              insert (Crypt X K) (analz (insert X H)) <= \
    1.60 -\              analz (insert (Crypt X K) H)";
    1.61 +\              insert (Crypt K X) (analz (insert X H)) <= \
    1.62 +\              analz (insert (Crypt K X) H)";
    1.63  by (Auto_tac());
    1.64  by (eres_inst_tac [("za","x")] analz.induct 1);
    1.65  by (Auto_tac());
    1.66 @@ -405,19 +404,19 @@
    1.67  val lemma2 = result();
    1.68  
    1.69  goal thy "!!H. Key (invKey K) : analz H ==>  \
    1.70 -\              analz (insert (Crypt X K) H) = \
    1.71 -\              insert (Crypt X K) (analz (insert X H))";
    1.72 +\              analz (insert (Crypt K X) H) = \
    1.73 +\              insert (Crypt K X) (analz (insert X H))";
    1.74  by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
    1.75  qed "analz_insert_Decrypt";
    1.76  
    1.77  (*Case analysis: either the message is secure, or it is not!
    1.78    Effective, but can cause subgoals to blow up!
    1.79    Use with expand_if;  apparently split_tac does not cope with patterns
    1.80 -  such as "analz (insert (Crypt X K) H)" *)
    1.81 -goal thy "analz (insert (Crypt X K) H) =                \
    1.82 +  such as "analz (insert (Crypt K X) H)" *)
    1.83 +goal thy "analz (insert (Crypt K X) H) =                \
    1.84  \         (if (Key (invKey K) : analz H)                \
    1.85 -\          then insert (Crypt X K) (analz (insert X H)) \
    1.86 -\          else insert (Crypt X K) (analz H))";
    1.87 +\          then insert (Crypt K X) (analz (insert X H)) \
    1.88 +\          else insert (Crypt K X) (analz H))";
    1.89  by (case_tac "Key (invKey K)  : analz H " 1);
    1.90  by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
    1.91                                                 analz_insert_Decrypt])));
    1.92 @@ -428,8 +427,8 @@
    1.93            analz_Crypt_if];
    1.94  
    1.95  (*This rule supposes "for the sake of argument" that we have the key.*)
    1.96 -goal thy  "analz (insert (Crypt X K) H) <=  \
    1.97 -\          insert (Crypt X K) (analz (insert X H))";
    1.98 +goal thy  "analz (insert (Crypt K X) H) <=  \
    1.99 +\          insert (Crypt K X) (analz (insert X H))";
   1.100  by (rtac subsetI 1);
   1.101  by (etac analz.induct 1);
   1.102  by (Auto_tac());
   1.103 @@ -496,7 +495,7 @@
   1.104  qed "analz_insert_cong";
   1.105  
   1.106  (*If there are no pairs or encryptions then analz does nothing*)
   1.107 -goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
   1.108 +goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
   1.109  \         analz H = H";
   1.110  by (Step_tac 1);
   1.111  by (etac analz.induct 1);
   1.112 @@ -528,7 +527,7 @@
   1.113  val Nonce_synth = mk_cases "Nonce n : synth H";
   1.114  val Key_synth   = mk_cases "Key K : synth H";
   1.115  val MPair_synth = mk_cases "{|X,Y|} : synth H";
   1.116 -val Crypt_synth = mk_cases "Crypt X K : synth H";
   1.117 +val Crypt_synth = mk_cases "Crypt K X : synth H";
   1.118  
   1.119  AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
   1.120  
   1.121 @@ -589,7 +588,7 @@
   1.122  by (Fast_tac 1);
   1.123  qed "Key_synth_eq";
   1.124  
   1.125 -goal thy "!!K. Key K ~: H ==> (Crypt X K : synth H) = (Crypt X K: H)";
   1.126 +goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)";
   1.127  by (Fast_tac 1);
   1.128  qed "Crypt_synth_eq";
   1.129  
   1.130 @@ -660,9 +659,9 @@
   1.131  qed "Fake_parts_insert";
   1.132  
   1.133  goal thy
   1.134 -     "!!H. [| Crypt Y K : parts (insert X H);  X: synth (analz G);  \
   1.135 +     "!!H. [| Crypt K Y : parts (insert X H);  X: synth (analz G);  \
   1.136  \             Key K ~: analz G |]                                   \
   1.137 -\          ==> Crypt Y K : parts G Un parts H";
   1.138 +\          ==> Crypt K Y : parts G Un parts H";
   1.139  by (dtac (impOfSubs Fake_parts_insert) 1);
   1.140  by (assume_tac 1);
   1.141  by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.142 @@ -699,7 +698,7 @@
   1.143  AddIffs [MPair_synth_analz];
   1.144  
   1.145  goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
   1.146 -\              ==> (Crypt X K : synth (analz H)) = (X : synth (analz H))";
   1.147 +\              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   1.148  by (Fast_tac 1);
   1.149  qed "Crypt_synth_analz";
   1.150  
     2.1 --- a/src/HOL/Auth/Message.thy	Fri Nov 29 17:58:18 1996 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Fri Nov 29 18:03:21 1996 +0100
     2.3 @@ -28,10 +28,10 @@
     2.4    isSymKey :: key=>bool
     2.5    "isSymKey K == (invKey K = K)"
     2.6  
     2.7 -  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
     2.8 -    because Crypt is a constructor!  We assume that encryption is injective,
     2.9 +  (*We do not assume  Crypt (invKey K) (Crypt K X) = X
    2.10 +    because Crypt a is constructor!  We assume that encryption is injective,
    2.11      which is not true in the real world.  The alternative is to take
    2.12 -    Crypt as an uninterpreted function symbol satisfying the equation
    2.13 +    Crypt an as uninterpreted function symbol satisfying the equation
    2.14      above.  This seems to require moving to ZF and regarding msg as an
    2.15      inductive definition instead of a datatype.*) 
    2.16  
    2.17 @@ -43,7 +43,7 @@
    2.18        | Nonce nat
    2.19        | Key   key
    2.20        | MPair msg msg
    2.21 -      | Crypt msg key
    2.22 +      | Crypt key msg
    2.23  
    2.24  (*Allows messages of the form {|A,B,NA|}, etc...*)
    2.25  syntax
    2.26 @@ -56,7 +56,7 @@
    2.27  
    2.28  constdefs  (*Keys useful to decrypt elements of a message set*)
    2.29    keysFor :: msg set => key set
    2.30 -  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
    2.31 +  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    2.32  
    2.33  (** Inductive definition of all "parts" of a message.  **)
    2.34  
    2.35 @@ -66,7 +66,7 @@
    2.36      Inj     "X: H ==> X: parts H"
    2.37      Fst     "{|X,Y|} : parts H ==> X : parts H"
    2.38      Snd     "{|X,Y|} : parts H ==> Y : parts H"
    2.39 -    Body    "Crypt X K : parts H ==> X : parts H"
    2.40 +    Body    "Crypt K X : parts H ==> X : parts H"
    2.41  
    2.42  
    2.43  (** Inductive definition of "analz" -- what can be broken down from a set of
    2.44 @@ -79,7 +79,7 @@
    2.45      Inj     "X: H ==> X: analz H"
    2.46      Fst     "{|X,Y|} : analz H ==> X : analz H"
    2.47      Snd     "{|X,Y|} : analz H ==> Y : analz H"
    2.48 -    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
    2.49 +    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
    2.50  
    2.51  
    2.52  (** Inductive definition of "synth" -- what can be built up from a set of
    2.53 @@ -92,6 +92,6 @@
    2.54      Inj     "X: H ==> X: synth H"
    2.55      Agent   "Agent agt : synth H"
    2.56      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    2.57 -    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H"
    2.58 +    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
    2.59  
    2.60  end
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Nov 29 17:58:18 1996 +0100
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Nov 29 18:03:21 1996 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4  goal thy 
     3.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     3.6  \        ==> EX N K. EX evs: ns_shared lost.          \
     3.7 -\               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
     3.8 +\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
     3.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.10  by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2);
    3.11  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    3.12 @@ -50,14 +50,14 @@
    3.13  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    3.14  
    3.15  (*For reasoning about the encrypted portion of message NS3*)
    3.16 -goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \
    3.17 +goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
    3.18  \                ==> X : parts (sees lost Spy evs)";
    3.19  by (fast_tac (!claset addSEs partsEs
    3.20                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    3.21  qed "NS3_msg_in_parts_sees_Spy";
    3.22                                
    3.23  goal thy
    3.24 -    "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs \
    3.25 +    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
    3.26  \           ==> K : parts (sees lost Spy evs)";
    3.27  by (fast_tac (!claset addSEs partsEs
    3.28                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    3.29 @@ -188,11 +188,11 @@
    3.30  
    3.31  (*Describes the form of K, X and K' when the Server sends this message.*)
    3.32  goal thy 
    3.33 - "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
    3.34 + "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
    3.35  \           evs : ns_shared lost |]    \
    3.36  \        ==> (EX evt: ns_shared lost. \
    3.37  \                  K = Key(newK evt) & \
    3.38 -\                  X = (Crypt {|K, Agent A|} (shrK B)) & \
    3.39 +\                  X = (Crypt (shrK B) {|K, Agent A|}) & \
    3.40  \                  K' = shrK A)";
    3.41  by (etac rev_mp 1);
    3.42  by (etac ns_shared.induct 1);
    3.43 @@ -202,13 +202,13 @@
    3.44  
    3.45  (*If the encrypted message appears then it originated with the Server*)
    3.46  goal thy
    3.47 - "!!evs. [| Crypt {|NA, Agent B, Key K, X|} (shrK A)                   \
    3.48 + "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
    3.49  \            : parts (sees lost Spy evs);                              \
    3.50  \           A ~: lost;  evs : ns_shared lost |]                        \
    3.51 -\         ==> X = (Crypt {|Key K, Agent A|} (shrK B)) &                \
    3.52 +\         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
    3.53  \             Says Server A                                            \
    3.54 -\              (Crypt {|NA, Agent B, Key K,                            \
    3.55 -\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
    3.56 +\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
    3.57 +\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
    3.58  \             : set_of_list evs";
    3.59  by (etac rev_mp 1);
    3.60  by (parts_induct_tac 1);
    3.61 @@ -220,11 +220,11 @@
    3.62    OR     reduces it to the Fake case.
    3.63    Use Says_Server_message_form if applicable.*)
    3.64  goal thy 
    3.65 - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))      \
    3.66 + "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    3.67  \            : set_of_list evs;  evs : ns_shared lost |]                   \
    3.68  \        ==> (EX evt: ns_shared lost. K = newK evt &                       \
    3.69  \                               length evt < length evs &                  \
    3.70 -\                               X = (Crypt {|Key K, Agent A|} (shrK B)))   \
    3.71 +\                               X = (Crypt (shrK B) {|Key K, Agent A|}))   \
    3.72  \          | X : analz (sees lost Spy evs)";
    3.73  by (case_tac "A : lost" 1);
    3.74  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    3.75 @@ -261,7 +261,7 @@
    3.76    We require that agents should behave like this subsequently also.*)
    3.77  goal thy 
    3.78   "!!evs. evs : ns_shared lost ==> \
    3.79 -\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
    3.80 +\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
    3.81  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    3.82  by (etac ns_shared.induct 1);
    3.83  by parts_Fake_tac;
    3.84 @@ -314,7 +314,7 @@
    3.85  goal thy 
    3.86   "!!evs. evs : ns_shared lost ==>                                            \
    3.87  \      EX A' NA' B' X'. ALL A NA B X.                                        \
    3.88 -\       Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))         \
    3.89 +\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
    3.90  \       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
    3.91  by (etac ns_shared.induct 1);
    3.92  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    3.93 @@ -333,10 +333,10 @@
    3.94  (*In messages of this form, the session key uniquely identifies the rest*)
    3.95  goal thy 
    3.96   "!!evs. [| Says Server A                                    \
    3.97 -\             (Crypt {|NA, Agent B, Key K, X|} (shrK A))     \
    3.98 +\             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
    3.99  \                  : set_of_list evs;                        \ 
   3.100  \           Says Server A'                                   \
   3.101 -\             (Crypt {|NA', Agent B', Key K, X'|} (shrK A')) \
   3.102 +\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
   3.103  \                  : set_of_list evs;                        \
   3.104  \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
   3.105  by (dtac lemma 1);
   3.106 @@ -354,8 +354,8 @@
   3.107   "!!evs. [| A ~: lost;  B ~: lost;  \
   3.108  \           evs : ns_shared lost;  evt: ns_shared lost |]  \
   3.109  \        ==> Says Server A                                             \
   3.110 -\              (Crypt {|NA, Agent B, Key K,                            \
   3.111 -\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
   3.112 +\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   3.113 +\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   3.114  \             : set_of_list evs -->                                    \
   3.115  \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
   3.116  \        Key K ~: analz (sees lost Spy evs)";
   3.117 @@ -393,7 +393,7 @@
   3.118  (*Final version: Server's message in the most abstract form*)
   3.119  goal thy 
   3.120   "!!evs. [| Says Server A                                               \
   3.121 -\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
   3.122 +\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
   3.123  \           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   3.124  \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   3.125  \        |] ==> K ~: analz (sees lost Spy evs)";
   3.126 @@ -405,7 +405,7 @@
   3.127  goal thy 
   3.128   "!!evs. [| C ~: {A,B,Server};                                          \
   3.129  \           Says Server A                                               \
   3.130 -\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
   3.131 +\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
   3.132  \           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
   3.133  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   3.134  \        ==> K ~: analz (sees lost C evs)";
   3.135 @@ -424,11 +424,11 @@
   3.136  
   3.137  (*If the encrypted message appears then it originated with the Server*)
   3.138  goal thy
   3.139 - "!!evs. [| Crypt {|Key K, Agent A|} (shrK B) : parts (sees lost Spy evs); \
   3.140 + "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
   3.141  \           B ~: lost;  evs : ns_shared lost |]                        \
   3.142  \         ==> EX NA. Says Server A                                     \
   3.143 -\              (Crypt {|NA, Agent B, Key K,                            \
   3.144 -\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
   3.145 +\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   3.146 +\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   3.147  \             : set_of_list evs";
   3.148  by (etac rev_mp 1);
   3.149  by (etac ns_shared.induct 1);
   3.150 @@ -444,10 +444,10 @@
   3.151  goal thy
   3.152   "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
   3.153  \        ==> Key K ~: analz (sees lost Spy evs) -->             \
   3.154 -\            Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   3.155 +\            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   3.156  \            : set_of_list evs --> \
   3.157 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->            \
   3.158 -\            Says B A (Crypt (Nonce NB) K) : set_of_list evs";
   3.159 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
   3.160 +\            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   3.161  by (etac ns_shared.induct 1);
   3.162  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   3.163  by parts_Fake_tac;
   3.164 @@ -461,7 +461,7 @@
   3.165  by (Fast_tac 2);
   3.166  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   3.167  (*Contradiction from the assumption   
   3.168 -   Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
   3.169 +   Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *)
   3.170  by (dtac Crypt_imp_invKey_keysFor 1);
   3.171  (**LEVEL 10**)
   3.172  by (Asm_full_simp_tac 1);
   3.173 @@ -475,12 +475,12 @@
   3.174  val lemma = result();
   3.175  
   3.176  goal thy
   3.177 - "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs);           \
   3.178 -\           Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   3.179 + "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   3.180 +\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   3.181  \           : set_of_list evs;                                        \
   3.182  \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   3.183  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   3.184 -\        ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
   3.185 +\        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
   3.186  by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   3.187                        addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
   3.188  qed "A_trust_NS4";
     4.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Nov 29 17:58:18 1996 +0100
     4.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Nov 29 18:03:21 1996 +0100
     4.3 @@ -36,15 +36,15 @@
     4.4                 the sender field.*)
     4.5      NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
     4.6               Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
     4.7 -          ==> Says Server A 
     4.8 -                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
     4.9 -                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    4.10 -                   (shrK A)) # evs : ns_shared lost"
    4.11 +          ==> Says Server A (Crypt (shrK A)
    4.12 +                             {|Nonce NA, Agent B, Key (newK evs),   
    4.13 +                               (Crypt (shrK B) {|Key (newK evs), Agent A|})|}) 
    4.14 +                # evs : ns_shared lost"
    4.15  
    4.16            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    4.17              Can inductively show A ~= Server*)
    4.18      NS3  "[| evs: ns_shared lost;  A ~= B;
    4.19 -             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    4.20 +             Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    4.21                 : set_of_list evs;
    4.22               Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    4.23            ==> Says A B X # evs : ns_shared lost"
    4.24 @@ -52,8 +52,8 @@
    4.25           (*Bob's nonce exchange.  He does not know who the message came
    4.26             from, but responds to A because she is mentioned inside.*)
    4.27      NS4  "[| evs: ns_shared lost;  A ~= B;  
    4.28 -             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
    4.29 -          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
    4.30 +             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    4.31 +          ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost"
    4.32  
    4.33           (*Alice responds with Nonce NB if she has seen the key before.
    4.34             Maybe should somehow check Nonce NA again.
    4.35 @@ -61,17 +61,17 @@
    4.36             Letting the Spy add or subtract 1 lets him send ALL nonces.
    4.37             Instead we distinguish the messages by sending the nonce twice.*)
    4.38      NS5  "[| evs: ns_shared lost;  A ~= B;  
    4.39 -             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    4.40 -             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    4.41 +             Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
    4.42 +             Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    4.43                 : set_of_list evs |]
    4.44 -          ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
    4.45 +          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
    4.46    
    4.47           (*This message models possible leaks of session keys.
    4.48             The two Nonces identify the protocol run: the rule insists upon
    4.49             the true senders in order to make them accurate.*)
    4.50      Oops "[| evs: ns_shared lost;  A ~= Spy;
    4.51 -             Says B A (Crypt (Nonce NB) K) : set_of_list evs;
    4.52 -             Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    4.53 +             Says B A (Crypt K (Nonce NB)) : set_of_list evs;
    4.54 +             Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    4.55                 : set_of_list evs |]
    4.56            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    4.57  
     5.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Nov 29 17:58:18 1996 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Nov 29 18:03:21 1996 +0100
     5.3 @@ -23,7 +23,7 @@
     5.4  goal thy 
     5.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     5.6  \        ==> EX K. EX NA. EX evs: otway lost.          \
     5.7 -\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
     5.8 +\               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
     5.9  \                 : set_of_list evs";
    5.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.11  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    5.12 @@ -65,7 +65,7 @@
    5.13  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    5.14  qed "OR4_analz_sees_Spy";
    5.15  
    5.16 -goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
    5.17 +goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    5.18  \                 ==> K : parts (sees lost Spy evs)";
    5.19  by (fast_tac (!claset addSEs partsEs
    5.20                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    5.21 @@ -137,7 +137,7 @@
    5.22  \                Key (newK evs') ~: parts (sees lost Spy evs)";
    5.23  by (parts_induct_tac 1);
    5.24  by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
    5.25 -				    addDs [impOfSubs analz_subset_parts,
    5.26 +                                    addDs [impOfSubs analz_subset_parts,
    5.27                                             impOfSubs parts_insert_subset_Un,
    5.28                                             Suc_leD]
    5.29                                      addss (!simpset))));
    5.30 @@ -167,7 +167,7 @@
    5.31                                addSEs partsEs
    5.32                                addSDs  [Says_imp_sees_Spy RS parts.Inj]
    5.33                                addEs [leD RS notE]
    5.34 -			      addDs  [impOfSubs analz_subset_parts,
    5.35 +                              addDs  [impOfSubs analz_subset_parts,
    5.36                                        impOfSubs parts_insert_subset_Un,
    5.37                                        Suc_leD]
    5.38                                addss (!simpset))));
    5.39 @@ -218,7 +218,7 @@
    5.40    for Oops case.*)
    5.41  goal thy 
    5.42   "!!evs. [| Says Server B \
    5.43 -\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
    5.44 +\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
    5.45  \           evs : otway lost |]                                   \
    5.46  \        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
    5.47  \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    5.48 @@ -284,7 +284,7 @@
    5.49  goal thy 
    5.50   "!!evs. evs : otway lost ==>                                                 \
    5.51  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    5.52 -\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
    5.53 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
    5.54  \     B=B' & NA=NA' & NB=NB' & X=X'";
    5.55  by (etac otway.induct 1);
    5.56  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    5.57 @@ -301,9 +301,9 @@
    5.58  val lemma = result();
    5.59  
    5.60  goal thy 
    5.61 - "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
    5.62 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    5.63  \            : set_of_list evs;                                    \ 
    5.64 -\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
    5.65 +\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    5.66  \            : set_of_list evs;                                    \
    5.67  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    5.68  by (dtac lemma 1);
    5.69 @@ -320,10 +320,10 @@
    5.70  (*Only OR1 can have caused such a part of a message to appear.*)
    5.71  goal thy 
    5.72   "!!evs. [| A ~: lost;  evs : otway lost |]                        \
    5.73 -\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)               \
    5.74 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
    5.75  \             : parts (sees lost Spy evs) -->                      \
    5.76  \            Says A B {|NA, Agent A, Agent B,                      \
    5.77 -\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
    5.78 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    5.79  \             : set_of_list evs";
    5.80  by (parts_induct_tac 1);
    5.81  qed_spec_mp "Crypt_imp_OR1";
    5.82 @@ -334,7 +334,7 @@
    5.83  goal thy 
    5.84   "!!evs. [| evs : otway lost; A ~: lost |]               \
    5.85  \ ==> EX B'. ALL B.    \
    5.86 -\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
    5.87 +\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
    5.88  \        --> B = B'";
    5.89  by (parts_induct_tac 1);
    5.90  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
    5.91 @@ -345,8 +345,8 @@
    5.92  val lemma = result();
    5.93  
    5.94  goal thy 
    5.95 - "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A): parts(sees lost Spy evs); \
    5.96 -\          Crypt {|NA, Agent A, Agent C|} (shrK A): parts(sees lost Spy evs); \
    5.97 + "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
    5.98 +\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
    5.99  \          evs : otway lost;  A ~: lost |]                                    \
   5.100  \        ==> B = C";
   5.101  by (dtac lemma 1);
   5.102 @@ -365,9 +365,9 @@
   5.103    over-simplified version of this protocol: see OtwayRees_Bad.*)
   5.104  goal thy 
   5.105   "!!evs. [| A ~: lost;  evs : otway lost |]                            \
   5.106 -\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
   5.107 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
   5.108  \             : parts (sees lost Spy evs) -->                       \
   5.109 -\            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
   5.110 +\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   5.111  \             ~: parts (sees lost Spy evs)";
   5.112  by (parts_induct_tac 1);
   5.113  by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
   5.114 @@ -380,14 +380,14 @@
   5.115    to start a run, then it originated with the Server!*)
   5.116  goal thy 
   5.117   "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   5.118 -\    ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs)      \
   5.119 +\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
   5.120  \        --> Says A B {|NA, Agent A, Agent B,                          \
   5.121 -\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}      \
   5.122 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   5.123  \             : set_of_list evs -->                                    \
   5.124  \            (EX NB. Says Server B                                     \
   5.125  \                 {|NA,                                                \
   5.126 -\                   Crypt {|NA, Key K|} (shrK A),                      \
   5.127 -\                   Crypt {|NB, Key K|} (shrK B)|}                     \
   5.128 +\                   Crypt (shrK A) {|NA, Key K|},                      \
   5.129 +\                   Crypt (shrK B) {|NB, Key K|}|}                     \
   5.130  \                   : set_of_list evs)";
   5.131  by (parts_induct_tac 1);
   5.132  (*OR1: it cannot be a new Nonce, contradiction.*)
   5.133 @@ -420,16 +420,16 @@
   5.134    bad form of this protocol, even though we can prove
   5.135    Spy_not_see_encrypted_key*)
   5.136  goal thy 
   5.137 - "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
   5.138 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   5.139  \            : set_of_list evs;                                    \
   5.140  \           Says A B {|NA, Agent A, Agent B,                       \
   5.141 -\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
   5.142 +\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   5.143  \            : set_of_list evs;                                    \
   5.144  \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   5.145  \        ==> EX NB. Says Server B                                  \
   5.146  \                     {|NA,                                        \
   5.147 -\                       Crypt {|NA, Key K|} (shrK A),              \
   5.148 -\                       Crypt {|NB, Key K|} (shrK B)|}             \
   5.149 +\                       Crypt (shrK A) {|NA, Key K|},              \
   5.150 +\                       Crypt (shrK B) {|NB, Key K|}|}             \
   5.151  \                       : set_of_list evs";
   5.152  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   5.153                        addEs  partsEs
   5.154 @@ -444,8 +444,8 @@
   5.155  goal thy 
   5.156   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   5.157  \        ==> Says Server B                                                 \
   5.158 -\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
   5.159 -\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
   5.160 +\              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   5.161 +\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   5.162  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   5.163  \            Key K ~: analz (sees lost Spy evs)";
   5.164  by (etac otway.induct 1);
   5.165 @@ -467,8 +467,8 @@
   5.166  
   5.167  goal thy 
   5.168   "!!evs. [| Says Server B \
   5.169 -\            {|NA, Crypt {|NA, K|} (shrK A),                             \
   5.170 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   5.171 +\            {|NA, Crypt (shrK A) {|NA, K|},                             \
   5.172 +\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   5.173  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   5.174  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   5.175  \        ==> K ~: analz (sees lost Spy evs)";
   5.176 @@ -480,8 +480,8 @@
   5.177  goal thy 
   5.178   "!!evs. [| C ~: {A,B,Server};                                           \
   5.179  \           Says Server B                                                \
   5.180 -\            {|NA, Crypt {|NA, K|} (shrK A),                             \
   5.181 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   5.182 +\            {|NA, Crypt (shrK A) {|NA, K|},                             \
   5.183 +\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   5.184  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   5.185  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   5.186  \        ==> K ~: analz (sees lost C evs)";
   5.187 @@ -498,11 +498,11 @@
   5.188    know anything about X: it does NOT have to have the right form.*)
   5.189  goal thy 
   5.190   "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   5.191 -\        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
   5.192 +\        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   5.193  \             : parts (sees lost Spy evs) -->                  \
   5.194  \            (EX X. Says B Server                              \
   5.195  \             {|NA, Agent A, Agent B, X,                       \
   5.196 -\               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
   5.197 +\               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   5.198  \             : set_of_list evs)";
   5.199  by (parts_induct_tac 1);
   5.200  by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   5.201 @@ -514,7 +514,7 @@
   5.202  goal thy 
   5.203   "!!evs. [| evs : otway lost; B ~: lost |]               \
   5.204  \ ==> EX NA' A'. ALL NA A.                               \
   5.205 -\      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
   5.206 +\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   5.207  \      --> NA = NA' & A = A'";
   5.208  by (parts_induct_tac 1);
   5.209  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   5.210 @@ -524,9 +524,9 @@
   5.211  val lemma = result();
   5.212  
   5.213  goal thy 
   5.214 - "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
   5.215 + "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   5.216  \                  : parts(sees lost Spy evs);         \
   5.217 -\          Crypt {|NC, NB, Agent C, Agent B|} (shrK B) \
   5.218 +\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   5.219  \                  : parts(sees lost Spy evs);         \
   5.220  \          evs : otway lost;  B ~: lost |]             \
   5.221  \        ==> NC = NA & C = A";
   5.222 @@ -543,14 +543,14 @@
   5.223    then it originated with the Server!*)
   5.224  goal thy 
   5.225   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   5.226 -\    ==> Crypt {|NB, Key K|} (shrK B) : parts (sees lost Spy evs)        \
   5.227 +\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   5.228  \        --> (ALL X'. Says B Server                                      \
   5.229  \                       {|NA, Agent A, Agent B, X',                      \
   5.230 -\                         Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
   5.231 +\                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   5.232  \             : set_of_list evs                                          \
   5.233  \             --> Says Server B                                          \
   5.234 -\                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
   5.235 -\                        Crypt {|NB, Key K|} (shrK B)|}                  \
   5.236 +\                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   5.237 +\                        Crypt (shrK B) {|NB, Key K|}|}                  \
   5.238  \                   : set_of_list evs)";
   5.239  by (parts_induct_tac 1);
   5.240  (*OR1: it cannot be a new Nonce, contradiction.*)
   5.241 @@ -577,16 +577,15 @@
   5.242    has sent the correct message.*)
   5.243  goal thy 
   5.244   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   5.245 -\           Says S B {|NA, X, Crypt {|NB, Key K|} (shrK B)|}       \
   5.246 +\           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
   5.247  \            : set_of_list evs;                                    \
   5.248  \           Says B Server {|NA, Agent A, Agent B, X',              \
   5.249 -\                           Crypt {|NA, NB, Agent A, Agent B|}     \
   5.250 -\                                 (shrK B)|}                       \
   5.251 +\                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   5.252  \            : set_of_list evs |]                                  \
   5.253  \        ==> Says Server B                                         \
   5.254  \                 {|NA,                                            \
   5.255 -\                   Crypt {|NA, Key K|} (shrK A),                  \
   5.256 -\                   Crypt {|NB, Key K|} (shrK B)|}                 \
   5.257 +\                   Crypt (shrK A) {|NA, Key K|},                  \
   5.258 +\                   Crypt (shrK B) {|NB, Key K|}|}                 \
   5.259  \                   : set_of_list evs";
   5.260  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   5.261                        addEs  partsEs
   5.262 @@ -600,15 +599,14 @@
   5.263  goal thy 
   5.264   "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   5.265  \        ==> Says Server B                                            \
   5.266 -\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
   5.267 -\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
   5.268 +\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   5.269 +\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   5.270  \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   5.271 -\                            Crypt {|NA, NB, Agent A, Agent B|}       \
   5.272 -\                                  (shrK B)|}                         \
   5.273 +\                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   5.274  \            : set_of_list evs)";
   5.275  by (etac otway.induct 1);
   5.276  by (Auto_tac());
   5.277 -bd (Says_imp_sees_Spy RS parts.Inj) 1;
   5.278 +by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   5.279  by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   5.280  bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   5.281  
   5.282 @@ -617,18 +615,15 @@
   5.283    We could probably prove that X has the expected form, but that is not
   5.284    strictly necessary for authentication.*)
   5.285  goal thy 
   5.286 - "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
   5.287 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   5.288  \            : set_of_list evs;                                    \
   5.289  \           Says A B {|NA, Agent A, Agent B,                       \
   5.290 -\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
   5.291 +\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   5.292  \            : set_of_list evs;                                    \
   5.293  \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   5.294  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   5.295 -\                                     Crypt {|NA, NB, Agent A, Agent B|}    \
   5.296 -\                                           (shrK B)|}                      \
   5.297 +\                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   5.298  \            : set_of_list evs";
   5.299  by (fast_tac (!claset addSDs  [A_trust_OR4]
   5.300 -	              addSEs [OR3_imp_OR2]) 1);
   5.301 +                      addSEs [OR3_imp_OR2]) 1);
   5.302  qed "A_auths_B";
   5.303 -
   5.304 -
     6.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Nov 29 17:58:18 1996 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Nov 29 18:03:21 1996 +0100
     6.3 @@ -30,8 +30,8 @@
     6.4           (*Alice initiates a protocol run*)
     6.5      OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
     6.6            ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
     6.7 -                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
     6.8 -                               (shrK A) |} 
     6.9 +                         Crypt (shrK A)
    6.10 +                               {|Nonce (newN evs), Agent A, Agent B|} |} 
    6.11                   # evs : otway lost"
    6.12  
    6.13           (*Bob's response to Alice's message.  Bob doesn't know who 
    6.14 @@ -41,8 +41,8 @@
    6.15               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    6.16            ==> Says B Server 
    6.17                    {|Nonce NA, Agent A, Agent B, X, 
    6.18 -                    Crypt {|Nonce NA, Nonce (newN evs), 
    6.19 -                            Agent A, Agent B|} (shrK B)|}
    6.20 +                    Crypt 
    6.21 +                          (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|}
    6.22                   # evs : otway lost"
    6.23  
    6.24           (*The Server receives Bob's message and checks that the three NAs
    6.25 @@ -51,30 +51,30 @@
    6.26      OR3  "[| evs: otway lost;  B ~= Server;
    6.27               Says B' Server 
    6.28                    {|Nonce NA, Agent A, Agent B, 
    6.29 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    6.30 -                    Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|}
    6.31 +                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    6.32 +                    Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    6.33                 : set_of_list evs |]
    6.34            ==> Says Server B 
    6.35                    {|Nonce NA, 
    6.36 -                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    6.37 -                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    6.38 +                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
    6.39 +                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
    6.40                   # evs : otway lost"
    6.41  
    6.42           (*Bob receives the Server's (?) message and compares the Nonces with
    6.43  	   those in the message he previously sent the Server.*)
    6.44      OR4  "[| evs: otway lost;  A ~= B;  
    6.45 -             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    6.46 +             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    6.47                 : set_of_list evs;
    6.48               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    6.49 -                             Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} 
    6.50 -                                   (shrK B)|}
    6.51 +                             Crypt (shrK B)
    6.52 +                                   {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    6.53                 : set_of_list evs |]
    6.54            ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    6.55  
    6.56           (*This message models possible leaks of session keys.  The nonces
    6.57             identify the protocol run.*)
    6.58      Oops "[| evs: otway lost;  B ~= Spy;
    6.59 -             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    6.60 +             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    6.61                 : set_of_list evs |]
    6.62            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    6.63  
     7.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 17:58:18 1996 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 18:03:21 1996 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4  goal thy 
     7.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     7.6  \        ==> EX K. EX NA. EX evs: otway lost.          \
     7.7 -\             Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
     7.8 +\             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
     7.9  \             : set_of_list evs";
    7.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    7.11  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    7.12 @@ -59,7 +59,7 @@
    7.13  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    7.14  qed "OR4_analz_sees_Spy";
    7.15  
    7.16 -goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
    7.17 +goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    7.18  \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    7.19  by (fast_tac (!claset addSEs partsEs
    7.20                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    7.21 @@ -176,8 +176,8 @@
    7.22  (*Describes the form of K and NA when the Server sends this message.*)
    7.23  goal thy 
    7.24   "!!evs. [| Says Server B \
    7.25 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
    7.26 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
    7.27 +\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    7.28 +\             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
    7.29  \           evs : otway lost |]                                        \
    7.30  \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
    7.31  \            (EX i. NA = Nonce i) &                  \
    7.32 @@ -246,8 +246,8 @@
    7.33   "!!evs. evs : otway lost ==>                      \
    7.34  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    7.35  \       Says Server B \
    7.36 -\         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
    7.37 -\           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
    7.38 +\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
    7.39 +\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
    7.40  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    7.41  by (etac otway.induct 1);
    7.42  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    7.43 @@ -266,12 +266,12 @@
    7.44  
    7.45  goal thy 
    7.46  "!!evs. [| Says Server B                                           \
    7.47 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
    7.48 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
    7.49 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
    7.50 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
    7.51  \           : set_of_list evs;                                     \
    7.52  \          Says Server B'                                          \
    7.53 -\            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
    7.54 -\              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
    7.55 +\            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    7.56 +\              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    7.57  \           : set_of_list evs;                                     \
    7.58  \          evs : otway lost |]                                     \
    7.59  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    7.60 @@ -289,11 +289,11 @@
    7.61  (*If the encrypted message appears then it originated with the Server!*)
    7.62  goal thy 
    7.63   "!!evs. [| A ~: lost;  evs : otway lost |]                 \
    7.64 -\ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
    7.65 +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
    7.66  \      : parts (sees lost Spy evs)                          \
    7.67  \     --> (EX NB. Says Server B                                     \
    7.68 -\                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
    7.69 -\                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
    7.70 +\                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    7.71 +\                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    7.72  \                  : set_of_list evs)";
    7.73  by (parts_induct_tac 1);
    7.74  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    7.75 @@ -308,12 +308,12 @@
    7.76    Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
    7.77    the Server's message from its nonce NA.)*)
    7.78  goal thy 
    7.79 - "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
    7.80 + "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    7.81  \            : set_of_list evs;                                         \
    7.82  \           A ~: lost;  evs : otway lost |]                             \
    7.83  \        ==> EX NB. Says Server B                                       \
    7.84 -\                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
    7.85 -\                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
    7.86 +\                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    7.87 +\                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    7.88  \                   : set_of_list evs";
    7.89  by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    7.90                        addEs  partsEs
    7.91 @@ -328,8 +328,8 @@
    7.92  goal thy 
    7.93   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
    7.94  \        ==> Says Server B                                                 \
    7.95 -\             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
    7.96 -\               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
    7.97 +\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    7.98 +\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    7.99  \            : set_of_list evs -->                                         \
   7.100  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   7.101  \            Key K ~: analz (sees lost Spy evs)";
   7.102 @@ -351,8 +351,8 @@
   7.103  
   7.104  goal thy 
   7.105   "!!evs. [| Says Server B                                                     \
   7.106 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   7.107 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   7.108 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   7.109 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   7.110  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   7.111  \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   7.112  \        ==> K ~: analz (sees lost Spy evs)";
   7.113 @@ -364,8 +364,8 @@
   7.114  goal thy 
   7.115   "!!evs. [| C ~: {A,B,Server};                                                \
   7.116  \           Says Server B                                                     \
   7.117 -\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   7.118 -\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   7.119 +\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
   7.120 +\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
   7.121  \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   7.122  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   7.123  \        ==> K ~: analz (sees lost C evs)";
   7.124 @@ -381,11 +381,11 @@
   7.125  (*If the encrypted message appears then it originated with the Server!*)
   7.126  goal thy 
   7.127   "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
   7.128 -\    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
   7.129 +\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
   7.130  \         : parts (sees lost Spy evs)                                       \
   7.131  \        --> (EX NA. Says Server B                                          \
   7.132 -\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   7.133 -\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   7.134 +\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   7.135 +\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   7.136  \                     : set_of_list evs)";
   7.137  by (parts_induct_tac 1);
   7.138  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   7.139 @@ -398,11 +398,11 @@
   7.140    has sent the correct message.*)
   7.141  goal thy 
   7.142   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   7.143 -\           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
   7.144 +\           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
   7.145  \            : set_of_list evs |]                                           \
   7.146  \        ==> EX NA. Says Server B                                           \
   7.147 -\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   7.148 -\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   7.149 +\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   7.150 +\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   7.151  \                     : set_of_list evs";
   7.152  by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   7.153                        addEs  partsEs
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Nov 29 17:58:18 1996 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Nov 29 18:03:21 1996 +0100
     8.3 @@ -45,15 +45,15 @@
     8.4               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
     8.5                 : set_of_list evs |]
     8.6            ==> Says Server B 
     8.7 -               {|Crypt {|Nonce NA, Agent A, Agent B, Key(newK evs)|} (shrK A),
     8.8 -                 Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|}
     8.9 +               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
    8.10 +                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
    8.11                # evs : otway lost"
    8.12  
    8.13           (*Bob receives the Server's (?) message and compares the Nonces with
    8.14  	   those in the message he previously sent the Server.*)
    8.15      OR4  "[| evs: otway lost;  A ~= B;
    8.16               Says S B {|X, 
    8.17 -                        Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    8.18 +                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    8.19                 : set_of_list evs;
    8.20               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    8.21                 : set_of_list evs |]
    8.22 @@ -63,8 +63,8 @@
    8.23             identify the protocol run.  B is not assumed to know shrK A.*)
    8.24      Oops "[| evs: otway lost;  B ~= Spy;
    8.25               Says Server B 
    8.26 -                      {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), 
    8.27 -                        Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    8.28 +                      {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
    8.29 +                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    8.30                 : set_of_list evs |]
    8.31            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    8.32  
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Nov 29 17:58:18 1996 +0100
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Nov 29 18:03:21 1996 +0100
     9.3 @@ -25,7 +25,7 @@
     9.4  goal thy 
     9.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     9.6  \        ==> EX K. EX NA. EX evs: otway.          \
     9.7 -\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
     9.8 +\               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
     9.9  \                 : set_of_list evs";
    9.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.11  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    9.12 @@ -68,7 +68,7 @@
    9.13  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    9.14  qed "OR4_analz_sees_Spy";
    9.15  
    9.16 -goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
    9.17 +goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    9.18  \                 ==> K : parts (sees lost Spy evs)";
    9.19  by (fast_tac (!claset addSEs partsEs
    9.20                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    9.21 @@ -218,7 +218,7 @@
    9.22    for Oops case.*)
    9.23  goal thy 
    9.24   "!!evs. [| Says Server B \
    9.25 -\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
    9.26 +\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
    9.27  \           evs : otway |]                                   \
    9.28  \        ==> (EX evt: otway. K = Key(newK evt)) &            \
    9.29  \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    9.30 @@ -295,7 +295,7 @@
    9.31  goal thy 
    9.32   "!!evs. evs : otway ==>                                                 \
    9.33  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    9.34 -\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
    9.35 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
    9.36  \     B=B' & NA=NA' & NB=NB' & X=X'";
    9.37  by (etac otway.induct 1);
    9.38  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    9.39 @@ -312,9 +312,9 @@
    9.40  val lemma = result();
    9.41  
    9.42  goal thy 
    9.43 - "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
    9.44 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    9.45  \            : set_of_list evs;                                    \ 
    9.46 -\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
    9.47 +\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    9.48  \            : set_of_list evs;                                    \
    9.49  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    9.50  by (dtac lemma 1);
    9.51 @@ -329,8 +329,8 @@
    9.52  goal thy 
    9.53   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
    9.54  \        ==> Says Server B                                            \
    9.55 -\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
    9.56 -\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
    9.57 +\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    9.58 +\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
    9.59  \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
    9.60  \            Key K ~: analz (sees lost Spy evs)";
    9.61  by (etac otway.induct 1);
    9.62 @@ -353,8 +353,8 @@
    9.63  
    9.64  goal thy 
    9.65   "!!evs. [| Says Server B                                         \
    9.66 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
    9.67 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
    9.68 +\            {|NA, Crypt (shrK A) {|NA, K|},                      \
    9.69 +\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
    9.70  \            Says B Spy {|NA, NB, K|} ~: set_of_list evs;         \
    9.71  \           A ~: lost;  B ~: lost;  evs : otway |]                \
    9.72  \        ==> K ~: analz (sees lost Spy evs)";
    9.73 @@ -371,10 +371,10 @@
    9.74  	this version.*)
    9.75  goal thy 
    9.76   "!!evs. [| A ~: lost;  A ~= B; evs : otway |]                 \
    9.77 -\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)           \
    9.78 +\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
    9.79  \             : parts (sees lost Spy evs) -->                  \
    9.80  \            Says A B {|NA, Agent A, Agent B,                  \
    9.81 -\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
    9.82 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    9.83  \             : set_of_list evs";
    9.84  by (parts_induct_tac 1);
    9.85  by (Fast_tac 1);
    9.86 @@ -387,14 +387,14 @@
    9.87            substituting some other nonce NA' for NB.*)
    9.88  goal thy 
    9.89   "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                        \
    9.90 -\        ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
    9.91 +\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
    9.92  \            Says A B {|NA, Agent A, Agent B,                  \
    9.93 -\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
    9.94 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    9.95  \             : set_of_list evs -->                            \
    9.96  \            (EX B NB. Says Server B                           \
    9.97  \                 {|NA,                                        \
    9.98 -\                   Crypt {|NA, Key K|} (shrK A),              \
    9.99 -\                   Crypt {|NB, Key K|} (shrK B)|}             \
   9.100 +\                   Crypt (shrK A) {|NA, Key K|},              \
   9.101 +\                   Crypt (shrK B) {|NB, Key K|}|}             \
   9.102  \                   : set_of_list evs)";
   9.103  by (parts_induct_tac 1);
   9.104  (*OR1: it cannot be a new Nonce, contradiction.*)
   9.105 @@ -415,12 +415,12 @@
   9.106    in two different roles:
   9.107            Says B' Server
   9.108             {|Nonce NAa, Agent Aa, Agent A,
   9.109 -             Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK Aa), Nonce NA,
   9.110 -             Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK A)|}
   9.111 +             Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
   9.112 +             Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
   9.113            : set_of_list evsa;
   9.114            Says A B
   9.115             {|Nonce NA, Agent A, Agent B,
   9.116 -             Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
   9.117 +             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
   9.118            : set_of_list evsa 
   9.119  *)
   9.120  writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
    10.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Nov 29 17:58:18 1996 +0100
    10.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Nov 29 18:03:21 1996 +0100
    10.3 @@ -29,8 +29,8 @@
    10.4           (*Alice initiates a protocol run*)
    10.5      OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    10.6            ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    10.7 -                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    10.8 -                               (shrK A) |} 
    10.9 +                         Crypt (shrK A) 
   10.10 +                               {|Nonce (newN evs), Agent A, Agent B|} |} 
   10.11                   # evs : otway"
   10.12  
   10.13           (*Bob's response to Alice's message.  Bob doesn't know who 
   10.14 @@ -40,7 +40,7 @@
   10.15               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
   10.16            ==> Says B Server 
   10.17                    {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
   10.18 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
   10.19 +                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   10.20                   # evs : otway"
   10.21  
   10.22           (*The Server receives Bob's message and checks that the three NAs
   10.23 @@ -49,20 +49,20 @@
   10.24      OR3  "[| evs: otway;  B ~= Server;
   10.25               Says B' Server 
   10.26                    {|Nonce NA, Agent A, Agent B, 
   10.27 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
   10.28 +                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   10.29                      Nonce NB, 
   10.30 -                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
   10.31 +                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   10.32                 : set_of_list evs |]
   10.33            ==> Says Server B 
   10.34                    {|Nonce NA, 
   10.35 -                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
   10.36 -                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
   10.37 +                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
   10.38 +                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
   10.39                   # evs : otway"
   10.40  
   10.41           (*Bob receives the Server's (?) message and compares the Nonces with
   10.42  	   those in the message he previously sent the Server.*)
   10.43      OR4  "[| evs: otway;  A ~= B;
   10.44 -             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
   10.45 +             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   10.46                 : set_of_list evs;
   10.47               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
   10.48                 : set_of_list evs |]
   10.49 @@ -71,7 +71,7 @@
   10.50           (*This message models possible leaks of session keys.  The nonces
   10.51             identify the protocol run.*)
   10.52      Oops "[| evs: otway;  B ~= Spy;
   10.53 -             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
   10.54 +             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
   10.55                 : set_of_list evs |]
   10.56            ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
   10.57  
    11.1 --- a/src/HOL/Auth/Shared.ML	Fri Nov 29 17:58:18 1996 +0100
    11.2 +++ b/src/HOL/Auth/Shared.ML	Fri Nov 29 18:03:21 1996 +0100
    11.3 @@ -120,7 +120,7 @@
    11.4  AddSIs [sees_own_shrK, Spy_sees_lost];
    11.5  
    11.6  (*Added for Yahalom/lost_tac*)
    11.7 -goal thy "!!A. [| Crypt X (shrK A) : analz (sees lost Spy evs);  A: lost |] \
    11.8 +goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
    11.9  \              ==> X : analz (sees lost Spy evs)";
   11.10  by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   11.11  qed "Crypt_Spy_analz_lost";
   11.12 @@ -172,14 +172,14 @@
   11.13  qed_spec_mp "Says_imp_sees_Spy";
   11.14  
   11.15  goal thy  
   11.16 - "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;  C : lost |] \
   11.17 + "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
   11.18  \        ==> X : analz (sees lost Spy evs)";
   11.19  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   11.20                        addss (!simpset)) 1);
   11.21  qed "Says_Crypt_lost";
   11.22  
   11.23  goal thy  
   11.24 - "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
   11.25 + "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;        \
   11.26  \           X ~: analz (sees lost Spy evs) |]                     \
   11.27  \        ==> C ~: lost";
   11.28  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
    12.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Nov 29 17:58:18 1996 +0100
    12.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 29 18:03:21 1996 +0100
    12.3 @@ -22,7 +22,7 @@
    12.4  goal thy 
    12.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    12.6  \        ==> EX X NB K. EX evs: yahalom lost.          \
    12.7 -\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    12.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    12.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   12.10  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
   12.11  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   12.12 @@ -54,7 +54,7 @@
   12.13  (** For reasoning about the encrypted portion of messages **)
   12.14  
   12.15  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   12.16 -goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
   12.17 +goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   12.18  \                X : analz (sees lost Spy evs)";
   12.19  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   12.20  qed "YM4_analz_sees_Spy";
   12.21 @@ -63,7 +63,7 @@
   12.22            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   12.23  
   12.24  (*Relates to both YM4 and Oops*)
   12.25 -goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
   12.26 +goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
   12.27  \                  : set_of_list evs ==> \
   12.28  \                K : parts (sees lost Spy evs)";
   12.29  by (fast_tac (!claset addSEs partsEs
   12.30 @@ -145,7 +145,7 @@
   12.31  
   12.32  
   12.33  (*Ready-made for the classical reasoner*)
   12.34 -goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|}  \
   12.35 +goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|}  \
   12.36  \                   : set_of_list evs;  evs : yahalom lost |]              \
   12.37  \                ==> R";
   12.38  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   12.39 @@ -189,7 +189,7 @@
   12.40    Oops as well as main secrecy property.*)
   12.41  goal thy 
   12.42   "!!evs. [| Says Server A                                           \
   12.43 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
   12.44 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
   12.45  \           evs : yahalom lost |]                                   \
   12.46  \        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   12.47  by (etac rev_mp 1);
   12.48 @@ -222,7 +222,7 @@
   12.49    We require that agents should behave like this subsequently also.*)
   12.50  goal thy 
   12.51   "!!evs. evs : yahalom lost ==> \
   12.52 -\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   12.53 +\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
   12.54  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   12.55  by (etac yahalom.induct 1);
   12.56  by parts_Fake_tac;
   12.57 @@ -273,7 +273,7 @@
   12.58   "!!evs. evs : yahalom lost ==>                                     \
   12.59  \      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
   12.60  \          Says Server A                                            \
   12.61 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
   12.62 +\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   12.63  \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   12.64  by (etac yahalom.induct 1);
   12.65  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   12.66 @@ -289,10 +289,10 @@
   12.67  
   12.68  goal thy 
   12.69  "!!evs. [| Says Server A                                            \
   12.70 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
   12.71 +\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   12.72  \           : set_of_list evs;                                      \
   12.73  \          Says Server A'                                           \
   12.74 -\           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|}   \
   12.75 +\           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
   12.76  \           : set_of_list evs;                                      \
   12.77  \          evs : yahalom lost |]                                    \
   12.78  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   12.79 @@ -306,12 +306,12 @@
   12.80  
   12.81  (*If the encrypted message appears then it originated with the Server*)
   12.82  goal thy
   12.83 - "!!evs. [| Crypt {|Agent B, Key K, NA, NB|} (shrK A)                  \
   12.84 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
   12.85  \            : parts (sees lost Spy evs);                              \
   12.86  \           A ~: lost;  evs : yahalom lost |]                          \
   12.87  \         ==> Says Server A                                            \
   12.88 -\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
   12.89 -\                Crypt {|Agent A, Key K|} (shrK B)|}                   \
   12.90 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
   12.91 +\                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   12.92  \             : set_of_list evs";
   12.93  by (etac rev_mp 1);
   12.94  by (parts_induct_tac 1);
   12.95 @@ -323,8 +323,8 @@
   12.96  goal thy 
   12.97   "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   12.98  \        ==> Says Server A                                        \
   12.99 -\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),       \
  12.100 -\                Crypt {|Agent A, Key K|} (shrK B)|}              \
  12.101 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
  12.102 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
  12.103  \             : set_of_list evs -->                               \
  12.104  \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
  12.105  \            Key K ~: analz (sees lost Spy evs)";
  12.106 @@ -349,8 +349,8 @@
  12.107  (*Final version: Server's message in the most abstract form*)
  12.108  goal thy 
  12.109   "!!evs. [| Says Server A                                               \
  12.110 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
  12.111 -\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
  12.112 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
  12.113 +\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
  12.114  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
  12.115  \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
  12.116  \     K ~: analz (sees lost Spy evs)";
  12.117 @@ -362,8 +362,8 @@
  12.118  goal thy 
  12.119   "!!evs. [| C ~: {A,B,Server};                                          \
  12.120  \           Says Server A                                               \
  12.121 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
  12.122 -\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
  12.123 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
  12.124 +\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
  12.125  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
  12.126  \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
  12.127  \     K ~: analz (sees lost C evs)";
  12.128 @@ -379,12 +379,12 @@
  12.129  (*B knows, by the first part of A's message, that the Server distributed 
  12.130    the key for A and B.  But this part says nothing about nonces.*)
  12.131  goal thy 
  12.132 - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
  12.133 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
  12.134  \           B ~: lost;  evs : yahalom lost |]                           \
  12.135  \        ==> EX NA NB. Says Server A                                    \
  12.136 -\                        {|Crypt {|Agent B, Key K,                      \
  12.137 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
  12.138 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
  12.139 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  12.140 +\                                  Nonce NA, Nonce NB|},       \
  12.141 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  12.142  \                       : set_of_list evs";
  12.143  by (etac rev_mp 1);
  12.144  by (parts_induct_tac 1);
  12.145 @@ -429,7 +429,7 @@
  12.146  
  12.147  goal thy 
  12.148   "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
  12.149 -\      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
  12.150 +\      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
  12.151  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
  12.152  by (parts_induct_tac 1);  (*100 seconds??*)
  12.153  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
  12.154 @@ -439,9 +439,9 @@
  12.155  val lemma = result();
  12.156  
  12.157  goal thy 
  12.158 - "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
  12.159 + "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
  12.160  \                  : parts (sees lost Spy evs);         \
  12.161 -\          Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
  12.162 +\          Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
  12.163  \                  : parts (sees lost Spy evs);         \
  12.164  \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
  12.165  \        ==> NA' = NA & A' = A & B' = B";
  12.166 @@ -473,9 +473,9 @@
  12.167  
  12.168  (*Variant useful for proving secrecy of NB*)
  12.169  goal thy 
  12.170 - "!!evs.[| Says C D   {|X,  Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
  12.171 + "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
  12.172  \          : set_of_list evs;  B ~: lost;         \
  12.173 -\          Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
  12.174 +\          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
  12.175  \          : set_of_list evs;                           \
  12.176  \          NB ~: analz (sees lost Spy evs);             \
  12.177  \          evs : yahalom lost |]  \
  12.178 @@ -489,8 +489,8 @@
  12.179  goal thy 
  12.180   "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
  12.181  \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
  12.182 -\      Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
  12.183 -\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
  12.184 +\      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
  12.185 +\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
  12.186  by (etac yahalom.induct 1);
  12.187  by parts_Fake_tac;
  12.188  by (REPEAT_FIRST 
  12.189 @@ -519,11 +519,11 @@
  12.190  goal thy 
  12.191   "!!evs. evs : yahalom lost                                             \
  12.192  \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
  12.193 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
  12.194 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
  12.195  \            (EX A B NA. Says Server A                                  \
  12.196 -\                        {|Crypt {|Agent B, Key K,                      \
  12.197 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
  12.198 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
  12.199 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  12.200 +\                                  Nonce NA, Nonce NB|},       \
  12.201 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  12.202  \                       : set_of_list evs)";
  12.203  by (etac yahalom.induct 1);
  12.204  by parts_Fake_tac;
  12.205 @@ -552,11 +552,11 @@
  12.206  goal thy 
  12.207   "!!evs. evs : yahalom lost                                             \
  12.208  \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
  12.209 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
  12.210 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
  12.211  \            (EX A B NA. Says Server A                                  \
  12.212 -\                        {|Crypt {|Agent B, Key K,                      \
  12.213 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
  12.214 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
  12.215 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
  12.216 +\                                  Nonce NA, Nonce NB|},       \
  12.217 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
  12.218  \                       : set_of_list evs)";
  12.219  by (etac yahalom.induct 1);
  12.220  by parts_Fake_tac;
  12.221 @@ -580,10 +580,10 @@
  12.222  (*YM3 can only be triggered by YM2*)
  12.223  goal thy 
  12.224   "!!evs. [| Says Server A                                           \
  12.225 -\            {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
  12.226 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
  12.227  \           evs : yahalom lost |]                                        \
  12.228  \        ==> EX B'. Says B' Server                                       \
  12.229 -\                      {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
  12.230 +\                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
  12.231  \                   : set_of_list evs";
  12.232  by (etac rev_mp 1);
  12.233  by (etac yahalom.induct 1);
  12.234 @@ -622,7 +622,7 @@
  12.235  \     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
  12.236  \     (EX K: newK``E. EX A B na X.                                        \
  12.237  \            Says Server A                                                \
  12.238 -\                {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|}   \
  12.239 +\                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
  12.240  \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
  12.241  by (etac yahalom.induct 1);
  12.242  by analz_Fake_tac;
  12.243 @@ -673,7 +673,7 @@
  12.244    for the induction to carry through.*)
  12.245  goal thy 
  12.246   "!!evs. [| Says Server A                                                     \
  12.247 -\            {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
  12.248 +\            {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
  12.249  \           : set_of_list evs;                                                \
  12.250  \           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
  12.251  \           evs : yahalom lost |]                                             \
  12.252 @@ -688,7 +688,7 @@
  12.253  goal thy 
  12.254   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
  12.255  \ ==> Says B Server                                                    \
  12.256 -\          {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
  12.257 +\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
  12.258  \     : set_of_list evs -->                               \
  12.259  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
  12.260  \     Nonce NB ~: analz (sees lost Spy evs)";
  12.261 @@ -757,16 +757,16 @@
  12.262    nonces are forced to agree with NA and NB). *)
  12.263  goal thy 
  12.264   "!!evs. [| Says B Server                                        \
  12.265 -\            {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}  \
  12.266 +\            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
  12.267  \           : set_of_list evs;       \
  12.268 -\           Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
  12.269 -\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
  12.270 +\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
  12.271 +\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
  12.272  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
  12.273  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
  12.274  \         ==> Says Server A                                       \
  12.275 -\                     {|Crypt {|Agent B, Key K,                         \
  12.276 -\                               Nonce NA, Nonce NB|} (shrK A),          \
  12.277 -\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
  12.278 +\                     {|Crypt (shrK A) {|Agent B, Key K,                         \
  12.279 +\                               Nonce NA, Nonce NB|},          \
  12.280 +\                       Crypt (shrK B) {|Agent A, Key K|}|}             \
  12.281  \                   : set_of_list evs";
  12.282  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
  12.283  by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
    13.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Nov 29 17:58:18 1996 +0100
    13.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 29 18:03:21 1996 +0100
    13.3 @@ -35,35 +35,35 @@
    13.4               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    13.5            ==> Says B Server 
    13.6                    {|Agent B, 
    13.7 -                    Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    13.8 +                    Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
    13.9                   # evs : yahalom lost"
   13.10  
   13.11           (*The Server receives Bob's message.  He responds by sending a
   13.12              new session key to Alice, with a packet for forwarding to Bob.*)
   13.13      YM3  "[| evs: yahalom lost;  A ~= Server;
   13.14               Says B' Server 
   13.15 -                  {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
   13.16 +                  {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   13.17                 : set_of_list evs |]
   13.18            ==> Says Server A
   13.19 -                  {|Crypt {|Agent B, Key (newK evs), 
   13.20 -                            Nonce NA, Nonce NB|} (shrK A),
   13.21 -                    Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
   13.22 +                  {|Crypt (shrK A) {|Agent B, Key (newK evs), 
   13.23 +                            Nonce NA, Nonce NB|},
   13.24 +                    Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
   13.25                   # evs : yahalom lost"
   13.26  
   13.27           (*Alice receives the Server's (?) message, checks her Nonce, and
   13.28             uses the new session key to send Bob his Nonce.*)
   13.29      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
   13.30 -             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
   13.31 +             Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   13.32                          X|}  : set_of_list evs;
   13.33               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
   13.34 -          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
   13.35 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
   13.36  
   13.37           (*This message models possible leaks of session keys.  The Nonces
   13.38             identify the protocol run.  Quoting Server here ensures they are
   13.39             correct.*)
   13.40      Oops "[| evs: yahalom lost;  A ~= Spy;
   13.41 -             Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
   13.42 -                                   (shrK A),
   13.43 +             Says Server A {|Crypt (shrK A)
   13.44 +                                   {|Agent B, Key K, Nonce NA, Nonce NB|},
   13.45                               X|}  : set_of_list evs |]
   13.46            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
   13.47  
    14.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Nov 29 17:58:18 1996 +0100
    14.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Nov 29 18:03:21 1996 +0100
    14.3 @@ -23,7 +23,7 @@
    14.4  goal thy 
    14.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    14.6  \        ==> EX X NB K. EX evs: yahalom lost.          \
    14.7 -\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
    14.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    14.9  by (REPEAT (resolve_tac [exI,bexI] 1));
   14.10  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
   14.11  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
   14.12 @@ -55,7 +55,7 @@
   14.13  (** For reasoning about the encrypted portion of messages **)
   14.14  
   14.15  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   14.16 -goal thy "!!evs. Says S A {|NB, Crypt Y (shrK A), X|} : set_of_list evs ==> \
   14.17 +goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
   14.18  \                X : analz (sees lost Spy evs)";
   14.19  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
   14.20  qed "YM4_analz_sees_Spy";
   14.21 @@ -64,7 +64,7 @@
   14.22            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   14.23  
   14.24  (*Relates to both YM4 and Oops*)
   14.25 -goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
   14.26 +goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
   14.27  \                  : set_of_list evs ==> \
   14.28  \                K : parts (sees lost Spy evs)";
   14.29  by (fast_tac (!claset addSEs partsEs
   14.30 @@ -187,7 +187,7 @@
   14.31  (*Describes the form of K when the Server sends this message.  Useful for
   14.32    Oops as well as main secrecy property.*)
   14.33  goal thy 
   14.34 - "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
   14.35 + "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
   14.36  \            : set_of_list evs;                                         \
   14.37  \           evs : yahalom lost |]                                       \
   14.38  \        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
   14.39 @@ -251,7 +251,7 @@
   14.40   "!!evs. evs : yahalom lost ==>                                     \
   14.41  \      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
   14.42  \          Says Server A                                            \
   14.43 -\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   14.44 +\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
   14.45  \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   14.46  by (etac yahalom.induct 1);
   14.47  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   14.48 @@ -267,10 +267,10 @@
   14.49  
   14.50  goal thy 
   14.51  "!!evs. [| Says Server A                                            \
   14.52 -\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
   14.53 +\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
   14.54  \           : set_of_list evs;                                      \
   14.55  \          Says Server A'                                           \
   14.56 -\           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|}   \
   14.57 +\           {|NB', Crypt (shrK A') {|Agent B', Key K, NA'|}, X'|}   \
   14.58  \           : set_of_list evs;                                      \
   14.59  \          evs : yahalom lost |]                                    \
   14.60  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   14.61 @@ -288,8 +288,8 @@
   14.62   "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
   14.63  \           evs : yahalom lost |]            \
   14.64  \        ==> Says Server A                                           \
   14.65 -\              {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),           \
   14.66 -\                    Crypt {|NB, Key K, Agent A|} (shrK B)|}          \
   14.67 +\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},           \
   14.68 +\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}          \
   14.69  \             : set_of_list evs -->                               \
   14.70  \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   14.71  \            Key K ~: analz (sees lost Spy evs)";
   14.72 @@ -316,8 +316,8 @@
   14.73  (*Final version: Server's message in the most abstract form*)
   14.74  goal thy 
   14.75   "!!evs. [| Says Server A                                         \
   14.76 -\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   14.77 -\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   14.78 +\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
   14.79 +\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
   14.80  \           : set_of_list evs;                                    \
   14.81  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   14.82  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   14.83 @@ -330,8 +330,8 @@
   14.84  goal thy 
   14.85   "!!evs. [| C ~: {A,B,Server};                                    \
   14.86  \           Says Server A                                         \
   14.87 -\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
   14.88 -\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
   14.89 +\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
   14.90 +\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
   14.91  \           : set_of_list evs;                                    \
   14.92  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
   14.93  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   14.94 @@ -347,12 +347,12 @@
   14.95  
   14.96  (*If the encrypted message appears then it originated with the Server.*)
   14.97  goal thy
   14.98 - "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A)                \
   14.99 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|}                \
  14.100  \            : parts (sees lost Spy evs);                              \
  14.101  \           A ~: lost;  evs : yahalom lost |]                          \
  14.102  \         ==> EX NB. Says Server A                                     \
  14.103 -\                      {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),    \
  14.104 -\                            Crypt {|NB, Key K, Agent A|} (shrK B)|}   \
  14.105 +\                      {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},    \
  14.106 +\                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
  14.107  \                    : set_of_list evs";
  14.108  by (etac rev_mp 1);
  14.109  by (parts_induct_tac 1);
  14.110 @@ -364,13 +364,13 @@
  14.111  (*B knows, by the first part of A's message, that the Server distributed 
  14.112    the key for A and B. *)
  14.113  goal thy 
  14.114 - "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B)              \
  14.115 + "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
  14.116  \            : parts (sees lost Spy evs);                            \
  14.117  \           B ~: lost;  evs : yahalom lost |]                        \
  14.118  \        ==> EX NA. Says Server A                                    \
  14.119  \                    {|Nonce NB,                                     \
  14.120 -\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),  \
  14.121 -\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
  14.122 +\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
  14.123 +\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
  14.124  \                       : set_of_list evs";
  14.125  by (etac rev_mp 1);
  14.126  by (parts_induct_tac 1);
  14.127 @@ -385,13 +385,13 @@
  14.128  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
  14.129    because we do not have to show that NB is secret. *)
  14.130  goal thy 
  14.131 - "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B),    \
  14.132 -\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
  14.133 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
  14.134 +\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
  14.135  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
  14.136  \        ==> EX NA. Says Server A                                       \
  14.137  \                    {|Nonce NB,                                        \
  14.138 -\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),     \
  14.139 -\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|}    \
  14.140 +\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},     \
  14.141 +\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
  14.142  \                   : set_of_list evs";
  14.143  by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
  14.144  by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
    15.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 17:58:18 1996 +0100
    15.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 18:03:21 1996 +0100
    15.3 @@ -48,25 +48,25 @@
    15.4                 : set_of_list evs |]
    15.5            ==> Says Server A
    15.6                 {|Nonce NB, 
    15.7 -                 Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
    15.8 -                 Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
    15.9 +                 Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
   15.10 +                 Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
   15.11                   # evs : yahalom lost"
   15.12  
   15.13           (*Alice receives the Server's (?) message, checks her Nonce, and
   15.14             uses the new session key to send Bob his Nonce.*)
   15.15      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
   15.16 -             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
   15.17 +             Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   15.18                          X|}
   15.19                 : set_of_list evs;
   15.20               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
   15.21 -          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
   15.22 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
   15.23  
   15.24           (*This message models possible leaks of session keys.  The nonces
   15.25             identify the protocol run.  Quoting Server here ensures they are
   15.26             correct. *)
   15.27      Oops "[| evs: yahalom lost;  A ~= Spy;
   15.28               Says Server A {|Nonce NB, 
   15.29 -                             Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
   15.30 +                             Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   15.31                               X|}  : set_of_list evs |]
   15.32            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
   15.33