# HG changeset patch
# User paulson
# Date 849287001 -3600
# Node ID 80ebd1a213fd9e1f7f5b8788bbfd1cd4dffa098e
# Parent  68829cf138fc9a1272eaec9f96dd7c22a98773f4
Swapped arguments of Crypt (for clarity and because it is conventional)

diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Message.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -58,9 +58,8 @@
 qed "keysFor_insert_MPair";
 
 goalw thy [keysFor_def]
-    "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
+    "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
 by (Auto_tac());
-by (Fast_tac 1);
 qed "keysFor_insert_Crypt";
 
 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
@@ -68,7 +67,7 @@
           keysFor_insert_Key, keysFor_insert_MPair,
           keysFor_insert_Crypt];
 
-goalw thy [keysFor_def] "!!H. Crypt X K : H ==> invKey K : keysFor H";
+goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
 by (Fast_tac 1);
 qed "Crypt_imp_invKey_keysFor";
 
@@ -234,8 +233,8 @@
 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 qed "parts_insert_Key";
 
-goal thy "parts (insert (Crypt X K) H) = \
-\         insert (Crypt X K) (parts (insert X H))";
+goal thy "parts (insert (Crypt K X) H) = \
+\         insert (Crypt K X) (parts (insert X H))";
 by (rtac equalityI 1);
 by (rtac subsetI 1);
 by (etac parts.induct 1);
@@ -378,8 +377,8 @@
 
 (*Can pull out enCrypted message if the Key is not known*)
 goal thy "!!H. Key (invKey K) ~: analz H ==>  \
-\              analz (insert (Crypt X K) H) = \
-\              insert (Crypt X K) (analz H)";
+\              analz (insert (Crypt K X) H) = \
+\              insert (Crypt K X) (analz H)";
 by (rtac (analz_insert RSN (2, equalityI)) 1);
 by (rtac subsetI 1);
 by (etac analz.induct 1);
@@ -387,16 +386,16 @@
 qed "analz_insert_Crypt";
 
 goal thy "!!H. Key (invKey K) : analz H ==>  \
-\              analz (insert (Crypt X K) H) <= \
-\              insert (Crypt X K) (analz (insert X H))";
+\              analz (insert (Crypt K X) H) <= \
+\              insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
 by (eres_inst_tac [("za","x")] analz.induct 1);
 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 val lemma1 = result();
 
 goal thy "!!H. Key (invKey K) : analz H ==>  \
-\              insert (Crypt X K) (analz (insert X H)) <= \
-\              analz (insert (Crypt X K) H)";
+\              insert (Crypt K X) (analz (insert X H)) <= \
+\              analz (insert (Crypt K X) H)";
 by (Auto_tac());
 by (eres_inst_tac [("za","x")] analz.induct 1);
 by (Auto_tac());
@@ -405,19 +404,19 @@
 val lemma2 = result();
 
 goal thy "!!H. Key (invKey K) : analz H ==>  \
-\              analz (insert (Crypt X K) H) = \
-\              insert (Crypt X K) (analz (insert X H))";
+\              analz (insert (Crypt K X) H) = \
+\              insert (Crypt K X) (analz (insert X H))";
 by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
 qed "analz_insert_Decrypt";
 
 (*Case analysis: either the message is secure, or it is not!
   Effective, but can cause subgoals to blow up!
   Use with expand_if;  apparently split_tac does not cope with patterns
-  such as "analz (insert (Crypt X K) H)" *)
-goal thy "analz (insert (Crypt X K) H) =                \
+  such as "analz (insert (Crypt K X) H)" *)
+goal thy "analz (insert (Crypt K X) H) =                \
 \         (if (Key (invKey K) : analz H)                \
-\          then insert (Crypt X K) (analz (insert X H)) \
-\          else insert (Crypt X K) (analz H))";
+\          then insert (Crypt K X) (analz (insert X H)) \
+\          else insert (Crypt K X) (analz H))";
 by (case_tac "Key (invKey K)  : analz H " 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
                                                analz_insert_Decrypt])));
@@ -428,8 +427,8 @@
           analz_Crypt_if];
 
 (*This rule supposes "for the sake of argument" that we have the key.*)
-goal thy  "analz (insert (Crypt X K) H) <=  \
-\          insert (Crypt X K) (analz (insert X H))";
+goal thy  "analz (insert (Crypt K X) H) <=  \
+\          insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
 by (etac analz.induct 1);
 by (Auto_tac());
@@ -496,7 +495,7 @@
 qed "analz_insert_cong";
 
 (*If there are no pairs or encryptions then analz does nothing*)
-goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt X K ~: H |] ==> \
+goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
 \         analz H = H";
 by (Step_tac 1);
 by (etac analz.induct 1);
@@ -528,7 +527,7 @@
 val Nonce_synth = mk_cases "Nonce n : synth H";
 val Key_synth   = mk_cases "Key K : synth H";
 val MPair_synth = mk_cases "{|X,Y|} : synth H";
-val Crypt_synth = mk_cases "Crypt X K : synth H";
+val Crypt_synth = mk_cases "Crypt K X : synth H";
 
 AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
 
@@ -589,7 +588,7 @@
 by (Fast_tac 1);
 qed "Key_synth_eq";
 
-goal thy "!!K. Key K ~: H ==> (Crypt X K : synth H) = (Crypt X K: H)";
+goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)";
 by (Fast_tac 1);
 qed "Crypt_synth_eq";
 
@@ -660,9 +659,9 @@
 qed "Fake_parts_insert";
 
 goal thy
-     "!!H. [| Crypt Y K : parts (insert X H);  X: synth (analz G);  \
+     "!!H. [| Crypt K Y : parts (insert X H);  X: synth (analz G);  \
 \             Key K ~: analz G |]                                   \
-\          ==> Crypt Y K : parts G Un parts H";
+\          ==> Crypt K Y : parts G Un parts H";
 by (dtac (impOfSubs Fake_parts_insert) 1);
 by (assume_tac 1);
 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
@@ -699,7 +698,7 @@
 AddIffs [MPair_synth_analz];
 
 goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
-\              ==> (Crypt X K : synth (analz H)) = (X : synth (analz H))";
+\              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
 by (Fast_tac 1);
 qed "Crypt_synth_analz";
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -28,10 +28,10 @@
   isSymKey :: key=>bool
   "isSymKey K == (invKey K = K)"
 
-  (*We do not assume  Crypt (Crypt X K) (invKey K) = X
-    because Crypt is a constructor!  We assume that encryption is injective,
+  (*We do not assume  Crypt (invKey K) (Crypt K X) = X
+    because Crypt a is constructor!  We assume that encryption is injective,
     which is not true in the real world.  The alternative is to take
-    Crypt as an uninterpreted function symbol satisfying the equation
+    Crypt an as uninterpreted function symbol satisfying the equation
     above.  This seems to require moving to ZF and regarding msg as an
     inductive definition instead of a datatype.*) 
 
@@ -43,7 +43,7 @@
       | Nonce nat
       | Key   key
       | MPair msg msg
-      | Crypt msg key
+      | Crypt key msg
 
 (*Allows messages of the form {|A,B,NA|}, etc...*)
 syntax
@@ -56,7 +56,7 @@
 
 constdefs  (*Keys useful to decrypt elements of a message set*)
   keysFor :: msg set => key set
-  "keysFor H == invKey `` {K. EX X. Crypt X K : H}"
+  "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
 
 (** Inductive definition of all "parts" of a message.  **)
 
@@ -66,7 +66,7 @@
     Inj     "X: H ==> X: parts H"
     Fst     "{|X,Y|} : parts H ==> X : parts H"
     Snd     "{|X,Y|} : parts H ==> Y : parts H"
-    Body    "Crypt X K : parts H ==> X : parts H"
+    Body    "Crypt K X : parts H ==> X : parts H"
 
 
 (** Inductive definition of "analz" -- what can be broken down from a set of
@@ -79,7 +79,7 @@
     Inj     "X: H ==> X: analz H"
     Fst     "{|X,Y|} : analz H ==> X : analz H"
     Snd     "{|X,Y|} : analz H ==> Y : analz H"
-    Decrypt "[| Crypt X K : analz H; Key(invKey K): analz H |] ==> X : analz H"
+    Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H"
 
 
 (** Inductive definition of "synth" -- what can be built up from a set of
@@ -92,6 +92,6 @@
     Inj     "X: H ==> X: synth H"
     Agent   "Agent agt : synth H"
     MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
-    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt X K : synth H"
+    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
 
 end
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -20,7 +20,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX N K. EX evs: ns_shared lost.          \
-\               Says A B (Crypt {|Nonce N, Nonce N|} K) : set_of_list evs";
+\               Says A B (Crypt K {|Nonce N, Nonce N|}) : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 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);
 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -50,14 +50,14 @@
 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 (*For reasoning about the encrypted portion of message NS3*)
-goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \
+goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \
 \                ==> X : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
 qed "NS3_msg_in_parts_sees_Spy";
                               
 goal thy
-    "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs \
+    "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \
 \           ==> K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -188,11 +188,11 @@
 
 (*Describes the form of K, X and K' when the Server sends this message.*)
 goal thy 
- "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
+ "!!evs. [| Says Server A (Crypt K' {|N, Agent B, K, X|}) : set_of_list evs; \
 \           evs : ns_shared lost |]    \
 \        ==> (EX evt: ns_shared lost. \
 \                  K = Key(newK evt) & \
-\                  X = (Crypt {|K, Agent A|} (shrK B)) & \
+\                  X = (Crypt (shrK B) {|K, Agent A|}) & \
 \                  K' = shrK A)";
 by (etac rev_mp 1);
 by (etac ns_shared.induct 1);
@@ -202,13 +202,13 @@
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
- "!!evs. [| Crypt {|NA, Agent B, Key K, X|} (shrK A)                   \
+ "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|}                   \
 \            : parts (sees lost Spy evs);                              \
 \           A ~: lost;  evs : ns_shared lost |]                        \
-\         ==> X = (Crypt {|Key K, Agent A|} (shrK B)) &                \
+\         ==> X = (Crypt (shrK B) {|Key K, Agent A|}) &                \
 \             Says Server A                                            \
-\              (Crypt {|NA, Agent B, Key K,                            \
-\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
+\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
+\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set_of_list evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -220,11 +220,11 @@
   OR     reduces it to the Fake case.
   Use Says_Server_message_form if applicable.*)
 goal thy 
- "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))      \
+ "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
 \            : set_of_list evs;  evs : ns_shared lost |]                   \
 \        ==> (EX evt: ns_shared lost. K = newK evt &                       \
 \                               length evt < length evs &                  \
-\                               X = (Crypt {|Key K, Agent A|} (shrK B)))   \
+\                               X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \          | X : analz (sees lost Spy evs)";
 by (case_tac "A : lost" 1);
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
@@ -261,7 +261,7 @@
   We require that agents should behave like this subsequently also.*)
 goal thy 
  "!!evs. evs : ns_shared lost ==> \
-\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
 by (etac ns_shared.induct 1);
 by parts_Fake_tac;
@@ -314,7 +314,7 @@
 goal thy 
  "!!evs. evs : ns_shared lost ==>                                            \
 \      EX A' NA' B' X'. ALL A NA B X.                                        \
-\       Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))         \
+\       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
 \       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -333,10 +333,10 @@
 (*In messages of this form, the session key uniquely identifies the rest*)
 goal thy 
  "!!evs. [| Says Server A                                    \
-\             (Crypt {|NA, Agent B, Key K, X|} (shrK A))     \
+\             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
 \                  : set_of_list evs;                        \ 
 \           Says Server A'                                   \
-\             (Crypt {|NA', Agent B', Key K, X'|} (shrK A')) \
+\             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
 \                  : set_of_list evs;                        \
 \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
 by (dtac lemma 1);
@@ -354,8 +354,8 @@
  "!!evs. [| A ~: lost;  B ~: lost;  \
 \           evs : ns_shared lost;  evt: ns_shared lost |]  \
 \        ==> Says Server A                                             \
-\              (Crypt {|NA, Agent B, Key K,                            \
-\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
+\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
+\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set_of_list evs -->                                    \
 \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
 \        Key K ~: analz (sees lost Spy evs)";
@@ -393,7 +393,7 @@
 (*Final version: Server's message in the most abstract form*)
 goal thy 
  "!!evs. [| Says Server A                                               \
-\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
+\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
 \           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
 \        |] ==> K ~: analz (sees lost Spy evs)";
@@ -405,7 +405,7 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                          \
 \           Says Server A                                               \
-\            (Crypt {|NA, Agent B, K, X|} K') : set_of_list evs;        \
+\            (Crypt K' {|NA, Agent B, K, X|}) : set_of_list evs;        \
 \           (ALL NB. Says A Spy {|NA, NB, K|} ~: set_of_list evs);      \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
 \        ==> K ~: analz (sees lost C evs)";
@@ -424,11 +424,11 @@
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
- "!!evs. [| Crypt {|Key K, Agent A|} (shrK B) : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (sees lost Spy evs); \
 \           B ~: lost;  evs : ns_shared lost |]                        \
 \         ==> EX NA. Says Server A                                     \
-\              (Crypt {|NA, Agent B, Key K,                            \
-\                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
+\              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
+\                                Crypt (shrK B) {|Key K, Agent A|}|})  \
 \             : set_of_list evs";
 by (etac rev_mp 1);
 by (etac ns_shared.induct 1);
@@ -444,10 +444,10 @@
 goal thy
  "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
 \        ==> Key K ~: analz (sees lost Spy evs) -->             \
-\            Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
+\            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
 \            : set_of_list evs --> \
-\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->            \
-\            Says B A (Crypt (Nonce NB) K) : set_of_list evs";
+\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
+\            Says B A (Crypt K (Nonce NB)) : set_of_list evs";
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
 by parts_Fake_tac;
@@ -461,7 +461,7 @@
 by (Fast_tac 2);
 by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
 (*Contradiction from the assumption   
-   Crypt (Nonce NB) (newK evsa) : parts (sees lost Spy evsa) *)
+   Crypt (newK evsa) (Nonce NB) : parts (sees lost Spy evsa) *)
 by (dtac Crypt_imp_invKey_keysFor 1);
 (**LEVEL 10**)
 by (Asm_full_simp_tac 1);
@@ -475,12 +475,12 @@
 val lemma = result();
 
 goal thy
- "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs);           \
-\           Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
+ "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
+\           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
 \           : set_of_list evs;                                        \
 \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
-\        ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
+\        ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs";
 by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
                       addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
 qed "A_trust_NS4";
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -36,15 +36,15 @@
                the sender field.*)
     NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
              Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
-          ==> Says Server A 
-                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
-                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
-                   (shrK A)) # evs : ns_shared lost"
+          ==> Says Server A (Crypt (shrK A)
+                             {|Nonce NA, Agent B, Key (newK evs),   
+                               (Crypt (shrK B) {|Key (newK evs), Agent A|})|}) 
+                # evs : ns_shared lost"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
             Can inductively show A ~= Server*)
     NS3  "[| evs: ns_shared lost;  A ~= B;
-             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
+             Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
                : set_of_list evs;
              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
           ==> Says A B X # evs : ns_shared lost"
@@ -52,8 +52,8 @@
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
     NS4  "[| evs: ns_shared lost;  A ~= B;  
-             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
-          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
+             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
+          ==> Says B A (Crypt K (Nonce (newN evs))) # evs : ns_shared lost"
 
          (*Alice responds with Nonce NB if she has seen the key before.
            Maybe should somehow check Nonce NA again.
@@ -61,17 +61,17 @@
            Letting the Spy add or subtract 1 lets him send ALL nonces.
            Instead we distinguish the messages by sending the nonce twice.*)
     NS5  "[| evs: ns_shared lost;  A ~= B;  
-             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
-             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+             Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
+             Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set_of_list evs |]
-          ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
+          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
   
          (*This message models possible leaks of session keys.
            The two Nonces identify the protocol run: the rule insists upon
            the true senders in order to make them accurate.*)
     Oops "[| evs: ns_shared lost;  A ~= Spy;
-             Says B A (Crypt (Nonce NB) K) : set_of_list evs;
-             Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
+             Says B A (Crypt K (Nonce NB)) : set_of_list evs;
+             Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set_of_list evs |]
           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -23,7 +23,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX K. EX NA. EX evs: otway lost.          \
-\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
+\               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \                 : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -65,7 +65,7 @@
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
-goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
 \                 ==> K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -137,7 +137,7 @@
 \                Key (newK evs') ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
-				    addDs [impOfSubs analz_subset_parts,
+                                    addDs [impOfSubs analz_subset_parts,
                                            impOfSubs parts_insert_subset_Un,
                                            Suc_leD]
                                     addss (!simpset))));
@@ -167,7 +167,7 @@
                               addSEs partsEs
                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
                               addEs [leD RS notE]
-			      addDs  [impOfSubs analz_subset_parts,
+                              addDs  [impOfSubs analz_subset_parts,
                                       impOfSubs parts_insert_subset_Un,
                                       Suc_leD]
                               addss (!simpset))));
@@ -218,7 +218,7 @@
   for Oops case.*)
 goal thy 
  "!!evs. [| Says Server B \
-\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
+\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
 \           evs : otway lost |]                                   \
 \        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
 \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
@@ -284,7 +284,7 @@
 goal thy 
  "!!evs. evs : otway lost ==>                                                 \
 \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
-\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
+\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -301,9 +301,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
 \            : set_of_list evs;                                    \ 
-\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
+\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
 \            : set_of_list evs;                                    \
 \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (dtac lemma 1);
@@ -320,10 +320,10 @@
 (*Only OR1 can have caused such a part of a message to appear.*)
 goal thy 
  "!!evs. [| A ~: lost;  evs : otway lost |]                        \
-\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)               \
+\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
 \             : parts (sees lost Spy evs) -->                      \
 \            Says A B {|NA, Agent A, Agent B,                      \
-\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set_of_list evs";
 by (parts_induct_tac 1);
 qed_spec_mp "Crypt_imp_OR1";
@@ -334,7 +334,7 @@
 goal thy 
  "!!evs. [| evs : otway lost; A ~: lost |]               \
 \ ==> EX B'. ALL B.    \
-\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
+\        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
 \        --> B = B'";
 by (parts_induct_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
@@ -345,8 +345,8 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A): parts(sees lost Spy evs); \
-\          Crypt {|NA, Agent A, Agent C|} (shrK A): parts(sees lost Spy evs); \
+ "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
+\          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
 \          evs : otway lost;  A ~: lost |]                                    \
 \        ==> B = C";
 by (dtac lemma 1);
@@ -365,9 +365,9 @@
   over-simplified version of this protocol: see OtwayRees_Bad.*)
 goal thy 
  "!!evs. [| A ~: lost;  evs : otway lost |]                            \
-\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
+\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
 \             : parts (sees lost Spy evs) -->                       \
-\            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
+\            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
 \             ~: parts (sees lost Spy evs)";
 by (parts_induct_tac 1);
 by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
@@ -380,14 +380,14 @@
   to start a run, then it originated with the Server!*)
 goal thy 
  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
-\    ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs)      \
+\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
-\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}      \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
 \             : set_of_list evs -->                                    \
 \            (EX NB. Says Server B                                     \
 \                 {|NA,                                                \
-\                   Crypt {|NA, Key K|} (shrK A),                      \
-\                   Crypt {|NB, Key K|} (shrK B)|}                     \
+\                   Crypt (shrK A) {|NA, Key K|},                      \
+\                   Crypt (shrK B) {|NB, Key K|}|}                     \
 \                   : set_of_list evs)";
 by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
@@ -420,16 +420,16 @@
   bad form of this protocol, even though we can prove
   Spy_not_see_encrypted_key*)
 goal thy 
- "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
 \            : set_of_list evs;                                    \
 \           Says A B {|NA, Agent A, Agent B,                       \
-\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
+\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
 \            : set_of_list evs;                                    \
 \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
 \        ==> EX NB. Says Server B                                  \
 \                     {|NA,                                        \
-\                       Crypt {|NA, Key K|} (shrK A),              \
-\                       Crypt {|NB, Key K|} (shrK B)|}             \
+\                       Crypt (shrK A) {|NA, Key K|},              \
+\                       Crypt (shrK B) {|NB, Key K|}|}             \
 \                       : set_of_list evs";
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
@@ -444,8 +444,8 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
 \        ==> Says Server B                                                 \
-\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
-\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
+\              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
+\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
@@ -467,8 +467,8 @@
 
 goal thy 
  "!!evs. [| Says Server B \
-\            {|NA, Crypt {|NA, K|} (shrK A),                             \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
+\            {|NA, Crypt (shrK A) {|NA, K|},                             \
+\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> K ~: analz (sees lost Spy evs)";
@@ -480,8 +480,8 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                           \
 \           Says Server B                                                \
-\            {|NA, Crypt {|NA, K|} (shrK A),                             \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
+\            {|NA, Crypt (shrK A) {|NA, K|},                             \
+\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> K ~: analz (sees lost C evs)";
@@ -498,11 +498,11 @@
   know anything about X: it does NOT have to have the right form.*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
-\        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
+\        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
 \             : parts (sees lost Spy evs) -->                  \
 \            (EX X. Says B Server                              \
 \             {|NA, Agent A, Agent B, X,                       \
-\               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
+\               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
 \             : set_of_list evs)";
 by (parts_induct_tac 1);
 by (auto_tac (!claset, !simpset addcongs [conj_cong]));
@@ -514,7 +514,7 @@
 goal thy 
  "!!evs. [| evs : otway lost; B ~: lost |]               \
 \ ==> EX NA' A'. ALL NA A.                               \
-\      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
+\      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
 \      --> NA = NA' & A = A'";
 by (parts_induct_tac 1);
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
@@ -524,9 +524,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
+ "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
 \                  : parts(sees lost Spy evs);         \
-\          Crypt {|NC, NB, Agent C, Agent B|} (shrK B) \
+\          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
 \                  : parts(sees lost Spy evs);         \
 \          evs : otway lost;  B ~: lost |]             \
 \        ==> NC = NA & C = A";
@@ -543,14 +543,14 @@
   then it originated with the Server!*)
 goal thy 
  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
-\    ==> Crypt {|NB, Key K|} (shrK B) : parts (sees lost Spy evs)        \
+\    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
 \        --> (ALL X'. Says B Server                                      \
 \                       {|NA, Agent A, Agent B, X',                      \
-\                         Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
+\                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
 \             : set_of_list evs                                          \
 \             --> Says Server B                                          \
-\                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
-\                        Crypt {|NB, Key K|} (shrK B)|}                  \
+\                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
+\                        Crypt (shrK B) {|NB, Key K|}|}                  \
 \                   : set_of_list evs)";
 by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
@@ -577,16 +577,15 @@
   has sent the correct message.*)
 goal thy 
  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
-\           Says S B {|NA, X, Crypt {|NB, Key K|} (shrK B)|}       \
+\           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
 \            : set_of_list evs;                                    \
 \           Says B Server {|NA, Agent A, Agent B, X',              \
-\                           Crypt {|NA, NB, Agent A, Agent B|}     \
-\                                 (shrK B)|}                       \
+\                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \            : set_of_list evs |]                                  \
 \        ==> Says Server B                                         \
 \                 {|NA,                                            \
-\                   Crypt {|NA, Key K|} (shrK A),                  \
-\                   Crypt {|NB, Key K|} (shrK B)|}                 \
+\                   Crypt (shrK A) {|NA, Key K|},                  \
+\                   Crypt (shrK B) {|NB, Key K|}|}                 \
 \                   : set_of_list evs";
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
@@ -600,15 +599,14 @@
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
 \        ==> Says Server B                                            \
-\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
-\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
+\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
-\                            Crypt {|NA, NB, Agent A, Agent B|}       \
-\                                  (shrK B)|}                         \
+\                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \            : set_of_list evs)";
 by (etac otway.induct 1);
 by (Auto_tac());
-bd (Says_imp_sees_Spy RS parts.Inj) 1;
+by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
 
@@ -617,18 +615,15 @@
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.*)
 goal thy 
- "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
 \            : set_of_list evs;                                    \
 \           Says A B {|NA, Agent A, Agent B,                       \
-\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
+\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
 \            : set_of_list evs;                                    \
 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
-\                                     Crypt {|NA, NB, Agent A, Agent B|}    \
-\                                           (shrK B)|}                      \
+\                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
 \            : set_of_list evs";
 by (fast_tac (!claset addSDs  [A_trust_OR4]
-	              addSEs [OR3_imp_OR2]) 1);
+                      addSEs [OR3_imp_OR2]) 1);
 qed "A_auths_B";
-
-
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -30,8 +30,8 @@
          (*Alice initiates a protocol run*)
     OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
           ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
-                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
-                               (shrK A) |} 
+                         Crypt (shrK A)
+                               {|Nonce (newN evs), Agent A, Agent B|} |} 
                  # evs : otway lost"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
@@ -41,8 +41,8 @@
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, 
-                    Crypt {|Nonce NA, Nonce (newN evs), 
-                            Agent A, Agent B|} (shrK B)|}
+                    Crypt 
+                          (shrK B){|Nonce NA, Nonce (newN evs), Agent A, Agent B|}|}
                  # evs : otway lost"
 
          (*The Server receives Bob's message and checks that the three NAs
@@ -51,30 +51,30 @@
     OR3  "[| evs: otway lost;  B ~= Server;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
-                    Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|}
+                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
+                    Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set_of_list evs |]
           ==> Says Server B 
                   {|Nonce NA, 
-                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
-                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
+                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
                  # evs : otway lost"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
     OR4  "[| evs: otway lost;  A ~= B;  
-             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs;
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
-                             Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} 
-                                   (shrK B)|}
+                             Crypt (shrK B)
+                                   {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set_of_list evs |]
           ==> Says B A {|Nonce NA, X|} # evs : otway lost"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
     Oops "[| evs: otway lost;  B ~= Spy;
-             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs |]
           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -22,7 +22,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX K. EX NA. EX evs: otway lost.          \
-\             Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
+\             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \             : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -59,7 +59,7 @@
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
-goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
+goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
 \                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -176,8 +176,8 @@
 (*Describes the form of K and NA when the Server sends this message.*)
 goal thy 
  "!!evs. [| Says Server B \
-\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
-\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
+\           {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\             Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs; \
 \           evs : otway lost |]                                        \
 \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
 \            (EX i. NA = Nonce i) &                  \
@@ -246,8 +246,8 @@
  "!!evs. evs : otway lost ==>                      \
 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
 \       Says Server B \
-\         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
-\           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
+\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -266,12 +266,12 @@
 
 goal thy 
 "!!evs. [| Says Server B                                           \
-\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
-\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
+\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
+\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
 \           : set_of_list evs;                                     \
 \          Says Server B'                                          \
-\            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
-\              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
+\            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
+\              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
 \           : set_of_list evs;                                     \
 \          evs : otway lost |]                                     \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -289,11 +289,11 @@
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
-\ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
+\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}        \
 \      : parts (sees lost Spy evs)                          \
 \     --> (EX NB. Says Server B                                     \
-\                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
-\                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
+\                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
+\                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                  : set_of_list evs)";
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -308,12 +308,12 @@
   Spy_not_see_encrypted_key.  (We can implicitly infer freshness of
   the Server's message from its nonce NA.)*)
 goal thy 
- "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
+ "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
 \            : set_of_list evs;                                         \
 \           A ~: lost;  evs : otway lost |]                             \
 \        ==> EX NB. Says Server B                                       \
-\                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
-\                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
+\                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
+\                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
 \                   : set_of_list evs";
 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
@@ -328,8 +328,8 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
 \        ==> Says Server B                                                 \
-\             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
-\               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
+\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
+\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
 \            : set_of_list evs -->                                         \
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
 \            Key K ~: analz (sees lost Spy evs)";
@@ -351,8 +351,8 @@
 
 goal thy 
  "!!evs. [| Says Server B                                                     \
-\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
-\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
+\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
 \        ==> K ~: analz (sees lost Spy evs)";
@@ -364,8 +364,8 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                                \
 \           Says Server B                                                     \
-\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
-\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
+\            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                    \
+\              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs;\
 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> K ~: analz (sees lost C evs)";
@@ -381,11 +381,11 @@
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost |]                                 \
-\    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)                     \
+\    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}                     \
 \         : parts (sees lost Spy evs)                                       \
 \        --> (EX NA. Says Server B                                          \
-\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
-\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
+\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
+\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set_of_list evs)";
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
@@ -398,11 +398,11 @@
   has sent the correct message.*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
-\           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}  \
+\           Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}  \
 \            : set_of_list evs |]                                           \
 \        ==> EX NA. Says Server B                                           \
-\                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
-\                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
+\                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
+\                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
 \                     : set_of_list evs";
 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
                       addEs  partsEs
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -45,15 +45,15 @@
              Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set_of_list evs |]
           ==> Says Server B 
-               {|Crypt {|Nonce NA, Agent A, Agent B, Key(newK evs)|} (shrK A),
-                 Crypt {|Nonce NB, Agent A, Agent B, Key(newK evs)|} (shrK B)|}
+               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key(newK evs)|},
+                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key(newK evs)|}|}
               # evs : otway lost"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
     OR4  "[| evs: otway lost;  A ~= B;
              Says S B {|X, 
-                        Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
+                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
                : set_of_list evs;
              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                : set_of_list evs |]
@@ -63,8 +63,8 @@
            identify the protocol run.  B is not assumed to know shrK A.*)
     Oops "[| evs: otway lost;  B ~= Spy;
              Says Server B 
-                      {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), 
-                        Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
+                      {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
+                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
                : set_of_list evs |]
           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -25,7 +25,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX K. EX NA. EX evs: otway.          \
-\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
+\               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \                 : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
@@ -68,7 +68,7 @@
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "OR4_analz_sees_Spy";
 
-goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
+goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
 \                 ==> K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
@@ -218,7 +218,7 @@
   for Oops case.*)
 goal thy 
  "!!evs. [| Says Server B \
-\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
+\            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
 \           evs : otway |]                                   \
 \        ==> (EX evt: otway. K = Key(newK evt)) &            \
 \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
@@ -295,7 +295,7 @@
 goal thy 
  "!!evs. evs : otway ==>                                                 \
 \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
-\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
+\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -312,9 +312,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
 \            : set_of_list evs;                                    \ 
-\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
+\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
 \            : set_of_list evs;                                    \
 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (dtac lemma 1);
@@ -329,8 +329,8 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
 \        ==> Says Server B                                            \
-\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
-\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
+\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->      \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
@@ -353,8 +353,8 @@
 
 goal thy 
  "!!evs. [| Says Server B                                         \
-\            {|NA, Crypt {|NA, K|} (shrK A),                      \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
+\            {|NA, Crypt (shrK A) {|NA, K|},                      \
+\                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
 \            Says B Spy {|NA, NB, K|} ~: set_of_list evs;         \
 \           A ~: lost;  B ~: lost;  evs : otway |]                \
 \        ==> K ~: analz (sees lost Spy evs)";
@@ -371,10 +371,10 @@
 	this version.*)
 goal thy 
  "!!evs. [| A ~: lost;  A ~= B; evs : otway |]                 \
-\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)           \
+\        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
 \             : parts (sees lost Spy evs) -->                  \
 \            Says A B {|NA, Agent A, Agent B,                  \
-\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set_of_list evs";
 by (parts_induct_tac 1);
 by (Fast_tac 1);
@@ -387,14 +387,14 @@
           substituting some other nonce NA' for NB.*)
 goal thy 
  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                        \
-\        ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
+\        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
 \            Says A B {|NA, Agent A, Agent B,                  \
-\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
 \             : set_of_list evs -->                            \
 \            (EX B NB. Says Server B                           \
 \                 {|NA,                                        \
-\                   Crypt {|NA, Key K|} (shrK A),              \
-\                   Crypt {|NB, Key K|} (shrK B)|}             \
+\                   Crypt (shrK A) {|NA, Key K|},              \
+\                   Crypt (shrK B) {|NB, Key K|}|}             \
 \                   : set_of_list evs)";
 by (parts_induct_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
@@ -415,12 +415,12 @@
   in two different roles:
           Says B' Server
            {|Nonce NAa, Agent Aa, Agent A,
-             Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK Aa), Nonce NA,
-             Crypt {|Nonce NAa, Agent Aa, Agent A|} (shrK A)|}
+             Crypt (shrK Aa) {|Nonce NAa, Agent Aa, Agent A|}, Nonce NA,
+             Crypt (shrK A) {|Nonce NAa, Agent Aa, Agent A|}|}
           : set_of_list evsa;
           Says A B
            {|Nonce NA, Agent A, Agent B,
-             Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}|}
           : set_of_list evsa 
 *)
 writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -29,8 +29,8 @@
          (*Alice initiates a protocol run*)
     OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
           ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
-                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
-                               (shrK A) |} 
+                         Crypt (shrK A) 
+                               {|Nonce (newN evs), Agent A, Agent B|} |} 
                  # evs : otway"
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
@@ -40,7 +40,7 @@
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
           ==> Says B Server 
                   {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                  # evs : otway"
 
          (*The Server receives Bob's message and checks that the three NAs
@@ -49,20 +49,20 @@
     OR3  "[| evs: otway;  B ~= Server;
              Says B' Server 
                   {|Nonce NA, Agent A, Agent B, 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
+                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
                     Nonce NB, 
-                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+                    Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                : set_of_list evs |]
           ==> Says Server B 
                   {|Nonce NA, 
-                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
-                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+                    Crypt (shrK A) {|Nonce NA, Key (newK evs)|},
+                    Crypt (shrK B) {|Nonce NB, Key (newK evs)|}|}
                  # evs : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
     OR4  "[| evs: otway;  A ~= B;
-             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+             Says S B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs;
              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
                : set_of_list evs |]
@@ -71,7 +71,7 @@
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
     Oops "[| evs: otway;  B ~= Spy;
-             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set_of_list evs |]
           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Shared.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -120,7 +120,7 @@
 AddSIs [sees_own_shrK, Spy_sees_lost];
 
 (*Added for Yahalom/lost_tac*)
-goal thy "!!A. [| Crypt X (shrK A) : analz (sees lost Spy evs);  A: lost |] \
+goal thy "!!A. [| Crypt (shrK A) X : analz (sees lost Spy evs);  A: lost |] \
 \              ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
 qed "Crypt_Spy_analz_lost";
@@ -172,14 +172,14 @@
 qed_spec_mp "Says_imp_sees_Spy";
 
 goal thy  
- "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;  C : lost |] \
+ "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
 \        ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
                       addss (!simpset)) 1);
 qed "Says_Crypt_lost";
 
 goal thy  
- "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs;        \
+ "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;        \
 \           X ~: analz (sees lost Spy evs) |]                     \
 \        ==> C ~: lost";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -22,7 +22,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX X NB K. EX evs: yahalom lost.          \
-\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -54,7 +54,7 @@
 (** For reasoning about the encrypted portion of messages **)
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
@@ -63,7 +63,7 @@
           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
 (*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
+goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
 \                  : set_of_list evs ==> \
 \                K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
@@ -145,7 +145,7 @@
 
 
 (*Ready-made for the classical reasoner*)
-goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|}  \
+goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|}  \
 \                   : set_of_list evs;  evs : yahalom lost |]              \
 \                ==> R";
 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
@@ -189,7 +189,7 @@
   Oops as well as main secrecy property.*)
 goal thy 
  "!!evs. [| Says Server A                                           \
-\            {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
+\            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
 \           evs : yahalom lost |]                                   \
 \        ==> (EX evt: yahalom lost. K = Key(newK evt))";
 by (etac rev_mp 1);
@@ -222,7 +222,7 @@
   We require that agents should behave like this subsequently also.*)
 goal thy 
  "!!evs. evs : yahalom lost ==> \
-\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
+\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by parts_Fake_tac;
@@ -273,7 +273,7 @@
  "!!evs. evs : yahalom lost ==>                                     \
 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
 \          Says Server A                                            \
-\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
+\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac yahalom.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -289,10 +289,10 @@
 
 goal thy 
 "!!evs. [| Says Server A                                            \
-\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
+\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
 \           : set_of_list evs;                                      \
 \          Says Server A'                                           \
-\           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|}   \
+\           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
 \           : set_of_list evs;                                      \
 \          evs : yahalom lost |]                                    \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -306,12 +306,12 @@
 
 (*If the encrypted message appears then it originated with the Server*)
 goal thy
- "!!evs. [| Crypt {|Agent B, Key K, NA, NB|} (shrK A)                  \
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
 \            : parts (sees lost Spy evs);                              \
 \           A ~: lost;  evs : yahalom lost |]                          \
 \         ==> Says Server A                                            \
-\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
-\                Crypt {|Agent A, Key K|} (shrK B)|}                   \
+\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
+\                Crypt (shrK B) {|Agent A, Key K|}|}                   \
 \             : set_of_list evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -323,8 +323,8 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Says Server A                                        \
-\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),       \
-\                Crypt {|Agent A, Key K|} (shrK B)|}              \
+\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
+\                Crypt (shrK B) {|Agent A, Key K|}|}              \
 \             : set_of_list evs -->                               \
 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
 \            Key K ~: analz (sees lost Spy evs)";
@@ -349,8 +349,8 @@
 (*Final version: Server's message in the most abstract form*)
 goal thy 
  "!!evs. [| Says Server A                                               \
-\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
-\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
+\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
+\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
 \     K ~: analz (sees lost Spy evs)";
@@ -362,8 +362,8 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                          \
 \           Says Server A                                               \
-\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
-\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
+\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
+\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
 \     K ~: analz (sees lost C evs)";
@@ -379,12 +379,12 @@
 (*B knows, by the first part of A's message, that the Server distributed 
   the key for A and B.  But this part says nothing about nonces.*)
 goal thy 
- "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
 \           B ~: lost;  evs : yahalom lost |]                           \
 \        ==> EX NA NB. Says Server A                                    \
-\                        {|Crypt {|Agent B, Key K,                      \
-\                                  Nonce NA, Nonce NB|} (shrK A),       \
-\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
+\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
+\                                  Nonce NA, Nonce NB|},       \
+\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -429,7 +429,7 @@
 
 goal thy 
  "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
-\      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
+\      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
 by (parts_induct_tac 1);  (*100 seconds??*)
 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
@@ -439,9 +439,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
+ "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
 \                  : parts (sees lost Spy evs);         \
-\          Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
+\          Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
 \                  : parts (sees lost Spy evs);         \
 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
 \        ==> NA' = NA & A' = A & B' = B";
@@ -473,9 +473,9 @@
 
 (*Variant useful for proving secrecy of NB*)
 goal thy 
- "!!evs.[| Says C D   {|X,  Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
+ "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
 \          : set_of_list evs;  B ~: lost;         \
-\          Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
+\          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
 \          : set_of_list evs;                           \
 \          NB ~: analz (sees lost Spy evs);             \
 \          evs : yahalom lost |]  \
@@ -489,8 +489,8 @@
 goal thy 
  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
 \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
-\      Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
-\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
+\      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
+\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by parts_Fake_tac;
 by (REPEAT_FIRST 
@@ -519,11 +519,11 @@
 goal thy 
  "!!evs. evs : yahalom lost                                             \
 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
-\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
+\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
 \            (EX A B NA. Says Server A                                  \
-\                        {|Crypt {|Agent B, Key K,                      \
-\                                  Nonce NA, Nonce NB|} (shrK A),       \
-\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
+\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
+\                                  Nonce NA, Nonce NB|},       \
+\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs)";
 by (etac yahalom.induct 1);
 by parts_Fake_tac;
@@ -552,11 +552,11 @@
 goal thy 
  "!!evs. evs : yahalom lost                                             \
 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
-\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
+\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
 \            (EX A B NA. Says Server A                                  \
-\                        {|Crypt {|Agent B, Key K,                      \
-\                                  Nonce NA, Nonce NB|} (shrK A),       \
-\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
+\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
+\                                  Nonce NA, Nonce NB|},       \
+\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
 \                       : set_of_list evs)";
 by (etac yahalom.induct 1);
 by parts_Fake_tac;
@@ -580,10 +580,10 @@
 (*YM3 can only be triggered by YM2*)
 goal thy 
  "!!evs. [| Says Server A                                           \
-\            {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
+\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
 \           evs : yahalom lost |]                                        \
 \        ==> EX B'. Says B' Server                                       \
-\                      {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
+\                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
 \                   : set_of_list evs";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
@@ -622,7 +622,7 @@
 \     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
 \     (EX K: newK``E. EX A B na X.                                        \
 \            Says Server A                                                \
-\                {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|}   \
+\                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
 \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_Fake_tac;
@@ -673,7 +673,7 @@
   for the induction to carry through.*)
 goal thy 
  "!!evs. [| Says Server A                                                     \
-\            {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
+\            {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
 \           : set_of_list evs;                                                \
 \           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
 \           evs : yahalom lost |]                                             \
@@ -688,7 +688,7 @@
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
 \ ==> Says B Server                                                    \
-\          {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
+\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
 \     : set_of_list evs -->                               \
 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
 \     Nonce NB ~: analz (sees lost Spy evs)";
@@ -757,16 +757,16 @@
   nonces are forced to agree with NA and NB). *)
 goal thy 
  "!!evs. [| Says B Server                                        \
-\            {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}  \
+\            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
 \           : set_of_list evs;       \
-\           Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
-\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
+\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
+\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
 \         ==> Says Server A                                       \
-\                     {|Crypt {|Agent B, Key K,                         \
-\                               Nonce NA, Nonce NB|} (shrK A),          \
-\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
+\                     {|Crypt (shrK A) {|Agent B, Key K,                         \
+\                               Nonce NA, Nonce NB|},          \
+\                       Crypt (shrK B) {|Agent A, Key K|}|}             \
 \                   : set_of_list evs";
 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -35,35 +35,35 @@
              Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
           ==> Says B Server 
                   {|Agent B, 
-                    Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
+                    Crypt (shrK B) {|Agent A, Nonce NA, Nonce (newN evs)|}|}
                  # evs : yahalom lost"
 
          (*The Server receives Bob's message.  He responds by sending a
             new session key to Alice, with a packet for forwarding to Bob.*)
     YM3  "[| evs: yahalom lost;  A ~= Server;
              Says B' Server 
-                  {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
+                  {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
                : set_of_list evs |]
           ==> Says Server A
-                  {|Crypt {|Agent B, Key (newK evs), 
-                            Nonce NA, Nonce NB|} (shrK A),
-                    Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
+                  {|Crypt (shrK A) {|Agent B, Key (newK evs), 
+                            Nonce NA, Nonce NB|},
+                    Crypt (shrK B) {|Agent A, Key (newK evs)|}|}
                  # evs : yahalom lost"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
-             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+             Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
                         X|}  : set_of_list evs;
              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
-          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
 
          (*This message models possible leaks of session keys.  The Nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct.*)
     Oops "[| evs: yahalom lost;  A ~= Spy;
-             Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
-                                   (shrK A),
+             Says Server A {|Crypt (shrK A)
+                                   {|Agent B, Key K, Nonce NA, Nonce NB|},
                              X|}  : set_of_list evs |]
           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
 
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Fri Nov 29 18:03:21 1996 +0100
@@ -23,7 +23,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX X NB K. EX evs: yahalom lost.          \
-\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
@@ -55,7 +55,7 @@
 (** For reasoning about the encrypted portion of messages **)
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
-goal thy "!!evs. Says S A {|NB, Crypt Y (shrK A), X|} : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
 \                X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
 qed "YM4_analz_sees_Spy";
@@ -64,7 +64,7 @@
           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
 (*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|NB, Crypt {|B, K, NA|} (shrK A), X|} \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
 \                  : set_of_list evs ==> \
 \                K : parts (sees lost Spy evs)";
 by (fast_tac (!claset addSEs partsEs
@@ -187,7 +187,7 @@
 (*Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.*)
 goal thy 
- "!!evs. [| Says Server A {|NB', Crypt {|Agent B, K, NA|} (shrK A), X|} \
+ "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, K, NA|}, X|} \
 \            : set_of_list evs;                                         \
 \           evs : yahalom lost |]                                       \
 \        ==> (EX evt: yahalom lost. K = Key(newK evt)) & A ~= B";
@@ -251,7 +251,7 @@
  "!!evs. evs : yahalom lost ==>                                     \
 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                        \
 \          Says Server A                                            \
-\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
+\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac yahalom.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -267,10 +267,10 @@
 
 goal thy 
 "!!evs. [| Says Server A                                            \
-\           {|NB, Crypt {|Agent B, Key K, NA|} (shrK A), X|}        \
+\           {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, X|}        \
 \           : set_of_list evs;                                      \
 \          Says Server A'                                           \
-\           {|NB', Crypt {|Agent B', Key K, NA'|} (shrK A'), X'|}   \
+\           {|NB', Crypt (shrK A') {|Agent B', Key K, NA'|}, X'|}   \
 \           : set_of_list evs;                                      \
 \          evs : yahalom lost |]                                    \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
@@ -288,8 +288,8 @@
  "!!evs. [| A ~: lost;  B ~: lost;  A ~= B;                          \
 \           evs : yahalom lost |]            \
 \        ==> Says Server A                                           \
-\              {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),           \
-\                    Crypt {|NB, Key K, Agent A|} (shrK B)|}          \
+\              {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},           \
+\                    Crypt (shrK B) {|NB, Key K, Agent A|}|}          \
 \             : set_of_list evs -->                               \
 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
 \            Key K ~: analz (sees lost Spy evs)";
@@ -316,8 +316,8 @@
 (*Final version: Server's message in the most abstract form*)
 goal thy 
  "!!evs. [| Says Server A                                         \
-\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
-\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
+\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
+\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
 \           : set_of_list evs;                                    \
 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
@@ -330,8 +330,8 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                    \
 \           Says Server A                                         \
-\              {|NB, Crypt {|Agent B, K, NA|} (shrK A),           \
-\                    Crypt {|NB, K, Agent A|} (shrK B)|}          \
+\              {|NB, Crypt (shrK A) {|Agent B, K, NA|},           \
+\                    Crypt (shrK B) {|NB, K, Agent A|}|}          \
 \           : set_of_list evs;                                    \
 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;          \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
@@ -347,12 +347,12 @@
 
 (*If the encrypted message appears then it originated with the Server.*)
 goal thy
- "!!evs. [| Crypt {|Agent B, Key K, NA|} (shrK A)                \
+ "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA|}                \
 \            : parts (sees lost Spy evs);                              \
 \           A ~: lost;  evs : yahalom lost |]                          \
 \         ==> EX NB. Says Server A                                     \
-\                      {|NB, Crypt {|Agent B, Key K, NA|} (shrK A),    \
-\                            Crypt {|NB, Key K, Agent A|} (shrK B)|}   \
+\                      {|NB, Crypt (shrK A) {|Agent B, Key K, NA|},    \
+\                            Crypt (shrK B) {|NB, Key K, Agent A|}|}   \
 \                    : set_of_list evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -364,13 +364,13 @@
 (*B knows, by the first part of A's message, that the Server distributed 
   the key for A and B. *)
 goal thy 
- "!!evs. [| Crypt {|Nonce NB, Key K, Agent A|} (shrK B)              \
+ "!!evs. [| Crypt (shrK B) {|Nonce NB, Key K, Agent A|}              \
 \            : parts (sees lost Spy evs);                            \
 \           B ~: lost;  evs : yahalom lost |]                        \
 \        ==> EX NA. Says Server A                                    \
 \                    {|Nonce NB,                                     \
-\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),  \
-\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|} \
+\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
+\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
 \                       : set_of_list evs";
 by (etac rev_mp 1);
 by (parts_induct_tac 1);
@@ -385,13 +385,13 @@
 (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
   because we do not have to show that NB is secret. *)
 goal thy 
- "!!evs. [| Says A' B {|Crypt {|Nonce NB, Key K, Agent A|} (shrK B),    \
-\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
+ "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
+\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
 \        ==> EX NA. Says Server A                                       \
 \                    {|Nonce NB,                                        \
-\                      Crypt {|Agent B, Key K, Nonce NA|} (shrK A),     \
-\                      Crypt {|Nonce NB, Key K, Agent A|} (shrK B)|}    \
+\                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},     \
+\                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}    \
 \                   : set_of_list evs";
 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
 by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
diff -r 68829cf138fc -r 80ebd1a213fd src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 17:58:18 1996 +0100
+++ b/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 18:03:21 1996 +0100
@@ -48,25 +48,25 @@
                : set_of_list evs |]
           ==> Says Server A
                {|Nonce NB, 
-                 Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
-                 Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
+                 Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
+                 Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
                  # evs : yahalom lost"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
            uses the new session key to send Bob his Nonce.*)
     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
-             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
+             Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                         X|}
                : set_of_list evs;
              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
-          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
+          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct. *)
     Oops "[| evs: yahalom lost;  A ~= Spy;
              Says Server A {|Nonce NB, 
-                             Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
+                             Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                              X|}  : set_of_list evs |]
           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"