Corrected indentations and margins after the renaming of "set_of_list"
authorpaulson
Fri Jun 27 10:47:13 1997 +0200 (1997-06-27)
changeset 346630791e5a69c4
parent 3465 e85c24717cad
child 3467 a0797ba03dfe
Corrected indentations and margins after the renaming of "set_of_list"
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Thu Jun 26 13:20:50 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Jun 27 10:47:13 1997 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  
     1.5  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
     1.6  goal thy 
     1.7 - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
     1.8 + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
     1.9  \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
    1.10  \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
    1.11  by (etac rev_mp 1);
    1.12 @@ -157,11 +157,11 @@
    1.13  (*Authentication for A: if she receives message 2 and has used NA
    1.14    to start a run, then B has sent message 2.*)
    1.15  goal thy 
    1.16 - "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
    1.17 -\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.18 -\             : set evs;\
    1.19 -\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
    1.20 -\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.21 + "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
    1.22 +\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
    1.23 +\             : set evs;                                               \
    1.24 +\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    1.25 +\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
    1.26  \              : set evs";
    1.27  by (etac rev_mp 1);
    1.28  (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
    1.29 @@ -237,7 +237,7 @@
    1.30  (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
    1.31  goal thy 
    1.32   "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.33 -\             : set evs;                                      \
    1.34 +\             : set evs;                                              \
    1.35  \           A ~: lost;  B ~: lost;  evs : ns_public |]                \
    1.36  \ ==> Nonce NB ~: analz (sees lost Spy evs)";
    1.37  by (etac rev_mp 1);
    1.38 @@ -262,8 +262,8 @@
    1.39    in message 2, then A has sent message 3.*)
    1.40  goal thy 
    1.41   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.42 -\             : set evs;                                       \
    1.43 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    1.44 +\             : set evs;                                               \
    1.45 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
    1.46  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    1.47  \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    1.48  by (etac rev_mp 1);
    1.49 @@ -294,8 +294,8 @@
    1.50    NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
    1.51  goal thy 
    1.52   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
    1.53 -\             : set evs;                                       \
    1.54 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    1.55 +\             : set evs;                                               \
    1.56 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
    1.57  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    1.58  \    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
    1.59  by (etac rev_mp 1);
     2.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Jun 26 13:20:50 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Public.thy	Fri Jun 27 10:47:13 1997 +0200
     2.3 @@ -31,8 +31,7 @@
     2.4  
     2.5           (*Bob responds to Alice's message with a further nonce*)
     2.6      NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
     2.7 -             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
     2.8 -               : set evs |]
     2.9 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    2.10            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    2.11                  # evs  :  ns_public"
    2.12  
     3.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jun 27 10:47:13 1997 +0200
     3.3 @@ -139,7 +139,7 @@
     3.4  
     3.5  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
     3.6  goal thy 
     3.7 - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
     3.8 + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
     3.9  \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
    3.10  \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
    3.11  by (etac rev_mp 1);
    3.12 @@ -162,9 +162,9 @@
    3.13  (*Authentication for A: if she receives message 2 and has used NA
    3.14    to start a run, then B has sent message 2.*)
    3.15  goal thy 
    3.16 - "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
    3.17 -\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;\
    3.18 -\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
    3.19 + "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
    3.20 +\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
    3.21 +\           A ~: lost;  B ~: lost;  evs : ns_public |]                  \
    3.22  \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
    3.23  by (etac rev_mp 1);
    3.24  (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
    3.25 @@ -240,9 +240,9 @@
    3.26  
    3.27  (*NB remains secret PROVIDED Alice never responds with round 3*)
    3.28  goal thy 
    3.29 - "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;\
    3.30 -\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);  \
    3.31 -\          A ~: lost;  B ~: lost;  evs : ns_public |]   \
    3.32 + "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;  \
    3.33 +\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);    \
    3.34 +\          A ~: lost;  B ~: lost;  evs : ns_public |]                   \
    3.35  \       ==> Nonce NB ~: analz (sees lost Spy evs)";
    3.36  by (etac rev_mp 1);
    3.37  by (etac rev_mp 1);
    3.38 @@ -270,8 +270,8 @@
    3.39    in message 2, then A has sent message 3--to somebody....*)
    3.40  goal thy 
    3.41   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|})          \
    3.42 -\             : set evs;                                       \
    3.43 -\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
    3.44 +\             : set evs;                                               \
    3.45 +\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
    3.46  \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
    3.47  \        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
    3.48  by (etac rev_mp 1);
    3.49 @@ -294,7 +294,7 @@
    3.50  
    3.51  (*Can we strengthen the secrecy theorem?  NO*)
    3.52  goal thy 
    3.53 - "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
    3.54 + "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]           \
    3.55  \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
    3.56  \     --> Nonce NB ~: analz (sees lost Spy evs)";
    3.57  by (analz_induct_tac 1);
     4.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jun 26 13:20:50 1997 +0200
     4.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Jun 27 10:47:13 1997 +0200
     4.3 @@ -21,7 +21,7 @@
     4.4  
     4.5  (*A "possibility property": there are traces that reach the end*)
     4.6  goal thy 
     4.7 - "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     4.8 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
     4.9  \        ==> EX N K. EX evs: ns_shared lost.          \
    4.10  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    4.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    4.12 @@ -38,7 +38,7 @@
    4.13  by (rtac subsetI 1);
    4.14  by (etac ns_shared.induct 1);
    4.15  by (REPEAT_FIRST
    4.16 -    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    4.17 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    4.18                                :: ns_shared.intrs))));
    4.19  qed "ns_shared_mono";
    4.20  
    4.21 @@ -128,7 +128,7 @@
    4.22  (*Describes the form of K, X and K' when the Server sends this message.*)
    4.23  goal thy 
    4.24   "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
    4.25 -\             : set evs;                              \
    4.26 +\             : set evs;                                      \
    4.27  \           evs : ns_shared lost |]                           \
    4.28  \        ==> K ~: range shrK &                                \
    4.29  \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
    4.30 @@ -161,7 +161,7 @@
    4.31    Use Says_Server_message_form if applicable.*)
    4.32  goal thy 
    4.33   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
    4.34 -\            : set evs;  evs : ns_shared lost |]                   \
    4.35 +\            : set evs;          evs : ns_shared lost |]                   \
    4.36  \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
    4.37  \            | X : analz (sees lost Spy evs)";
    4.38  by (case_tac "A : lost" 1);
    4.39 @@ -195,9 +195,9 @@
    4.40    to encrypt messages containing other keys, in the actual protocol.
    4.41    We require that agents should behave like this subsequently also.*)
    4.42  goal thy 
    4.43 - "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
    4.44 -\        (Crypt KAB X) : parts (sees lost Spy evs) & \
    4.45 -\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    4.46 + "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
    4.47 +\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
    4.48 +\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    4.49  by parts_induct_tac;
    4.50  (*Deals with Faked messages*)
    4.51  by (blast_tac (!claset addSEs partsEs
    4.52 @@ -211,9 +211,9 @@
    4.53  
    4.54  (*The equality makes the induction hypothesis easier to apply*)
    4.55  goal thy  
    4.56 - "!!evs. evs : ns_shared lost ==> \
    4.57 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    4.58 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    4.59 + "!!evs. evs : ns_shared lost ==>                                \
    4.60 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
    4.61 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
    4.62  \            (K : KK | Key K : analz (sees lost Spy evs))";
    4.63  by (etac ns_shared.induct 1);
    4.64  by analz_sees_tac;
    4.65 @@ -242,7 +242,7 @@
    4.66   "!!evs. evs : ns_shared lost ==>                                        \
    4.67  \      EX A' NA' B' X'. ALL A NA B X.                                    \
    4.68  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
    4.69 -\       : set evs --> A=A' & NA=NA' & B=B' & X=X'";
    4.70 +\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
    4.71  by (etac ns_shared.induct 1);
    4.72  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    4.73  by (Step_tac 1);
    4.74 @@ -260,10 +260,10 @@
    4.75  goal thy 
    4.76   "!!evs. [| Says Server A                                    \
    4.77  \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
    4.78 -\                  : set evs;                        \ 
    4.79 +\                  : set evs;                                \ 
    4.80  \           Says Server A'                                   \
    4.81  \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
    4.82 -\                  : set evs;                        \
    4.83 +\                  : set evs;                                \
    4.84  \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
    4.85  by (prove_unique_tac lemma 1);
    4.86  qed "unique_session_keys";
    4.87 @@ -276,8 +276,8 @@
    4.88  \        ==> Says Server A                                             \
    4.89  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
    4.90  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
    4.91 -\             : set evs -->                                    \
    4.92 -\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
    4.93 +\             : set evs -->                                            \
    4.94 +\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
    4.95  \        Key K ~: analz (sees lost Spy evs)";
    4.96  by (etac ns_shared.induct 1);
    4.97  by analz_sees_tac;
    4.98 @@ -308,8 +308,8 @@
    4.99  (*Final version: Server's message in the most abstract form*)
   4.100  goal thy 
   4.101   "!!evs. [| Says Server A                                               \
   4.102 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
   4.103 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
   4.104 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   4.105 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   4.106  \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
   4.107  \        |] ==> Key K ~: analz (sees lost Spy evs)";
   4.108  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   4.109 @@ -320,8 +320,8 @@
   4.110  goal thy 
   4.111   "!!evs. [| C ~: {A,B,Server};                                          \
   4.112  \           Says Server A                                               \
   4.113 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
   4.114 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
   4.115 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   4.116 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   4.117  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
   4.118  \        ==> Key K ~: analz (sees lost C evs)";
   4.119  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   4.120 @@ -354,11 +354,11 @@
   4.121  
   4.122  
   4.123  goal thy
   4.124 - "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
   4.125 -\        ==> Key K ~: analz (sees lost Spy evs) -->             \
   4.126 + "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
   4.127 +\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
   4.128  \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   4.129 -\            : set evs --> \
   4.130 -\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
   4.131 +\            : set evs -->                                             \
   4.132 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
   4.133  \            Says B A (Crypt K (Nonce NB)) : set evs";
   4.134  by (etac ns_shared.induct 1);
   4.135  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   4.136 @@ -390,8 +390,8 @@
   4.137  goal thy
   4.138   "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
   4.139  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   4.140 -\           : set evs;                                        \
   4.141 -\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;  \
   4.142 +\           : set evs;                                                \
   4.143 +\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
   4.144  \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   4.145  \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   4.146  by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
     5.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 13:20:50 1997 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Jun 27 10:47:13 1997 +0200
     5.3 @@ -150,7 +150,7 @@
     5.4    for Oops case.*)
     5.5  goal thy 
     5.6   "!!evs. [| Says Server B                                                 \
     5.7 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
     5.8 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
     5.9  \           evs : otway lost |]                                           \
    5.10  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    5.11  by (etac rev_mp 1);
    5.12 @@ -183,9 +183,9 @@
    5.13  
    5.14  (*The equality makes the induction hypothesis easier to apply*)
    5.15  goal thy  
    5.16 - "!!evs. evs : otway lost ==>                                         \
    5.17 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    5.18 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    5.19 + "!!evs. evs : otway lost ==>                                    \
    5.20 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
    5.21 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
    5.22  \            (K : KK | Key K : analz (sees lost Spy evs))";
    5.23  by (etac otway.induct 1);
    5.24  by analz_sees_tac;
    5.25 @@ -200,8 +200,8 @@
    5.26  
    5.27  
    5.28  goal thy
    5.29 - "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
    5.30 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
    5.31 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
    5.32 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
    5.33  \        (K = KAB | Key K : analz (sees lost Spy evs))";
    5.34  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    5.35  qed "analz_insert_freshK";
    5.36 @@ -210,9 +210,9 @@
    5.37  (*** The Key K uniquely identifies the Server's  message. **)
    5.38  
    5.39  goal thy 
    5.40 - "!!evs. evs : otway lost ==>                                                 \
    5.41 -\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    5.42 -\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
    5.43 + "!!evs. evs : otway lost ==>                                             \
    5.44 +\   EX B' NA' NB' X'. ALL B NA NB X.                                      \
    5.45 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
    5.46  \     B=B' & NA=NA' & NB=NB' & X=X'";
    5.47  by (etac otway.induct 1);
    5.48  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    5.49 @@ -229,9 +229,9 @@
    5.50  
    5.51  goal thy 
    5.52   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    5.53 -\            : set evs;                                    \ 
    5.54 +\            : set evs;                                            \ 
    5.55  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    5.56 -\            : set evs;                                    \
    5.57 +\            : set evs;                                            \
    5.58  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    5.59  by (prove_unique_tac lemma 1);
    5.60  qed "unique_session_keys";
    5.61 @@ -257,7 +257,7 @@
    5.62  
    5.63  goal thy 
    5.64   "!!evs. [| evs : otway lost; A ~: lost |]               \
    5.65 -\ ==> EX B'. ALL B.    \
    5.66 +\ ==> EX B'. ALL B.                                      \
    5.67  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
    5.68  \        --> B = B'";
    5.69  by parts_induct_tac;
    5.70 @@ -300,7 +300,7 @@
    5.71  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
    5.72  \        --> Says A B {|NA, Agent A, Agent B,                          \
    5.73  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    5.74 -\             : set evs -->                                    \
    5.75 +\             : set evs -->                                            \
    5.76  \            (EX NB. Says Server B                                     \
    5.77  \                 {|NA,                                                \
    5.78  \                   Crypt (shrK A) {|NA, Key K|},                      \
    5.79 @@ -335,10 +335,10 @@
    5.80    Spy_not_see_encrypted_key*)
    5.81  goal thy 
    5.82   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
    5.83 -\            : set evs;                                    \
    5.84 +\            : set evs;                                            \
    5.85  \           Says A B {|NA, Agent A, Agent B,                       \
    5.86  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
    5.87 -\            : set evs;                                    \
    5.88 +\            : set evs;                                            \
    5.89  \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
    5.90  \        ==> EX NB. Says Server B                                  \
    5.91  \                     {|NA,                                        \
    5.92 @@ -358,8 +358,8 @@
    5.93   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
    5.94  \        ==> Says Server B                                                 \
    5.95  \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
    5.96 -\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->      \
    5.97 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    5.98 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->              \
    5.99 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
   5.100  \            Key K ~: analz (sees lost Spy evs)";
   5.101  by (etac otway.induct 1);
   5.102  by analz_sees_tac;
   5.103 @@ -382,8 +382,8 @@
   5.104  goal thy 
   5.105   "!!evs. [| Says Server B                                                \
   5.106  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   5.107 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   5.108 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   5.109 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
   5.110 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
   5.111  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   5.112  \        ==> Key K ~: analz (sees lost Spy evs)";
   5.113  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.114 @@ -395,8 +395,8 @@
   5.115   "!!evs. [| C ~: {A,B,Server};                                           \
   5.116  \           Says Server B                                                \
   5.117  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   5.118 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   5.119 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   5.120 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
   5.121 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
   5.122  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   5.123  \        ==> Key K ~: analz (sees lost C evs)";
   5.124  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   5.125 @@ -458,7 +458,7 @@
   5.126  \        --> (ALL X'. Says B Server                                      \
   5.127  \                       {|NA, Agent A, Agent B, X',                      \
   5.128  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   5.129 -\             : set evs                                          \
   5.130 +\             : set evs                                                  \
   5.131  \             --> Says Server B                                          \
   5.132  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   5.133  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   5.134 @@ -486,10 +486,10 @@
   5.135  goal thy 
   5.136   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   5.137  \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   5.138 -\            : set evs;                                    \
   5.139 +\            : set evs;                                            \
   5.140  \           Says B Server {|NA, Agent A, Agent B, X',              \
   5.141  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   5.142 -\            : set evs |]                                  \
   5.143 +\            : set evs |]                                          \
   5.144  \        ==> Says Server B                                         \
   5.145  \                 {|NA,                                            \
   5.146  \                   Crypt (shrK A) {|NA, Key K|},                  \
   5.147 @@ -507,7 +507,7 @@
   5.148   "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   5.149  \        ==> Says Server B                                            \
   5.150  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   5.151 -\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
   5.152 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   5.153  \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   5.154  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   5.155  \            : set evs)";
   5.156 @@ -523,13 +523,11 @@
   5.157    We could probably prove that X has the expected form, but that is not
   5.158    strictly necessary for authentication.*)
   5.159  goal thy 
   5.160 - "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   5.161 -\            : set evs;                                    \
   5.162 -\           Says A B {|NA, Agent A, Agent B,                       \
   5.163 -\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   5.164 -\            : set evs;                                    \
   5.165 -\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   5.166 -\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   5.167 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   5.168 +\           Says A B {|NA, Agent A, Agent B,                                \
   5.169 +\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   5.170 +\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |]          \
   5.171 +\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   5.172  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   5.173  \            : set evs";
   5.174  by (blast_tac (!claset addSDs  [A_trusts_OR4]
     6.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 13:20:50 1997 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jun 27 10:47:13 1997 +0200
     6.3 @@ -139,7 +139,7 @@
     6.4   "!!evs. [| Says Server B                                           \
     6.5  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
     6.6  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
     6.7 -\             : set evs;                                    \
     6.8 +\             : set evs;                                            \
     6.9  \           evs : otway lost |]                                     \
    6.10  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    6.11  by (etac rev_mp 1);
    6.12 @@ -171,9 +171,9 @@
    6.13  
    6.14  (*The equality makes the induction hypothesis easier to apply*)
    6.15  goal thy  
    6.16 - "!!evs. evs : otway lost ==>                                         \
    6.17 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    6.18 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    6.19 + "!!evs. evs : otway lost ==>                                    \
    6.20 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
    6.21 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
    6.22  \            (K : KK | Key K : analz (sees lost Spy evs))";
    6.23  by (etac otway.induct 1);
    6.24  by analz_sees_tac;
    6.25 @@ -188,8 +188,8 @@
    6.26  
    6.27  
    6.28  goal thy
    6.29 - "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
    6.30 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
    6.31 + "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
    6.32 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
    6.33  \        (K = KAB | Key K : analz (sees lost Spy evs))";
    6.34  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    6.35  qed "analz_insert_freshK";
    6.36 @@ -200,8 +200,8 @@
    6.37  goal thy 
    6.38   "!!evs. evs : otway lost ==>                              \
    6.39  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    6.40 -\       Says Server B \
    6.41 -\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    6.42 +\       Says Server B                                      \
    6.43 +\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
    6.44  \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    6.45  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    6.46  by (etac otway.induct 1);
    6.47 @@ -222,11 +222,11 @@
    6.48  "!!evs. [| Says Server B                                           \
    6.49  \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
    6.50  \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
    6.51 -\           : set evs;                                     \
    6.52 +\           : set evs;                                             \
    6.53  \          Says Server B'                                          \
    6.54  \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    6.55  \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    6.56 -\           : set evs;                                     \
    6.57 +\           : set evs;                                             \
    6.58  \          evs : otway lost |]                                     \
    6.59  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    6.60  by (prove_unique_tac lemma 1);
    6.61 @@ -257,7 +257,7 @@
    6.62    Freshness may be inferred from nonce NA.*)
    6.63  goal thy 
    6.64   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    6.65 -\            : set evs;                                         \
    6.66 +\            : set evs;                                                 \
    6.67  \           A ~: lost;  evs : otway lost |]                             \
    6.68  \        ==> EX NB. Says Server B                                       \
    6.69  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    6.70 @@ -277,8 +277,8 @@
    6.71  \        ==> Says Server B                                                 \
    6.72  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    6.73  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    6.74 -\            : set evs -->                                         \
    6.75 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
    6.76 +\            : set evs -->                                                 \
    6.77 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
    6.78  \            Key K ~: analz (sees lost Spy evs)";
    6.79  by (etac otway.induct 1);
    6.80  by analz_sees_tac;
    6.81 @@ -302,8 +302,8 @@
    6.82   "!!evs. [| Says Server B                                           \
    6.83  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    6.84  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    6.85 -\             : set evs;                                    \
    6.86 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
    6.87 +\             : set evs;                                            \
    6.88 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    6.89  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
    6.90  \        ==> Key K ~: analz (sees lost Spy evs)";
    6.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    6.92 @@ -316,8 +316,8 @@
    6.93  \           Says Server B                                           \
    6.94  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    6.95  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    6.96 -\             : set evs;                                    \
    6.97 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
    6.98 +\             : set evs;                                            \
    6.99 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   6.100  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   6.101  \        ==> Key K ~: analz (sees lost C evs)";
   6.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   6.103 @@ -351,7 +351,7 @@
   6.104  goal thy 
   6.105   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   6.106  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   6.107 -\            : set evs |]                                           \
   6.108 +\            : set evs |]                                                   \
   6.109  \        ==> EX NA. Says Server B                                           \
   6.110  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   6.111  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
     7.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jun 26 13:20:50 1997 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Jun 27 10:47:13 1997 +0200
     7.3 @@ -56,8 +56,7 @@
     7.4           (*Bob receives the Server's (?) message and compares the Nonces with
     7.5  	   those in the message he previously sent the Server.*)
     7.6      OR4  "[| evs: otway lost;  A ~= B;
     7.7 -             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
     7.8 -               : set evs;
     7.9 +             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
    7.10               Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    7.11                 : set evs |]
    7.12            ==> Says B A X # evs : otway lost"
     8.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jun 27 10:47:13 1997 +0200
     8.3 @@ -140,7 +140,7 @@
     8.4    for Oops case.*)
     8.5  goal thy 
     8.6   "!!evs. [| Says Server B                                                 \
     8.7 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
     8.8 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
     8.9  \           evs : otway |]                                                \
    8.10  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    8.11  by (etac rev_mp 1);
    8.12 @@ -172,9 +172,9 @@
    8.13  
    8.14  (*The equality makes the induction hypothesis easier to apply*)
    8.15  goal thy  
    8.16 - "!!evs. evs : otway ==> \
    8.17 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    8.18 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    8.19 + "!!evs. evs : otway ==>                                         \
    8.20 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
    8.21 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
    8.22  \            (K : KK | Key K : analz (sees lost Spy evs))";
    8.23  by (etac otway.induct 1);
    8.24  by analz_sees_tac;
    8.25 @@ -199,9 +199,9 @@
    8.26  (*** The Key K uniquely identifies the Server's  message. **)
    8.27  
    8.28  goal thy 
    8.29 - "!!evs. evs : otway ==>                                                      \
    8.30 -\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    8.31 -\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
    8.32 + "!!evs. evs : otway ==>                                                  \
    8.33 +\   EX B' NA' NB' X'. ALL B NA NB X.                                      \
    8.34 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
    8.35  \     B=B' & NA=NA' & NB=NB' & X=X'";
    8.36  by (etac otway.induct 1);
    8.37  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    8.38 @@ -217,10 +217,8 @@
    8.39  val lemma = result();
    8.40  
    8.41  goal thy 
    8.42 - "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    8.43 -\            : set evs;                                    \ 
    8.44 -\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    8.45 -\            : set evs;                                    \
    8.46 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
    8.47 +\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
    8.48  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    8.49  by (prove_unique_tac lemma 1);
    8.50  qed "unique_session_keys";
    8.51 @@ -231,8 +229,8 @@
    8.52   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
    8.53  \        ==> Says Server B                                            \
    8.54  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
    8.55 -\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
    8.56 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->      \
    8.57 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
    8.58 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
    8.59  \            Key K ~: analz (sees lost Spy evs)";
    8.60  by (etac otway.induct 1);
    8.61  by analz_sees_tac;
    8.62 @@ -253,10 +251,10 @@
    8.63  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    8.64  
    8.65  goal thy 
    8.66 - "!!evs. [| Says Server B                                                \
    8.67 -\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
    8.68 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
    8.69 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
    8.70 + "!!evs. [| Says Server B                                         \
    8.71 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
    8.72 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
    8.73 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
    8.74  \           A ~: lost;  B ~: lost;  evs : otway |]                \
    8.75  \        ==> Key K ~: analz (sees lost Spy evs)";
    8.76  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    8.77 @@ -275,8 +273,7 @@
    8.78  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
    8.79  \             : parts (sees lost Spy evs) -->                  \
    8.80  \            Says A B {|NA, Agent A, Agent B,                  \
    8.81 -\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    8.82 -\             : set evs";
    8.83 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
    8.84  by parts_induct_tac;
    8.85  by (Fake_parts_insert_tac 1);
    8.86  by (Blast_tac 1);
    8.87 @@ -288,16 +285,15 @@
    8.88  (*Only it is FALSE.  Somebody could make a fake message to Server
    8.89            substituting some other nonce NA' for NB.*)
    8.90  goal thy 
    8.91 - "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                        \
    8.92 + "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                         \
    8.93  \        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
    8.94 -\            Says A B {|NA, Agent A, Agent B,                  \
    8.95 +\            Says A B {|NA, Agent A, Agent B,                      \
    8.96  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    8.97 -\             : set evs -->                            \
    8.98 +\             : set evs -->                                    \
    8.99  \            (EX B NB. Says Server B                           \
   8.100  \                 {|NA,                                        \
   8.101  \                   Crypt (shrK A) {|NA, Key K|},              \
   8.102 -\                   Crypt (shrK B) {|NB, Key K|}|}             \
   8.103 -\                   : set evs)";
   8.104 +\                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
   8.105  by parts_induct_tac;
   8.106  by (Fake_parts_insert_tac 1);
   8.107  (*OR1: it cannot be a new Nonce, contradiction.*)
     9.1 --- a/src/HOL/Auth/Recur.ML	Thu Jun 26 13:20:50 1997 +0200
     9.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jun 27 10:47:13 1997 +0200
     9.3 @@ -21,11 +21,10 @@
     9.4  
     9.5  (*Simplest case: Alice goes directly to the server*)
     9.6  goal thy
     9.7 - "!!A. A ~= Server   \
     9.8 + "!!A. A ~= Server                          \
     9.9  \ ==> EX K NA. EX evs: recur lost.          \
    9.10  \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    9.11 -\                     Agent Server|}      \
    9.12 -\         : set evs";
    9.13 +\                     Agent Server|}  : set evs";
    9.14  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.15  by (rtac (recur.Nil RS recur.RA1 RS 
    9.16            (respond.One RSN (4,recur.RA3))) 2);
    9.17 @@ -38,8 +37,7 @@
    9.18   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    9.19  \ ==> EX K. EX NA. EX evs: recur lost.            \
    9.20  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    9.21 -\                  Agent Server|}                               \
    9.22 -\         : set evs";
    9.23 +\                  Agent Server|}  : set evs";
    9.24  by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
    9.25  by (REPEAT (eresolve_tac [exE, conjE] 1));
    9.26  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.27 @@ -58,8 +56,7 @@
    9.28   "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
    9.29  \ ==> EX K. EX NA. EX evs: recur lost.                          \
    9.30  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    9.31 -\                  Agent Server|}                               \
    9.32 -\         : set evs";
    9.33 +\                  Agent Server|}  : set evs";
    9.34  by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
    9.35  by (REPEAT (eresolve_tac [exE, conjE] 1));
    9.36  by (REPEAT (resolve_tac [exI,bexI] 1));
    9.37 @@ -82,7 +79,7 @@
    9.38  by (rtac subsetI 1);
    9.39  by (etac recur.induct 1);
    9.40  by (REPEAT_FIRST
    9.41 -    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    9.42 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    9.43                                :: recur.intrs))));
    9.44  qed "recur_mono";
    9.45  
    9.46 @@ -528,9 +525,8 @@
    9.47  goalw thy [HPair_def]
    9.48   "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
    9.49  \             : parts (sees lost Spy evs);                        \
    9.50 -\            A ~: lost;  evs : recur lost |]                        \
    9.51 -\        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
    9.52 -\             : set evs";
    9.53 +\            A ~: lost;  evs : recur lost |]                      \
    9.54 +\     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
    9.55  by (etac rev_mp 1);
    9.56  by parts_induct_tac;
    9.57  by (Fake_parts_insert_tac 1);
    9.58 @@ -547,7 +543,7 @@
    9.59  goal thy 
    9.60   "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
    9.61  \           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
    9.62 -\        ==> EX C RC. Says Server C RC : set evs &   \
    9.63 +\        ==> EX C RC. Says Server C RC : set evs  &          \
    9.64  \                     Crypt (shrK A) Y : parts {RC}";
    9.65  by (etac rev_mp 1);
    9.66  by parts_induct_tac;
    10.1 --- a/src/HOL/Auth/Recur.thy	Thu Jun 26 13:20:50 1997 +0200
    10.2 +++ b/src/HOL/Auth/Recur.thy	Fri Jun 27 10:47:13 1997 +0200
    10.3 @@ -90,15 +90,13 @@
    10.4             those in the message he previously sent the Server.*)
    10.5      RA4  "[| evs: recur lost;  A ~= B;  
    10.6               Says B  C {|XH, Agent B, Agent C, Nonce NB, 
    10.7 -                         XA, Agent A, Agent B, Nonce NA, P|} 
    10.8 -               : set evs;
    10.9 +                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
   10.10               Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
   10.11                           Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
   10.12 -                         RA|}
   10.13 -               : set evs |]
   10.14 +                         RA|} : set evs |]
   10.15            ==> Says B A RA # evs : recur lost"
   10.16  
   10.17 -(**No "oops" message can readily be expressed, since each session key is
   10.18 +(**No "oops" message can easily be expressed.  Each session key is
   10.19     associated--in two separate messages--with two nonces.
   10.20  ***)
   10.21  end
    11.1 --- a/src/HOL/Auth/WooLam.ML	Thu Jun 26 13:20:50 1997 +0200
    11.2 +++ b/src/HOL/Auth/WooLam.ML	Fri Jun 27 10:47:13 1997 +0200
    11.3 @@ -21,8 +21,7 @@
    11.4  goal thy 
    11.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    11.6  \        ==> EX NB. EX evs: woolam.               \
    11.7 -\               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
    11.8 -\                 : set evs";
    11.9 +\              Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
   11.10  by (REPEAT (resolve_tac [exI,bexI] 1));
   11.11  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
   11.12            woolam.WL4 RS woolam.WL5) 2);
   11.13 @@ -107,7 +106,7 @@
   11.14    Alice, then she originated that certificate.  But we DO NOT know that B
   11.15    ever saw it: the Spy may have rerouted the message to the Server.*)
   11.16  goal thy 
   11.17 - "!!evs. [| A ~: lost;  evs : woolam;               \
   11.18 + "!!evs. [| A ~: lost;  evs : woolam;                      \
   11.19  \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   11.20  \            : set evs |]                                  \
   11.21  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   11.22 @@ -121,8 +120,8 @@
   11.23  
   11.24  (*Server sent WL5 only if it received the right sort of message*)
   11.25  goal thy 
   11.26 - "!!evs. evs : woolam ==>                                              \
   11.27 -\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs   \
   11.28 + "!!evs. evs : woolam ==>                                                   \
   11.29 +\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs           \
   11.30  \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   11.31  \               : set evs)";
   11.32  by parts_induct_tac;
   11.33 @@ -133,8 +132,8 @@
   11.34  
   11.35  (*If the encrypted message appears then it originated with the Server!*)
   11.36  goal thy 
   11.37 - "!!evs. [| B ~: lost;  evs : woolam |]                   \
   11.38 -\    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
   11.39 + "!!evs. [| B ~: lost;  evs : woolam |]                                  \
   11.40 +\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)  \
   11.41  \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   11.42  by parts_induct_tac;
   11.43  by (Fake_parts_insert_tac 1);
   11.44 @@ -143,7 +142,7 @@
   11.45  (*Partial guarantee for B: if it gets a message of correct form then the Server
   11.46    sent the same message.*)
   11.47  goal thy 
   11.48 - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
   11.49 + "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs;         \
   11.50  \           B ~: lost;  evs : woolam |]                                  \
   11.51  \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   11.52  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   11.53 @@ -156,7 +155,7 @@
   11.54    the Server via the Spy.*)
   11.55  goal thy 
   11.56   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
   11.57 -\           A ~: lost;  B ~: lost;  evs : woolam  |] \
   11.58 +\           A ~: lost;  B ~: lost;  evs : woolam  |]                  \
   11.59  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   11.60  by (blast_tac (!claset addIs  [Server_trusts_WL4]
   11.61                        addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
   11.62 @@ -176,9 +175,9 @@
   11.63  
   11.64  (**CANNOT be proved because A doesn't know where challenges come from...
   11.65  goal thy 
   11.66 - "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
   11.67 + "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                \
   11.68  \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
   11.69 -\        Says B A (Nonce NB) : set evs        \
   11.70 +\        Says B A (Nonce NB) : set evs                            \
   11.71  \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   11.72  by parts_induct_tac;
   11.73  by (Fake_parts_insert_tac 1);
    12.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 13:20:50 1997 +0200
    12.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jun 27 10:47:13 1997 +0200
    12.3 @@ -23,7 +23,7 @@
    12.4  (*A "possibility property": there are traces that reach the end*)
    12.5  goal thy 
    12.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    12.7 -\        ==> EX X NB K. EX evs: yahalom lost.          \
    12.8 +\        ==> EX X NB K. EX evs: yahalom lost.     \
    12.9  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   12.10  by (REPEAT (resolve_tac [exI,bexI] 1));
   12.11  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   12.12 @@ -39,7 +39,7 @@
   12.13  by (rtac subsetI 1);
   12.14  by (etac yahalom.induct 1);
   12.15  by (REPEAT_FIRST
   12.16 -    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
   12.17 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
   12.18                                :: yahalom.intrs))));
   12.19  qed "yahalom_mono";
   12.20  
   12.21 @@ -65,8 +65,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 (shrK A) {|B, K, NA, NB|}, X|} \
   12.26 -\                  : set evs ==> \
   12.27 +goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
   12.28  \                K : parts (sees lost Spy evs)";
   12.29  by (blast_tac (!claset addSEs partsEs
   12.30                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   12.31 @@ -140,7 +139,7 @@
   12.32    Oops as well as main secrecy property.*)
   12.33  goal thy 
   12.34   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   12.35 -\             : set evs;                                           \
   12.36 +\             : set evs;                                                   \
   12.37  \           evs : yahalom lost |]                                          \
   12.38  \        ==> K ~: range shrK";
   12.39  by (etac rev_mp 1);
   12.40 @@ -169,8 +168,8 @@
   12.41  (** Session keys are not used to encrypt other session keys **)
   12.42  
   12.43  goal thy  
   12.44 - "!!evs. evs : yahalom lost ==> \
   12.45 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
   12.46 + "!!evs. evs : yahalom lost ==>                                 \
   12.47 +\  ALL K KK. KK <= Compl (range shrK) -->                       \
   12.48  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   12.49  \            (K : KK | Key K : analz (sees lost Spy evs))";
   12.50  by (etac yahalom.induct 1);
   12.51 @@ -186,7 +185,7 @@
   12.52  
   12.53  goal thy
   12.54   "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   12.55 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   12.56 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
   12.57  \        (K = KAB | Key K : analz (sees lost Spy evs))";
   12.58  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   12.59  qed "analz_insert_freshK";
   12.60 @@ -196,7 +195,7 @@
   12.61  
   12.62  goal thy 
   12.63   "!!evs. evs : yahalom lost ==>                                     \
   12.64 -\      EX A' B' na' nb' X'. ALL A B na nb X.                             \
   12.65 +\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
   12.66  \          Says Server A                                            \
   12.67  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   12.68  \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   12.69 @@ -216,10 +215,10 @@
   12.70  goal thy 
   12.71  "!!evs. [| Says Server A                                            \
   12.72  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   12.73 -\           : set evs;                                      \
   12.74 +\           : set evs;                                              \
   12.75  \          Says Server A'                                           \
   12.76  \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   12.77 -\           : set evs;                                      \
   12.78 +\           : set evs;                                              \
   12.79  \          evs : yahalom lost |]                                    \
   12.80  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   12.81  by (prove_unique_tac lemma 1);
   12.82 @@ -233,8 +232,8 @@
   12.83  \        ==> Says Server A                                        \
   12.84  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   12.85  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   12.86 -\             : set evs -->                               \
   12.87 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->  \
   12.88 +\             : set evs -->                                       \
   12.89 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   12.90  \            Key K ~: analz (sees lost Spy evs)";
   12.91  by (etac yahalom.induct 1);
   12.92  by analz_sees_tac;
   12.93 @@ -259,8 +258,8 @@
   12.94   "!!evs. [| Says Server A                                         \
   12.95  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   12.96  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   12.97 -\             : set evs;                                  \
   12.98 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   12.99 +\             : set evs;                                          \
  12.100 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
  12.101  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  12.102  \        ==> Key K ~: analz (sees lost Spy evs)";
  12.103  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
  12.104 @@ -274,8 +273,8 @@
  12.105  \           Says Server A                                         \
  12.106  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
  12.107  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
  12.108 -\             : set evs;                                  \
  12.109 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
  12.110 +\             : set evs;                                          \
  12.111 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
  12.112  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  12.113  \        ==> Key K ~: analz (sees lost C evs)";
  12.114  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  12.115 @@ -394,7 +393,7 @@
  12.116  goalw thy [KeyWithNonce_def]
  12.117   "!!evs. [| Says Server A                                                \
  12.118  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
  12.119 -\             : set evs;                                         \
  12.120 +\             : set evs;                                                 \
  12.121  \           NB ~= NB';  evs : yahalom lost |]                            \
  12.122  \        ==> ~ KeyWithNonce K NB evs";
  12.123  by (blast_tac (!claset addDs [unique_session_keys]) 1);
  12.124 @@ -453,7 +452,7 @@
  12.125  goal thy 
  12.126   "!!evs. [| Says Server A                                                 \
  12.127  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
  12.128 -\           : set evs;                                            \
  12.129 +\           : set evs;                                                    \
  12.130  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
  12.131  \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
  12.132  \            (Nonce NB : analz (sees lost Spy evs))";
  12.133 @@ -495,9 +494,9 @@
  12.134    not_lost_tac to remove the assumption B' ~: lost.*)
  12.135  goal thy 
  12.136   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
  12.137 -\            : set evs;  B ~: lost;                               \
  12.138 +\            : set evs;          B ~: lost;                               \
  12.139  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
  12.140 -\            : set evs;                                           \
  12.141 +\            : set evs;                                                   \
  12.142  \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
  12.143  \        ==> NA' = NA & A' = A & B' = B";
  12.144  by (not_lost_tac "B'" 1);
  12.145 @@ -527,8 +526,8 @@
  12.146  
  12.147  (*The Server sends YM3 only in response to YM2.*)
  12.148  goal thy 
  12.149 - "!!evs. [| Says Server A                                           \
  12.150 -\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
  12.151 + "!!evs. [| Says Server A                                                \
  12.152 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
  12.153  \           evs : yahalom lost |]                                        \
  12.154  \        ==> EX B'. Says B' Server                                       \
  12.155  \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
  12.156 @@ -546,8 +545,8 @@
  12.157   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
  12.158  \ ==> Says B Server                                                    \
  12.159  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
  12.160 -\     : set evs -->                               \
  12.161 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->  \
  12.162 +\     : set evs -->                                                    \
  12.163 +\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
  12.164  \     Nonce NB ~: analz (sees lost Spy evs)";
  12.165  by (etac yahalom.induct 1);
  12.166  by analz_sees_tac;
  12.167 @@ -606,10 +605,10 @@
  12.168  goal thy 
  12.169   "!!evs. [| Says B Server                                                   \
  12.170  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
  12.171 -\             : set evs;                                            \
  12.172 +\             : set evs;                                                    \
  12.173  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  12.174 -\                       Crypt K (Nonce NB)|} : set evs;             \
  12.175 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
  12.176 +\                       Crypt K (Nonce NB)|} : set evs;                     \
  12.177 +\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
  12.178  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
  12.179  \         ==> Says Server A                                                 \
  12.180  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
  12.181 @@ -636,8 +635,7 @@
  12.182  \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
  12.183  \        : parts (sees lost Spy evs) -->                               \
  12.184  \      B ~: lost -->                                                   \
  12.185 -\      Says B Server {|Agent B,                                \
  12.186 -\                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  12.187 +\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  12.188  \         : set evs";
  12.189  by parts_induct_tac;
  12.190  by (Fake_parts_insert_tac 1);
  12.191 @@ -645,12 +643,11 @@
  12.192  
  12.193  (*If the server sends YM3 then B sent YM2*)
  12.194  goal thy 
  12.195 - "!!evs. evs : yahalom lost                                       \
  12.196 + "!!evs. evs : yahalom lost                                                 \
  12.197  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  12.198 -\         : set evs -->                                          \
  12.199 -\      B ~: lost -->                                                     \
  12.200 -\      Says B Server {|Agent B,                            \
  12.201 -\                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
  12.202 +\         : set evs -->                                                     \
  12.203 +\      B ~: lost -->                                                        \
  12.204 +\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
  12.205  \                 : set evs";
  12.206  by (etac yahalom.induct 1);
  12.207  by (ALLGOALS Asm_simp_tac);
  12.208 @@ -664,7 +661,7 @@
  12.209  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  12.210  goal thy
  12.211   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  12.212 -\             : set evs;                                            \
  12.213 +\             : set evs;                                                    \
  12.214  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
  12.215  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
  12.216  \         : set evs";
  12.217 @@ -720,11 +717,10 @@
  12.218  goal thy 
  12.219   "!!evs. [| Says B Server                                                   \
  12.220  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
  12.221 -\             : set evs;                                            \
  12.222 -\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
  12.223 -\                       Crypt K (Nonce NB)|} : set evs;  \
  12.224 -\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
  12.225 -\               ~: set evs);                             \
  12.226 +\             : set evs;                                                    \
  12.227 +\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  12.228 +\                       Crypt K (Nonce NB)|} : set evs;                     \
  12.229 +\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
  12.230  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
  12.231  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
  12.232  by (dtac B_trusts_YM4 1);
    13.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 13:20:50 1997 +0200
    13.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jun 27 10:47:13 1997 +0200
    13.3 @@ -23,7 +23,7 @@
    13.4  
    13.5  (*A "possibility property": there are traces that reach the end*)
    13.6  goal thy 
    13.7 - "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    13.8 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]        \
    13.9  \        ==> EX X NB K. EX evs: yahalom lost.          \
   13.10  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   13.11  by (REPEAT (resolve_tac [exI,bexI] 1));
   13.12 @@ -66,11 +66,10 @@
   13.13            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
   13.14  
   13.15  (*Relates to both YM4 and Oops*)
   13.16 -goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
   13.17 -\                  : set evs ==> \
   13.18 +goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
   13.19  \                K : parts (sees lost Spy evs)";
   13.20  by (blast_tac (!claset addSEs partsEs
   13.21 -                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   13.22 +                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   13.23  qed "YM4_Key_parts_sees_Spy";
   13.24  
   13.25  (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
   13.26 @@ -140,7 +139,7 @@
   13.27    Oops as well as main secrecy property.*)
   13.28  goal thy 
   13.29   "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
   13.30 -\            : set evs;                                         \
   13.31 +\            : set evs;                                                 \
   13.32  \           evs : yahalom lost |]                                       \
   13.33  \        ==> K ~: range shrK & A ~= B";
   13.34  by (etac rev_mp 1);
   13.35 @@ -170,9 +169,9 @@
   13.36  (** Session keys are not used to encrypt other session keys **)
   13.37  
   13.38  goal thy  
   13.39 - "!!evs. evs : yahalom lost ==> \
   13.40 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
   13.41 -\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   13.42 + "!!evs. evs : yahalom lost ==>                                  \
   13.43 +\  ALL K KK. KK <= Compl (range shrK) -->                        \
   13.44 +\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
   13.45  \            (K : KK | Key K : analz (sees lost Spy evs))";
   13.46  by (etac yahalom.induct 1);
   13.47  by analz_sees_tac;
   13.48 @@ -187,7 +186,7 @@
   13.49  
   13.50  goal thy
   13.51   "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   13.52 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   13.53 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
   13.54  \        (K = KAB | Key K : analz (sees lost Spy evs))";
   13.55  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   13.56  qed "analz_insert_freshK";
   13.57 @@ -216,10 +215,10 @@
   13.58  goal thy 
   13.59  "!!evs. [| Says Server A                                            \
   13.60  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
   13.61 -\           : set evs;                                      \
   13.62 +\           : set evs;                                              \
   13.63  \          Says Server A'                                           \
   13.64  \           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
   13.65 -\           : set evs;                                      \
   13.66 +\           : set evs;                                              \
   13.67  \          evs : yahalom lost |]                                    \
   13.68  \       ==> A=A' & B=B' & na=na' & nb=nb'";
   13.69  by (prove_unique_tac lemma 1);
   13.70 @@ -234,8 +233,8 @@
   13.71  \        ==> Says Server A                                           \
   13.72  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
   13.73  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
   13.74 -\             : set evs -->                                  \
   13.75 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->     \
   13.76 +\             : set evs -->                                          \
   13.77 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->             \
   13.78  \            Key K ~: analz (sees lost Spy evs)";
   13.79  by (etac yahalom.induct 1);
   13.80  by analz_sees_tac;
   13.81 @@ -260,8 +259,8 @@
   13.82   "!!evs. [| Says Server A                                         \
   13.83  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
   13.84  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
   13.85 -\           : set evs;                                    \
   13.86 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   13.87 +\           : set evs;                                            \
   13.88 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   13.89  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   13.90  \        ==> Key K ~: analz (sees lost Spy evs)";
   13.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   13.92 @@ -275,8 +274,8 @@
   13.93  \           Says Server A                                         \
   13.94  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
   13.95  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
   13.96 -\           : set evs;                                    \
   13.97 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   13.98 +\           : set evs;                                            \
   13.99 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
  13.100  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
  13.101  \        ==> Key K ~: analz (sees lost C evs)";
  13.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
  13.103 @@ -333,7 +332,7 @@
  13.104    because we do not have to show that NB is secret. *)
  13.105  goal thy 
  13.106   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
  13.107 -\             : set evs;                                         \
  13.108 +\             : set evs;                                                 \
  13.109  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
  13.110  \        ==> EX NA. Says Server A                                        \
  13.111  \                    {|Nonce NB,                                         \
  13.112 @@ -364,9 +363,9 @@
  13.113  
  13.114  (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
  13.115  goal thy 
  13.116 - "!!evs. evs : yahalom lost                                       \
  13.117 + "!!evs. evs : yahalom lost                                              \
  13.118  \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  13.119 -\         : set evs -->                                          \
  13.120 +\         : set evs -->                                                  \
  13.121  \      B ~: lost -->                                                     \
  13.122  \      (EX nb'. Says B Server {|Agent B, nb',                            \
  13.123  \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
  13.124 @@ -384,7 +383,7 @@
  13.125  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  13.126  goal thy
  13.127   "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  13.128 -\             : set evs;                                            \
  13.129 +\             : set evs;                                                    \
  13.130  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
  13.131  \   ==> EX nb'. Says B Server                                               \
  13.132  \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
  13.133 @@ -440,7 +439,7 @@
  13.134    Other premises guarantee secrecy of K.*)
  13.135  goal thy 
  13.136   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
  13.137 -\                       Crypt K (Nonce NB)|} : set evs;         \
  13.138 +\                       Crypt K (Nonce NB)|} : set evs;                 \
  13.139  \           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
  13.140  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
  13.141  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    14.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 13:20:50 1997 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Jun 27 10:47:13 1997 +0200
    14.3 @@ -57,8 +57,7 @@
    14.4             uses the new session key to send Bob his Nonce.*)
    14.5      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    14.6               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    14.7 -                        X|}
    14.8 -               : set evs;
    14.9 +                        X|}  : set evs;
   14.10               Says A B {|Agent A, Nonce NA|} : set evs |]
   14.11            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
   14.12