src/HOL/Auth/Yahalom2.ML
changeset 4598 649bf14debe7
parent 4537 4e835bd9fada
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Feb 05 10:26:59 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Feb 05 10:38:34 1998 +0100
     1.3 @@ -261,6 +261,15 @@
     1.4  by (Blast_tac 1);
     1.5  qed "A_trusts_YM3";
     1.6  
     1.7 +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
     1.8 +goal thy
     1.9 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \
    1.10 +\           ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs;            \
    1.11 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
    1.12 +\        ==> Key K ~: analz (spies evs)";
    1.13 +by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
    1.14 +qed "A_gets_good_key";
    1.15 +
    1.16  
    1.17  (** Security Guarantee for B upon receiving YM4 **)
    1.18  
    1.19 @@ -301,6 +310,17 @@
    1.20  qed "B_trusts_YM4";
    1.21  
    1.22  
    1.23 +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
    1.24 +goal thy 
    1.25 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
    1.26 +\             : set evs;                                                 \
    1.27 +\           ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;        \
    1.28 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    1.29 +\        ==> Key K ~: analz (spies evs)";
    1.30 +by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
    1.31 +qed "B_gets_good_key";
    1.32 +
    1.33 +
    1.34  
    1.35  (*** Authenticating B to A ***)
    1.36  
    1.37 @@ -318,6 +338,7 @@
    1.38  by (Blast_tac 1);
    1.39  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
    1.40  
    1.41 +
    1.42  (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
    1.43  goal thy 
    1.44   "!!evs. evs : yahalom                                                   \