src/HOL/Auth/Yahalom.ML
changeset 2284 80ebd1a213fd
parent 2269 820f68aec6ee
child 2322 fbe6dd4abddc
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Nov 29 17:58:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Nov 29 18:03:21 1996 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  goal thy 
     1.5   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.6  \        ==> EX X NB K. EX evs: yahalom lost.          \
     1.7 -\               Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
     1.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
     1.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.10  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    1.11  by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.12 @@ -54,7 +54,7 @@
    1.13  (** For reasoning about the encrypted portion of messages **)
    1.14  
    1.15  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.16 -goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
    1.17 +goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    1.18  \                X : analz (sees lost Spy evs)";
    1.19  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.20  qed "YM4_analz_sees_Spy";
    1.21 @@ -63,7 +63,7 @@
    1.22            YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.23  
    1.24  (*Relates to both YM4 and Oops*)
    1.25 -goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
    1.26 +goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
    1.27  \                  : set_of_list evs ==> \
    1.28  \                K : parts (sees lost Spy evs)";
    1.29  by (fast_tac (!claset addSEs partsEs
    1.30 @@ -145,7 +145,7 @@
    1.31  
    1.32  
    1.33  (*Ready-made for the classical reasoner*)
    1.34 -goal thy "!!evs. [| Says A B {|Crypt {|b, Key (newK evs), na, nb|} K, X|}  \
    1.35 +goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|}  \
    1.36  \                   : set_of_list evs;  evs : yahalom lost |]              \
    1.37  \                ==> R";
    1.38  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.39 @@ -189,7 +189,7 @@
    1.40    Oops as well as main secrecy property.*)
    1.41  goal thy 
    1.42   "!!evs. [| Says Server A                                           \
    1.43 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A), X|} : set_of_list evs; \
    1.44 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
    1.45  \           evs : yahalom lost |]                                   \
    1.46  \        ==> (EX evt: yahalom lost. K = Key(newK evt))";
    1.47  by (etac rev_mp 1);
    1.48 @@ -222,7 +222,7 @@
    1.49    We require that agents should behave like this subsequently also.*)
    1.50  goal thy 
    1.51   "!!evs. evs : yahalom lost ==> \
    1.52 -\        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
    1.53 +\        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
    1.54  \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
    1.55  by (etac yahalom.induct 1);
    1.56  by parts_Fake_tac;
    1.57 @@ -273,7 +273,7 @@
    1.58   "!!evs. evs : yahalom lost ==>                                     \
    1.59  \      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
    1.60  \          Says Server A                                            \
    1.61 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
    1.62 +\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
    1.63  \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
    1.64  by (etac yahalom.induct 1);
    1.65  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.66 @@ -289,10 +289,10 @@
    1.67  
    1.68  goal thy 
    1.69  "!!evs. [| Says Server A                                            \
    1.70 -\           {|Crypt {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
    1.71 +\           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
    1.72  \           : set_of_list evs;                                      \
    1.73  \          Says Server A'                                           \
    1.74 -\           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), X'|}   \
    1.75 +\           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
    1.76  \           : set_of_list evs;                                      \
    1.77  \          evs : yahalom lost |]                                    \
    1.78  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.79 @@ -306,12 +306,12 @@
    1.80  
    1.81  (*If the encrypted message appears then it originated with the Server*)
    1.82  goal thy
    1.83 - "!!evs. [| Crypt {|Agent B, Key K, NA, NB|} (shrK A)                  \
    1.84 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
    1.85  \            : parts (sees lost Spy evs);                              \
    1.86  \           A ~: lost;  evs : yahalom lost |]                          \
    1.87  \         ==> Says Server A                                            \
    1.88 -\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
    1.89 -\                Crypt {|Agent A, Key K|} (shrK B)|}                   \
    1.90 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
    1.91 +\                Crypt (shrK B) {|Agent A, Key K|}|}                   \
    1.92  \             : set_of_list evs";
    1.93  by (etac rev_mp 1);
    1.94  by (parts_induct_tac 1);
    1.95 @@ -323,8 +323,8 @@
    1.96  goal thy 
    1.97   "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    1.98  \        ==> Says Server A                                        \
    1.99 -\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),       \
   1.100 -\                Crypt {|Agent A, Key K|} (shrK B)|}              \
   1.101 +\              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   1.102 +\                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.103  \             : set_of_list evs -->                               \
   1.104  \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   1.105  \            Key K ~: analz (sees lost Spy evs)";
   1.106 @@ -349,8 +349,8 @@
   1.107  (*Final version: Server's message in the most abstract form*)
   1.108  goal thy 
   1.109   "!!evs. [| Says Server A                                               \
   1.110 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   1.111 -\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.112 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   1.113 +\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   1.114  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   1.115  \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.116  \     K ~: analz (sees lost Spy evs)";
   1.117 @@ -362,8 +362,8 @@
   1.118  goal thy 
   1.119   "!!evs. [| C ~: {A,B,Server};                                          \
   1.120  \           Says Server A                                               \
   1.121 -\            {|Crypt {|Agent B, K, NA, NB|} (shrK A),                   \
   1.122 -\              Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs;       \
   1.123 +\            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   1.124 +\              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   1.125  \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   1.126  \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   1.127  \     K ~: analz (sees lost C evs)";
   1.128 @@ -379,12 +379,12 @@
   1.129  (*B knows, by the first part of A's message, that the Server distributed 
   1.130    the key for A and B.  But this part says nothing about nonces.*)
   1.131  goal thy 
   1.132 - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
   1.133 + "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   1.134  \           B ~: lost;  evs : yahalom lost |]                           \
   1.135  \        ==> EX NA NB. Says Server A                                    \
   1.136 -\                        {|Crypt {|Agent B, Key K,                      \
   1.137 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.138 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.139 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   1.140 +\                                  Nonce NA, Nonce NB|},       \
   1.141 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.142  \                       : set_of_list evs";
   1.143  by (etac rev_mp 1);
   1.144  by (parts_induct_tac 1);
   1.145 @@ -429,7 +429,7 @@
   1.146  
   1.147  goal thy 
   1.148   "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
   1.149 -\      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
   1.150 +\      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
   1.151  \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   1.152  by (parts_induct_tac 1);  (*100 seconds??*)
   1.153  by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   1.154 @@ -439,9 +439,9 @@
   1.155  val lemma = result();
   1.156  
   1.157  goal thy 
   1.158 - "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
   1.159 + "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
   1.160  \                  : parts (sees lost Spy evs);         \
   1.161 -\          Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
   1.162 +\          Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
   1.163  \                  : parts (sees lost Spy evs);         \
   1.164  \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   1.165  \        ==> NA' = NA & A' = A & B' = B";
   1.166 @@ -473,9 +473,9 @@
   1.167  
   1.168  (*Variant useful for proving secrecy of NB*)
   1.169  goal thy 
   1.170 - "!!evs.[| Says C D   {|X,  Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
   1.171 + "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
   1.172  \          : set_of_list evs;  B ~: lost;         \
   1.173 -\          Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
   1.174 +\          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   1.175  \          : set_of_list evs;                           \
   1.176  \          NB ~: analz (sees lost Spy evs);             \
   1.177  \          evs : yahalom lost |]  \
   1.178 @@ -489,8 +489,8 @@
   1.179  goal thy 
   1.180   "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   1.181  \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
   1.182 -\      Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
   1.183 -\ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
   1.184 +\      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
   1.185 +\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
   1.186  by (etac yahalom.induct 1);
   1.187  by parts_Fake_tac;
   1.188  by (REPEAT_FIRST 
   1.189 @@ -519,11 +519,11 @@
   1.190  goal thy 
   1.191   "!!evs. evs : yahalom lost                                             \
   1.192  \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   1.193 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   1.194 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   1.195  \            (EX A B NA. Says Server A                                  \
   1.196 -\                        {|Crypt {|Agent B, Key K,                      \
   1.197 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.198 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.199 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   1.200 +\                                  Nonce NA, Nonce NB|},       \
   1.201 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.202  \                       : set_of_list evs)";
   1.203  by (etac yahalom.induct 1);
   1.204  by parts_Fake_tac;
   1.205 @@ -552,11 +552,11 @@
   1.206  goal thy 
   1.207   "!!evs. evs : yahalom lost                                             \
   1.208  \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   1.209 -\            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   1.210 +\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   1.211  \            (EX A B NA. Says Server A                                  \
   1.212 -\                        {|Crypt {|Agent B, Key K,                      \
   1.213 -\                                  Nonce NA, Nonce NB|} (shrK A),       \
   1.214 -\                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   1.215 +\                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   1.216 +\                                  Nonce NA, Nonce NB|},       \
   1.217 +\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.218  \                       : set_of_list evs)";
   1.219  by (etac yahalom.induct 1);
   1.220  by parts_Fake_tac;
   1.221 @@ -580,10 +580,10 @@
   1.222  (*YM3 can only be triggered by YM2*)
   1.223  goal thy 
   1.224   "!!evs. [| Says Server A                                           \
   1.225 -\            {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
   1.226 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
   1.227  \           evs : yahalom lost |]                                        \
   1.228  \        ==> EX B'. Says B' Server                                       \
   1.229 -\                      {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
   1.230 +\                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.231  \                   : set_of_list evs";
   1.232  by (etac rev_mp 1);
   1.233  by (etac yahalom.induct 1);
   1.234 @@ -622,7 +622,7 @@
   1.235  \     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
   1.236  \     (EX K: newK``E. EX A B na X.                                        \
   1.237  \            Says Server A                                                \
   1.238 -\                {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|}   \
   1.239 +\                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
   1.240  \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
   1.241  by (etac yahalom.induct 1);
   1.242  by analz_Fake_tac;
   1.243 @@ -673,7 +673,7 @@
   1.244    for the induction to carry through.*)
   1.245  goal thy 
   1.246   "!!evs. [| Says Server A                                                     \
   1.247 -\            {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
   1.248 +\            {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
   1.249  \           : set_of_list evs;                                                \
   1.250  \           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
   1.251  \           evs : yahalom lost |]                                             \
   1.252 @@ -688,7 +688,7 @@
   1.253  goal thy 
   1.254   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   1.255  \ ==> Says B Server                                                    \
   1.256 -\          {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
   1.257 +\          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.258  \     : set_of_list evs -->                               \
   1.259  \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   1.260  \     Nonce NB ~: analz (sees lost Spy evs)";
   1.261 @@ -757,16 +757,16 @@
   1.262    nonces are forced to agree with NA and NB). *)
   1.263  goal thy 
   1.264   "!!evs. [| Says B Server                                        \
   1.265 -\            {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}  \
   1.266 +\            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
   1.267  \           : set_of_list evs;       \
   1.268 -\           Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   1.269 -\                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   1.270 +\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
   1.271 +\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   1.272  \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   1.273  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   1.274  \         ==> Says Server A                                       \
   1.275 -\                     {|Crypt {|Agent B, Key K,                         \
   1.276 -\                               Nonce NA, Nonce NB|} (shrK A),          \
   1.277 -\                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   1.278 +\                     {|Crypt (shrK A) {|Agent B, Key K,                         \
   1.279 +\                               Nonce NA, Nonce NB|},          \
   1.280 +\                       Crypt (shrK B) {|Agent A, Key K|}|}             \
   1.281  \                   : set_of_list evs";
   1.282  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.283  by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN