src/HOL/Auth/OtwayRees_AN.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
equal deleted inserted replaced
4536:74f7c556fd90 4537:4e835bd9fada
    56 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    56 goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    57 \                  : set evs ==> K : parts (spies evs)";
    57 \                  : set evs ==> K : parts (spies evs)";
    58 by (Blast_tac 1);
    58 by (Blast_tac 1);
    59 qed "Oops_parts_spies";
    59 qed "Oops_parts_spies";
    60 
    60 
    61 (*OR4_analz_spies lets us treat those cases using the same 
       
    62   argument as for the Fake case.  This is possible for most, but not all,
       
    63   proofs, since Fake messages originate from the Spy. *)
       
    64 
       
    65 bind_thm ("OR4_parts_spies",
    61 bind_thm ("OR4_parts_spies",
    66           OR4_analz_spies RS (impOfSubs analz_subset_parts));
    62           OR4_analz_spies RS (impOfSubs analz_subset_parts));
    67 
    63 
    68 (*For proving the easier theorems about X ~: parts (spies evs).*)
    64 (*For proving the easier theorems about X ~: parts (spies evs).*)
    69 fun parts_induct_tac i = 
    65 fun parts_induct_tac i = 
    74 
    70 
    75 
    71 
    76 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    72 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    77     sends messages containing X! **)
    73     sends messages containing X! **)
    78 
    74 
    79 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    75 (*Spy never sees a good agent's shared key!*)
    80 goal thy 
    76 goal thy 
    81  "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    77  "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    82 by (parts_induct_tac 1);
    78 by (parts_induct_tac 1);
    83 by (ALLGOALS Blast_tac);
    79 by (ALLGOALS Blast_tac);
    84 qed "Spy_see_shrK";
    80 qed "Spy_see_shrK";
   246 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   242 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   247     Does not in itself guarantee security: an attack could violate 
   243     Does not in itself guarantee security: an attack could violate 
   248     the premises, e.g. by having A=Spy **)
   244     the premises, e.g. by having A=Spy **)
   249 
   245 
   250 goal thy 
   246 goal thy 
   251  "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                 \
   247  "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                   \
   252 \        ==> Says Server B                                         \
   248 \        ==> Says Server B                                         \
   253 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   249 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   254 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   250 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   255 \            : set evs -->                                         \
   251 \            : set evs -->                                         \
   256 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
   252 \            Notes Spy {|NA, NB, Key K|} ~: set evs -->            \
   257 \            Key K ~: analz (spies evs)";
   253 \            Key K ~: analz (spies evs)";
   258 by (etac otway.induct 1);
   254 by (etac otway.induct 1);
   259 by analz_spies_tac;
   255 by analz_spies_tac;
   260 by (ALLGOALS
   256 by (ALLGOALS
   261     (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
   257     (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
   274 goal thy 
   270 goal thy 
   275  "!!evs. [| Says Server B                                           \
   271  "!!evs. [| Says Server B                                           \
   276 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   272 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   277 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   273 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   278 \             : set evs;                                            \
   274 \             : set evs;                                            \
   279 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   275 \           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   280 \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   276 \           A ~: bad;  B ~: bad;  evs : otway |]                    \
   281 \        ==> Key K ~: analz (spies evs)";
   277 \        ==> Key K ~: analz (spies evs)";
   282 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   278 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   283 by (blast_tac (claset() addSEs [lemma]) 1);
   279 by (blast_tac (claset() addSEs [lemma]) 1);
   284 qed "Spy_not_see_encrypted_key";
   280 qed "Spy_not_see_encrypted_key";
   285 
   281