src/HOL/Auth/OtwayRees_AN.ML
changeset 3465 e85c24717cad
parent 3451 d10f100676d8
child 3466 30791e5a69c4
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -23,7 +23,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 (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 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 @@ -42,7 +42,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 @@ -52,13 +52,13 @@
    1.22  
    1.23  (** For reasoning about the encrypted portion of messages **)
    1.24  
    1.25 -goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set_of_list evs ==> \
    1.26 +goal thy "!!evs. Says S' B {|X, Crypt(shrK 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 "OR4_analz_sees_Spy";
    1.30  
    1.31  goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    1.32 -\                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    1.33 +\                  : set evs ==> K : parts (sees lost Spy evs)";
    1.34  by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    1.35  qed "Oops_parts_sees_Spy";
    1.36  
    1.37 @@ -139,7 +139,7 @@
    1.38   "!!evs. [| Says Server B                                           \
    1.39  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    1.40  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    1.41 -\             : set_of_list evs;                                    \
    1.42 +\             : set evs;                                    \
    1.43  \           evs : otway lost |]                                     \
    1.44  \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.45  by (etac rev_mp 1);
    1.46 @@ -202,7 +202,7 @@
    1.47  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
    1.48  \       Says Server B \
    1.49  \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
    1.50 -\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set_of_list evs  \
    1.51 +\           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
    1.52  \       --> A=A' & B=B' & NA=NA' & NB=NB'";
    1.53  by (etac otway.induct 1);
    1.54  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.55 @@ -222,11 +222,11 @@
    1.56  "!!evs. [| Says Server B                                           \
    1.57  \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
    1.58  \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
    1.59 -\           : set_of_list evs;                                     \
    1.60 +\           : set evs;                                     \
    1.61  \          Says Server B'                                          \
    1.62  \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
    1.63  \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
    1.64 -\           : set_of_list evs;                                     \
    1.65 +\           : set evs;                                     \
    1.66  \          evs : otway lost |]                                     \
    1.67  \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
    1.68  by (prove_unique_tac lemma 1);
    1.69 @@ -244,7 +244,7 @@
    1.70  \     --> (EX NB. Says Server B                                          \
    1.71  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    1.72  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    1.73 -\                  : set_of_list evs)";
    1.74 +\                  : set evs)";
    1.75  by parts_induct_tac;
    1.76  by (Fake_parts_insert_tac 1);
    1.77  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    1.78 @@ -257,12 +257,12 @@
    1.79    Freshness may be inferred from nonce NA.*)
    1.80  goal thy 
    1.81   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    1.82 -\            : set_of_list evs;                                         \
    1.83 +\            : set evs;                                         \
    1.84  \           A ~: lost;  evs : otway lost |]                             \
    1.85  \        ==> EX NB. Says Server B                                       \
    1.86  \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
    1.87  \                      Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    1.88 -\                   : set_of_list evs";
    1.89 +\                   : set evs";
    1.90  by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
    1.91                        addEs  sees_Spy_partsEs) 1);
    1.92  qed "A_trusts_OR4";
    1.93 @@ -277,8 +277,8 @@
    1.94  \        ==> Says Server B                                                 \
    1.95  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
    1.96  \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
    1.97 -\            : set_of_list evs -->                                         \
    1.98 -\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
    1.99 +\            : set evs -->                                         \
   1.100 +\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   1.101  \            Key K ~: analz (sees lost Spy evs)";
   1.102  by (etac otway.induct 1);
   1.103  by analz_sees_tac;
   1.104 @@ -302,8 +302,8 @@
   1.105   "!!evs. [| Says Server B                                           \
   1.106  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.107  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.108 -\             : set_of_list evs;                                    \
   1.109 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   1.110 +\             : set evs;                                    \
   1.111 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
   1.112  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.113  \        ==> Key K ~: analz (sees lost Spy evs)";
   1.114  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.115 @@ -316,8 +316,8 @@
   1.116  \           Says Server B                                           \
   1.117  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   1.118  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   1.119 -\             : set_of_list evs;                                    \
   1.120 -\           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;        \
   1.121 +\             : set evs;                                    \
   1.122 +\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
   1.123  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
   1.124  \        ==> Key K ~: analz (sees lost C evs)";
   1.125  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.126 @@ -337,7 +337,7 @@
   1.127  \        --> (EX NA. Says Server B                                          \
   1.128  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.129  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.130 -\                     : set_of_list evs)";
   1.131 +\                     : set evs)";
   1.132  by parts_induct_tac;
   1.133  by (Fake_parts_insert_tac 1);
   1.134  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.135 @@ -351,11 +351,11 @@
   1.136  goal thy 
   1.137   "!!evs. [| B ~: lost;  evs : otway lost;                                   \
   1.138  \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   1.139 -\            : set_of_list evs |]                                           \
   1.140 +\            : set evs |]                                           \
   1.141  \        ==> EX NA. Says Server B                                           \
   1.142  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   1.143  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   1.144 -\                     : set_of_list evs";
   1.145 +\                     : set evs";
   1.146  by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   1.147                         addEs  sees_Spy_partsEs) 1);
   1.148  qed "B_trusts_OR3";