src/HOL/Auth/Yahalom2.ML
changeset 3465 e85c24717cad
parent 3450 cd73bc206d87
child 3466 30791e5a69c4
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -25,7 +25,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 @@ -46,7 +46,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 @@ -57,7 +57,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 {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    1.26 +goal thy "!!evs. Says S A {|NB, 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 @@ -67,7 +67,7 @@
    1.31  
    1.32  (*Relates to both YM4 and Oops*)
    1.33  goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, 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 {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
    1.43 -\            : set_of_list evs;                                         \
    1.44 +\            : set evs;                                         \
    1.45  \           evs : yahalom lost |]                                       \
    1.46  \        ==> K ~: range shrK & A ~= B";
    1.47  by (etac rev_mp 1);
    1.48 @@ -200,7 +200,7 @@
    1.49  \      EX A' B' na' nb' X'. ALL A B na nb X.                        \
    1.50  \          Says Server A                                            \
    1.51  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, 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  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
    1.61 -\           : set_of_list evs;                                      \
    1.62 +\           : set evs;                                      \
    1.63  \          Says Server A'                                           \
    1.64  \           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, 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 @@ -234,8 +234,8 @@
    1.71  \        ==> Says Server A                                           \
    1.72  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
    1.73  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
    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 @@ -260,8 +260,8 @@
    1.82   "!!evs. [| Says Server A                                         \
    1.83  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
    1.84  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
    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 @@ -275,8 +275,8 @@
    1.93  \           Says Server A                                         \
    1.94  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
    1.95  \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
    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 @@ -297,7 +297,7 @@
   1.104  \         ==> EX nb. Says Server A                                     \
   1.105  \                      {|nb, Crypt (shrK A) {|Agent B, Key K, na|},    \
   1.106  \                            Crypt (shrK B) {|nb, Key K, Agent A|}|}   \
   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 @@ -317,7 +317,7 @@
   1.113  \                    {|Nonce NB,                                     \
   1.114  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},  \
   1.115  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \
   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 @@ -333,13 +333,13 @@
   1.122    because we do not have to show that NB is secret. *)
   1.123  goal thy 
   1.124   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
   1.125 -\             : set_of_list evs;                                         \
   1.126 +\             : set evs;                                         \
   1.127  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
   1.128  \        ==> EX NA. Says Server A                                        \
   1.129  \                    {|Nonce NB,                                         \
   1.130  \                      Crypt (shrK A) {|Agent B, Key K, Nonce NA|},      \
   1.131  \                      Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|}     \
   1.132 -\                   : set_of_list evs";
   1.133 +\                   : set evs";
   1.134  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   1.135  by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1);
   1.136  qed "B_trusts_YM4";
   1.137 @@ -355,7 +355,7 @@
   1.138  \      B ~: lost -->                                                   \
   1.139  \      (EX NB. Says B Server {|Agent B, Nonce NB,                      \
   1.140  \                              Crypt (shrK B) {|Agent A, Nonce NA|}|}  \
   1.141 -\         : set_of_list evs)";
   1.142 +\         : set evs)";
   1.143  by parts_induct_tac;
   1.144  by (Fake_parts_insert_tac 1);
   1.145  (*YM2*)
   1.146 @@ -366,11 +366,11 @@
   1.147  goal thy 
   1.148   "!!evs. evs : yahalom lost                                       \
   1.149  \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   1.150 -\         : set_of_list evs -->                                          \
   1.151 +\         : set evs -->                                          \
   1.152  \      B ~: lost -->                                                     \
   1.153  \      (EX nb'. Says B Server {|Agent B, nb',                            \
   1.154  \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
   1.155 -\                 : set_of_list evs)";
   1.156 +\                 : set evs)";
   1.157  by (etac yahalom.induct 1);
   1.158  by (ALLGOALS Asm_simp_tac);
   1.159  (*YM3*)
   1.160 @@ -384,11 +384,11 @@
   1.161  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.162  goal thy
   1.163   "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
   1.164 -\             : set_of_list evs;                                            \
   1.165 +\             : set evs;                                            \
   1.166  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   1.167  \   ==> EX nb'. Says B Server                                               \
   1.168  \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
   1.169 -\                 : set_of_list evs";
   1.170 +\                 : set evs";
   1.171  by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   1.172  		       addEs sees_Spy_partsEs) 1);
   1.173  qed "YM3_auth_B_to_A";
   1.174 @@ -419,7 +419,7 @@
   1.175  \            Crypt (shrK B) {|Nonce NB, Key K, Agent A|}                \
   1.176  \              : parts (sees lost Spy evs) -->                          \
   1.177  \            B ~: lost -->                                              \
   1.178 -\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
   1.179 +\             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   1.180  by analz_mono_parts_induct_tac;
   1.181  (*Fake*)
   1.182  by (Fake_parts_insert_tac 1);
   1.183 @@ -440,11 +440,10 @@
   1.184    Other premises guarantee secrecy of K.*)
   1.185  goal thy 
   1.186   "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
   1.187 -\                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   1.188 -\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|}           \
   1.189 -\               ~: set_of_list evs);                                    \
   1.190 +\                       Crypt K (Nonce NB)|} : set evs;         \
   1.191 +\           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
   1.192  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
   1.193 -\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   1.194 +\        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.195  by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   1.196  by (dtac B_trusts_YM4_shrK 1);
   1.197  by (safe_tac (!claset));