src/HOL/Auth/Yahalom.ML
changeset 3465 e85c24717cad
parent 3464 315694e22856
child 3466 30791e5a69c4
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -24,7 +24,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 K (Nonce NB)|} : set_of_list evs";
     1.8 +\               Says A B {|X, Crypt K (Nonce NB)|} : set 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 
    1.11            yahalom.YM4) 2);
    1.12 @@ -45,7 +45,7 @@
    1.13  
    1.14  
    1.15  (*Nobody sends themselves messages*)
    1.16 -goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.17 +goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    1.18  by (etac yahalom.induct 1);
    1.19  by (Auto_tac());
    1.20  qed_spec_mp "not_Says_to_self";
    1.21 @@ -56,7 +56,7 @@
    1.22  (** For reasoning about the encrypted portion of messages **)
    1.23  
    1.24  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    1.25 -goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    1.26 +goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
    1.27  \                X : analz (sees lost Spy evs)";
    1.28  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.29  qed "YM4_analz_sees_Spy";
    1.30 @@ -66,7 +66,7 @@
    1.31  
    1.32  (*Relates to both YM4 and Oops*)
    1.33  goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
    1.34 -\                  : set_of_list evs ==> \
    1.35 +\                  : set evs ==> \
    1.36  \                K : parts (sees lost Spy evs)";
    1.37  by (blast_tac (!claset addSEs partsEs
    1.38                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    1.39 @@ -140,7 +140,7 @@
    1.40    Oops as well as main secrecy property.*)
    1.41  goal thy 
    1.42   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
    1.43 -\             : set_of_list evs;                                           \
    1.44 +\             : set evs;                                           \
    1.45  \           evs : yahalom lost |]                                          \
    1.46  \        ==> K ~: range shrK";
    1.47  by (etac rev_mp 1);
    1.48 @@ -199,7 +199,7 @@
    1.49  \      EX A' B' na' nb' X'. ALL A B na nb X.                             \
    1.50  \          Says Server A                                            \
    1.51  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.52 -\          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    1.53 +\          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    1.54  by (etac yahalom.induct 1);
    1.55  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.56  by (Step_tac 1);
    1.57 @@ -216,10 +216,10 @@
    1.58  goal thy 
    1.59  "!!evs. [| Says Server A                                            \
    1.60  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.61 -\           : set_of_list evs;                                      \
    1.62 +\           : set evs;                                      \
    1.63  \          Says Server A'                                           \
    1.64  \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
    1.65 -\           : set_of_list evs;                                      \
    1.66 +\           : set evs;                                      \
    1.67  \          evs : yahalom lost |]                                    \
    1.68  \       ==> A=A' & B=B' & na=na' & nb=nb'";
    1.69  by (prove_unique_tac lemma 1);
    1.70 @@ -233,8 +233,8 @@
    1.71  \        ==> Says Server A                                        \
    1.72  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.73  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.74 -\             : set_of_list evs -->                               \
    1.75 -\            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->  \
    1.76 +\             : set evs -->                               \
    1.77 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->  \
    1.78  \            Key K ~: analz (sees lost Spy evs)";
    1.79  by (etac yahalom.induct 1);
    1.80  by analz_sees_tac;
    1.81 @@ -259,8 +259,8 @@
    1.82   "!!evs. [| Says Server A                                         \
    1.83  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.84  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.85 -\             : set_of_list evs;                                  \
    1.86 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
    1.87 +\             : set evs;                                  \
    1.88 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
    1.89  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    1.90  \        ==> Key K ~: analz (sees lost Spy evs)";
    1.91  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
    1.92 @@ -274,8 +274,8 @@
    1.93  \           Says Server A                                         \
    1.94  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.95  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.96 -\             : set_of_list evs;                                  \
    1.97 -\           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
    1.98 +\             : set evs;                                  \
    1.99 +\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   1.100  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.101  \        ==> Key K ~: analz (sees lost C evs)";
   1.102  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.103 @@ -309,7 +309,7 @@
   1.104  \         ==> Says Server A                                            \
   1.105  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   1.106  \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   1.107 -\             : set_of_list evs";
   1.108 +\             : set evs";
   1.109  by (etac rev_mp 1);
   1.110  by parts_induct_tac;
   1.111  by (Fake_parts_insert_tac 1);
   1.112 @@ -327,7 +327,7 @@
   1.113  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.114  \                                           Nonce NA, Nonce NB|},       \
   1.115  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.116 -\                       : set_of_list evs";
   1.117 +\                       : set evs";
   1.118  by (etac rev_mp 1);
   1.119  by parts_induct_tac;
   1.120  by (Fake_parts_insert_tac 1);
   1.121 @@ -346,7 +346,7 @@
   1.122  \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   1.123  \                                  Nonce NA, Nonce NB|},                \
   1.124  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   1.125 -\                       : set_of_list evs)";
   1.126 +\                       : set evs)";
   1.127  by analz_mono_parts_induct_tac;
   1.128  (*YM3 & Fake*)
   1.129  by (Blast_tac 2);
   1.130 @@ -368,7 +368,7 @@
   1.131  goalw thy [KeyWithNonce_def]
   1.132   "!!evs. Says Server A                                              \
   1.133  \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   1.134 -\          : set_of_list evs ==> KeyWithNonce K NB evs";
   1.135 +\          : set evs ==> KeyWithNonce K NB evs";
   1.136  by (Blast_tac 1);
   1.137  qed "KeyWithNonceI";
   1.138  
   1.139 @@ -394,7 +394,7 @@
   1.140  goalw thy [KeyWithNonce_def]
   1.141   "!!evs. [| Says Server A                                                \
   1.142  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   1.143 -\             : set_of_list evs;                                         \
   1.144 +\             : set evs;                                         \
   1.145  \           NB ~= NB';  evs : yahalom lost |]                            \
   1.146  \        ==> ~ KeyWithNonce K NB evs";
   1.147  by (blast_tac (!claset addDs [unique_session_keys]) 1);
   1.148 @@ -453,7 +453,7 @@
   1.149  goal thy 
   1.150   "!!evs. [| Says Server A                                                 \
   1.151  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   1.152 -\           : set_of_list evs;                                            \
   1.153 +\           : set evs;                                            \
   1.154  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
   1.155  \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
   1.156  \            (Nonce NB : analz (sees lost Spy evs))";
   1.157 @@ -495,9 +495,9 @@
   1.158    not_lost_tac to remove the assumption B' ~: lost.*)
   1.159  goal thy 
   1.160   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
   1.161 -\            : set_of_list evs;  B ~: lost;                               \
   1.162 +\            : set evs;  B ~: lost;                               \
   1.163  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   1.164 -\            : set_of_list evs;                                           \
   1.165 +\            : set evs;                                           \
   1.166  \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
   1.167  \        ==> NA' = NA & A' = A & B' = B";
   1.168  by (not_lost_tac "B'" 1);
   1.169 @@ -528,11 +528,11 @@
   1.170  (*The Server sends YM3 only in response to YM2.*)
   1.171  goal thy 
   1.172   "!!evs. [| Says Server A                                           \
   1.173 -\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
   1.174 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
   1.175  \           evs : yahalom lost |]                                        \
   1.176  \        ==> EX B'. Says B' Server                                       \
   1.177  \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.178 -\                   : set_of_list evs";
   1.179 +\                   : set evs";
   1.180  by (etac rev_mp 1);
   1.181  by (etac yahalom.induct 1);
   1.182  by (ALLGOALS Asm_simp_tac);
   1.183 @@ -546,8 +546,8 @@
   1.184   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   1.185  \ ==> Says B Server                                                    \
   1.186  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.187 -\     : set_of_list evs -->                               \
   1.188 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   1.189 +\     : set evs -->                               \
   1.190 +\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->  \
   1.191  \     Nonce NB ~: analz (sees lost Spy evs)";
   1.192  by (etac yahalom.induct 1);
   1.193  by analz_sees_tac;
   1.194 @@ -606,16 +606,16 @@
   1.195  goal thy 
   1.196   "!!evs. [| Says B Server                                                   \
   1.197  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.198 -\             : set_of_list evs;                                            \
   1.199 +\             : set evs;                                            \
   1.200  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.201 -\                       Crypt K (Nonce NB)|} : set_of_list evs;             \
   1.202 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   1.203 +\                       Crypt K (Nonce NB)|} : set evs;             \
   1.204 +\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
   1.205  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.206  \         ==> Says Server A                                                 \
   1.207  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   1.208  \                               Nonce NA, Nonce NB|},                       \
   1.209  \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   1.210 -\               : set_of_list evs";
   1.211 +\               : set evs";
   1.212  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.213  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
   1.214      dtac B_trusts_YM4_shrK 1);
   1.215 @@ -638,7 +638,7 @@
   1.216  \      B ~: lost -->                                                   \
   1.217  \      Says B Server {|Agent B,                                \
   1.218  \                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.219 -\         : set_of_list evs";
   1.220 +\         : set evs";
   1.221  by parts_induct_tac;
   1.222  by (Fake_parts_insert_tac 1);
   1.223  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   1.224 @@ -647,11 +647,11 @@
   1.225  goal thy 
   1.226   "!!evs. evs : yahalom lost                                       \
   1.227  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.228 -\         : set_of_list evs -->                                          \
   1.229 +\         : set evs -->                                          \
   1.230  \      B ~: lost -->                                                     \
   1.231  \      Says B Server {|Agent B,                            \
   1.232  \                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
   1.233 -\                 : set_of_list evs";
   1.234 +\                 : set evs";
   1.235  by (etac yahalom.induct 1);
   1.236  by (ALLGOALS Asm_simp_tac);
   1.237  (*YM4*)
   1.238 @@ -664,10 +664,10 @@
   1.239  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.240  goal thy
   1.241   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.242 -\             : set_of_list evs;                                            \
   1.243 +\             : set evs;                                            \
   1.244  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   1.245  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.246 -\         : set_of_list evs";
   1.247 +\         : set evs";
   1.248  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   1.249  		       addEs sees_Spy_partsEs) 1);
   1.250  qed "YM3_auth_B_to_A";
   1.251 @@ -698,7 +698,7 @@
   1.252  \            Crypt (shrK B) {|Agent A, Key K|}                          \
   1.253  \              : parts (sees lost Spy evs) -->                          \
   1.254  \            B ~: lost -->                                              \
   1.255 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
   1.256 +\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.257  by analz_mono_parts_induct_tac;
   1.258  (*Fake*)
   1.259  by (Fake_parts_insert_tac 1);
   1.260 @@ -720,13 +720,13 @@
   1.261  goal thy 
   1.262   "!!evs. [| Says B Server                                                   \
   1.263  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.264 -\             : set_of_list evs;                                            \
   1.265 +\             : set evs;                                            \
   1.266  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
   1.267 -\                       Crypt K (Nonce NB)|} : set_of_list evs;  \
   1.268 +\                       Crypt K (Nonce NB)|} : set evs;  \
   1.269  \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
   1.270 -\               ~: set_of_list evs);                             \
   1.271 +\               ~: set evs);                             \
   1.272  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.273 -\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   1.274 +\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.275  by (dtac B_trusts_YM4 1);
   1.276  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   1.277  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);