src/HOL/Auth/OtwayRees.ML
changeset 3465 e85c24717cad
parent 3451 d10f100676d8
child 3466 30791e5a69c4
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.5  \        ==> EX K. EX NA. EX evs: otway lost.          \
     1.6  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
     1.7 -\                 : set_of_list evs";
     1.8 +\                 : set evs";
     1.9  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.10  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    1.11  by possibility_tac;
    1.12 @@ -45,7 +45,7 @@
    1.13  qed "otway_mono";
    1.14  
    1.15  (*Nobody sends themselves messages*)
    1.16 -goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    1.17 +goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    1.18  by (etac otway.induct 1);
    1.19  by (Auto_tac());
    1.20  qed_spec_mp "not_Says_to_self";
    1.21 @@ -55,17 +55,17 @@
    1.22  
    1.23  (** For reasoning about the encrypted portion of messages **)
    1.24  
    1.25 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    1.26 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, 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 "OR2_analz_sees_Spy";
    1.30  
    1.31 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    1.32 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    1.33  \                ==> X : analz (sees lost Spy evs)";
    1.34  by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    1.35  qed "OR4_analz_sees_Spy";
    1.36  
    1.37 -goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    1.38 +goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    1.39  \                 ==> K : parts (sees lost Spy evs)";
    1.40  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.41  qed "Oops_parts_sees_Spy";
    1.42 @@ -150,7 +150,7 @@
    1.43    for Oops case.*)
    1.44  goal thy 
    1.45   "!!evs. [| Says Server B                                                 \
    1.46 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
    1.47 +\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
    1.48  \           evs : otway lost |]                                           \
    1.49  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.50  by (etac rev_mp 1);
    1.51 @@ -212,7 +212,7 @@
    1.52  goal thy 
    1.53   "!!evs. evs : otway lost ==>                                                 \
    1.54  \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
    1.55 -\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
    1.56 +\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
    1.57  \     B=B' & NA=NA' & NB=NB' & X=X'";
    1.58  by (etac otway.induct 1);
    1.59  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.60 @@ -229,9 +229,9 @@
    1.61  
    1.62  goal thy 
    1.63   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
    1.64 -\            : set_of_list evs;                                    \ 
    1.65 +\            : set evs;                                    \ 
    1.66  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
    1.67 -\            : set_of_list evs;                                    \
    1.68 +\            : set evs;                                    \
    1.69  \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
    1.70  by (prove_unique_tac lemma 1);
    1.71  qed "unique_session_keys";
    1.72 @@ -247,7 +247,7 @@
    1.73  \             : parts (sees lost Spy evs) -->                      \
    1.74  \            Says A B {|NA, Agent A, Agent B,                      \
    1.75  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
    1.76 -\             : set_of_list evs";
    1.77 +\             : set evs";
    1.78  by parts_induct_tac;
    1.79  by (Fake_parts_insert_tac 1);
    1.80  qed_spec_mp "Crypt_imp_OR1";
    1.81 @@ -300,12 +300,12 @@
    1.82  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
    1.83  \        --> Says A B {|NA, Agent A, Agent B,                          \
    1.84  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    1.85 -\             : set_of_list evs -->                                    \
    1.86 +\             : set evs -->                                    \
    1.87  \            (EX NB. Says Server B                                     \
    1.88  \                 {|NA,                                                \
    1.89  \                   Crypt (shrK A) {|NA, Key K|},                      \
    1.90  \                   Crypt (shrK B) {|NB, Key K|}|}                     \
    1.91 -\                   : set_of_list evs)";
    1.92 +\                   : set evs)";
    1.93  by parts_induct_tac;
    1.94  by (Fake_parts_insert_tac 1);
    1.95  (*OR1: it cannot be a new Nonce, contradiction.*)
    1.96 @@ -335,16 +335,16 @@
    1.97    Spy_not_see_encrypted_key*)
    1.98  goal thy 
    1.99   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   1.100 -\            : set_of_list evs;                                    \
   1.101 +\            : set evs;                                    \
   1.102  \           Says A B {|NA, Agent A, Agent B,                       \
   1.103  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   1.104 -\            : set_of_list evs;                                    \
   1.105 +\            : set evs;                                    \
   1.106  \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   1.107  \        ==> EX NB. Says Server B                                  \
   1.108  \                     {|NA,                                        \
   1.109  \                       Crypt (shrK A) {|NA, Key K|},              \
   1.110  \                       Crypt (shrK B) {|NB, Key K|}|}             \
   1.111 -\                       : set_of_list evs";
   1.112 +\                       : set evs";
   1.113  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   1.114                         addEs  sees_Spy_partsEs) 1);
   1.115  qed "A_trusts_OR4";
   1.116 @@ -358,8 +358,8 @@
   1.117   "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   1.118  \        ==> Says Server B                                                 \
   1.119  \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   1.120 -\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   1.121 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   1.122 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->      \
   1.123 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   1.124  \            Key K ~: analz (sees lost Spy evs)";
   1.125  by (etac otway.induct 1);
   1.126  by analz_sees_tac;
   1.127 @@ -382,8 +382,8 @@
   1.128  goal thy 
   1.129   "!!evs. [| Says Server B                                                \
   1.130  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   1.131 -\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   1.132 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   1.133 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   1.134 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   1.135  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.136  \        ==> Key K ~: analz (sees lost Spy evs)";
   1.137  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.138 @@ -395,8 +395,8 @@
   1.139   "!!evs. [| C ~: {A,B,Server};                                           \
   1.140  \           Says Server B                                                \
   1.141  \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   1.142 -\                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   1.143 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   1.144 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
   1.145 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
   1.146  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.147  \        ==> Key K ~: analz (sees lost C evs)";
   1.148  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.149 @@ -417,7 +417,7 @@
   1.150  \            (EX X. Says B Server                              \
   1.151  \             {|NA, Agent A, Agent B, X,                       \
   1.152  \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.153 -\             : set_of_list evs)";
   1.154 +\             : set evs)";
   1.155  by parts_induct_tac;
   1.156  by (Fake_parts_insert_tac 1);
   1.157  by (ALLGOALS Blast_tac);
   1.158 @@ -458,11 +458,11 @@
   1.159  \        --> (ALL X'. Says B Server                                      \
   1.160  \                       {|NA, Agent A, Agent B, X',                      \
   1.161  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   1.162 -\             : set_of_list evs                                          \
   1.163 +\             : set evs                                          \
   1.164  \             --> Says Server B                                          \
   1.165  \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   1.166  \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   1.167 -\                   : set_of_list evs)";
   1.168 +\                   : set evs)";
   1.169  by parts_induct_tac;
   1.170  by (Fake_parts_insert_tac 1);
   1.171  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.172 @@ -486,15 +486,15 @@
   1.173  goal thy 
   1.174   "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   1.175  \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   1.176 -\            : set_of_list evs;                                    \
   1.177 +\            : set evs;                                    \
   1.178  \           Says B Server {|NA, Agent A, Agent B, X',              \
   1.179  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   1.180 -\            : set_of_list evs |]                                  \
   1.181 +\            : set evs |]                                  \
   1.182  \        ==> Says Server B                                         \
   1.183  \                 {|NA,                                            \
   1.184  \                   Crypt (shrK A) {|NA, Key K|},                  \
   1.185  \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   1.186 -\                   : set_of_list evs";
   1.187 +\                   : set evs";
   1.188  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.189                         addSEs sees_Spy_partsEs) 1);
   1.190  qed "B_trusts_OR3";
   1.191 @@ -507,10 +507,10 @@
   1.192   "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   1.193  \        ==> Says Server B                                            \
   1.194  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.195 -\                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   1.196 +\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
   1.197  \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   1.198  \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   1.199 -\            : set_of_list evs)";
   1.200 +\            : set evs)";
   1.201  by (etac otway.induct 1);
   1.202  by (ALLGOALS Asm_simp_tac);
   1.203  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   1.204 @@ -524,14 +524,14 @@
   1.205    strictly necessary for authentication.*)
   1.206  goal thy 
   1.207   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   1.208 -\            : set_of_list evs;                                    \
   1.209 +\            : set evs;                                    \
   1.210  \           Says A B {|NA, Agent A, Agent B,                       \
   1.211  \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   1.212 -\            : set_of_list evs;                                    \
   1.213 +\            : set evs;                                    \
   1.214  \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   1.215  \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   1.216  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.217 -\            : set_of_list evs";
   1.218 +\            : set evs";
   1.219  by (blast_tac (!claset addSDs  [A_trusts_OR4]
   1.220                         addSEs [OR3_imp_OR2]) 1);
   1.221  qed "A_auths_B";