src/HOL/Auth/Yahalom.ML
changeset 3466 30791e5a69c4
parent 3465 e85c24717cad
child 3501 4ab477ffb4c6
     1.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 13:20:50 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jun 27 10:47:13 1997 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  (*A "possibility property": there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
     1.7 -\        ==> EX X NB K. EX evs: yahalom lost.          \
     1.8 +\        ==> EX X NB K. EX evs: yahalom lost.     \
     1.9  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    1.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.11  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    1.12 @@ -39,7 +39,7 @@
    1.13  by (rtac subsetI 1);
    1.14  by (etac yahalom.induct 1);
    1.15  by (REPEAT_FIRST
    1.16 -    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    1.17 +    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    1.18                                :: yahalom.intrs))));
    1.19  qed "yahalom_mono";
    1.20  
    1.21 @@ -65,8 +65,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 (shrK A) {|B, K, NA, NB|}, X|} \
    1.26 -\                  : set evs ==> \
    1.27 +goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
    1.28  \                K : parts (sees lost Spy evs)";
    1.29  by (blast_tac (!claset addSEs partsEs
    1.30                        addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    1.31 @@ -140,7 +139,7 @@
    1.32    Oops as well as main secrecy property.*)
    1.33  goal thy 
    1.34   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
    1.35 -\             : set evs;                                           \
    1.36 +\             : set evs;                                                   \
    1.37  \           evs : yahalom lost |]                                          \
    1.38  \        ==> K ~: range shrK";
    1.39  by (etac rev_mp 1);
    1.40 @@ -169,8 +168,8 @@
    1.41  (** Session keys are not used to encrypt other session keys **)
    1.42  
    1.43  goal thy  
    1.44 - "!!evs. evs : yahalom lost ==> \
    1.45 -\  ALL K KK. KK <= Compl (range shrK) -->                      \
    1.46 + "!!evs. evs : yahalom lost ==>                                 \
    1.47 +\  ALL K KK. KK <= Compl (range shrK) -->                       \
    1.48  \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
    1.49  \            (K : KK | Key K : analz (sees lost Spy evs))";
    1.50  by (etac yahalom.induct 1);
    1.51 @@ -186,7 +185,7 @@
    1.52  
    1.53  goal thy
    1.54   "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
    1.55 -\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
    1.56 +\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
    1.57  \        (K = KAB | Key K : analz (sees lost Spy evs))";
    1.58  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    1.59  qed "analz_insert_freshK";
    1.60 @@ -196,7 +195,7 @@
    1.61  
    1.62  goal thy 
    1.63   "!!evs. evs : yahalom lost ==>                                     \
    1.64 -\      EX A' B' na' nb' X'. ALL A B na nb X.                             \
    1.65 +\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
    1.66  \          Says Server A                                            \
    1.67  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.68  \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
    1.69 @@ -216,10 +215,10 @@
    1.70  goal thy 
    1.71  "!!evs. [| Says Server A                                            \
    1.72  \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
    1.73 -\           : set evs;                                      \
    1.74 +\           : set evs;                                              \
    1.75  \          Says Server A'                                           \
    1.76  \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
    1.77 -\           : set evs;                                      \
    1.78 +\           : set evs;                                              \
    1.79  \          evs : yahalom lost |]                                    \
    1.80  \       ==> A=A' & B=B' & na=na' & nb=nb'";
    1.81  by (prove_unique_tac lemma 1);
    1.82 @@ -233,8 +232,8 @@
    1.83  \        ==> Says Server A                                        \
    1.84  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.85  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.86 -\             : set evs -->                               \
    1.87 -\            Says A Spy {|na, nb, Key K|} ~: set evs -->  \
    1.88 +\             : set evs -->                                       \
    1.89 +\            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
    1.90  \            Key K ~: analz (sees lost Spy evs)";
    1.91  by (etac yahalom.induct 1);
    1.92  by analz_sees_tac;
    1.93 @@ -259,8 +258,8 @@
    1.94   "!!evs. [| Says Server A                                         \
    1.95  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    1.96  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
    1.97 -\             : set evs;                                  \
    1.98 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
    1.99 +\             : set evs;                                          \
   1.100 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   1.101  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.102  \        ==> Key K ~: analz (sees lost Spy evs)";
   1.103  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.104 @@ -274,8 +273,8 @@
   1.105  \           Says Server A                                         \
   1.106  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   1.107  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   1.108 -\             : set evs;                                  \
   1.109 -\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
   1.110 +\             : set evs;                                          \
   1.111 +\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   1.112  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   1.113  \        ==> Key K ~: analz (sees lost C evs)";
   1.114  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.115 @@ -394,7 +393,7 @@
   1.116  goalw thy [KeyWithNonce_def]
   1.117   "!!evs. [| Says Server A                                                \
   1.118  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   1.119 -\             : set evs;                                         \
   1.120 +\             : set evs;                                                 \
   1.121  \           NB ~= NB';  evs : yahalom lost |]                            \
   1.122  \        ==> ~ KeyWithNonce K NB evs";
   1.123  by (blast_tac (!claset addDs [unique_session_keys]) 1);
   1.124 @@ -453,7 +452,7 @@
   1.125  goal thy 
   1.126   "!!evs. [| Says Server A                                                 \
   1.127  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   1.128 -\           : set evs;                                            \
   1.129 +\           : set evs;                                                    \
   1.130  \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
   1.131  \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
   1.132  \            (Nonce NB : analz (sees lost Spy evs))";
   1.133 @@ -495,9 +494,9 @@
   1.134    not_lost_tac to remove the assumption B' ~: lost.*)
   1.135  goal thy 
   1.136   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
   1.137 -\            : set evs;  B ~: lost;                               \
   1.138 +\            : set evs;          B ~: lost;                               \
   1.139  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   1.140 -\            : set evs;                                           \
   1.141 +\            : set evs;                                                   \
   1.142  \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
   1.143  \        ==> NA' = NA & A' = A & B' = B";
   1.144  by (not_lost_tac "B'" 1);
   1.145 @@ -527,8 +526,8 @@
   1.146  
   1.147  (*The Server sends YM3 only in response to YM2.*)
   1.148  goal thy 
   1.149 - "!!evs. [| Says Server A                                           \
   1.150 -\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
   1.151 + "!!evs. [| Says Server A                                                \
   1.152 +\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   1.153  \           evs : yahalom lost |]                                        \
   1.154  \        ==> EX B'. Says B' Server                                       \
   1.155  \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   1.156 @@ -546,8 +545,8 @@
   1.157   "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   1.158  \ ==> Says B Server                                                    \
   1.159  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   1.160 -\     : set evs -->                               \
   1.161 -\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->  \
   1.162 +\     : set evs -->                                                    \
   1.163 +\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   1.164  \     Nonce NB ~: analz (sees lost Spy evs)";
   1.165  by (etac yahalom.induct 1);
   1.166  by analz_sees_tac;
   1.167 @@ -606,10 +605,10 @@
   1.168  goal thy 
   1.169   "!!evs. [| Says B Server                                                   \
   1.170  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.171 -\             : set evs;                                            \
   1.172 +\             : set evs;                                                    \
   1.173  \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.174 -\                       Crypt K (Nonce NB)|} : set evs;             \
   1.175 -\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
   1.176 +\                       Crypt K (Nonce NB)|} : set evs;                     \
   1.177 +\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   1.178  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.179  \         ==> Says Server A                                                 \
   1.180  \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   1.181 @@ -636,8 +635,7 @@
   1.182  \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
   1.183  \        : parts (sees lost Spy evs) -->                               \
   1.184  \      B ~: lost -->                                                   \
   1.185 -\      Says B Server {|Agent B,                                \
   1.186 -\                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.187 +\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.188  \         : set evs";
   1.189  by parts_induct_tac;
   1.190  by (Fake_parts_insert_tac 1);
   1.191 @@ -645,12 +643,11 @@
   1.192  
   1.193  (*If the server sends YM3 then B sent YM2*)
   1.194  goal thy 
   1.195 - "!!evs. evs : yahalom lost                                       \
   1.196 + "!!evs. evs : yahalom lost                                                 \
   1.197  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.198 -\         : set evs -->                                          \
   1.199 -\      B ~: lost -->                                                     \
   1.200 -\      Says B Server {|Agent B,                            \
   1.201 -\                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
   1.202 +\         : set evs -->                                                     \
   1.203 +\      B ~: lost -->                                                        \
   1.204 +\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   1.205  \                 : set evs";
   1.206  by (etac yahalom.induct 1);
   1.207  by (ALLGOALS Asm_simp_tac);
   1.208 @@ -664,7 +661,7 @@
   1.209  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   1.210  goal thy
   1.211   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   1.212 -\             : set evs;                                            \
   1.213 +\             : set evs;                                                    \
   1.214  \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   1.215  \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   1.216  \         : set evs";
   1.217 @@ -720,11 +717,10 @@
   1.218  goal thy 
   1.219   "!!evs. [| Says B Server                                                   \
   1.220  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   1.221 -\             : set evs;                                            \
   1.222 -\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
   1.223 -\                       Crypt K (Nonce NB)|} : set evs;  \
   1.224 -\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
   1.225 -\               ~: set evs);                             \
   1.226 +\             : set evs;                                                    \
   1.227 +\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   1.228 +\                       Crypt K (Nonce NB)|} : set evs;                     \
   1.229 +\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   1.230  \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   1.231  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   1.232  by (dtac B_trusts_YM4 1);