Added some more explicit guarantees of key secrecy for agents
authorpaulson
Thu Feb 05 10:38:34 1998 +0100 (1998-02-05)
changeset 4598649bf14debe7
parent 4597 a0bdee64194c
child 4599 3a4348a3d6ff
Added some more explicit guarantees of key secrecy for agents

Deleted spurious A~=Spy assumptions
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Feb 05 10:26:59 1998 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Feb 05 10:38:34 1998 +0100
     1.3 @@ -259,7 +259,7 @@
     1.4  (*Crucial property: If the encrypted message appears, and A has used NA
     1.5    to start a run, then it originated with the Server!*)
     1.6  goal thy 
     1.7 - "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
     1.8 + "!!evs. [| A ~: bad;  evs : otway |]                                  \
     1.9  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
    1.10  \        --> Says A B {|NA, Agent A, Agent B,                          \
    1.11  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
    1.12 @@ -291,10 +291,10 @@
    1.13    bad form of this protocol, even though we can prove
    1.14    Spy_not_see_encrypted_key*)
    1.15  goal thy 
    1.16 - "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
    1.17 -\           Says A  B {|NA, Agent A, Agent B,                       \
    1.18 + "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
    1.19  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
    1.20 -\           A ~: bad;  A ~= Spy;  evs : otway |]                  \
    1.21 +\           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
    1.22 +\           A ~: bad;  evs : otway |]                              \
    1.23  \        ==> EX NB. Says Server B                                  \
    1.24  \                     {|NA,                                        \
    1.25  \                       Crypt (shrK A) {|NA, Key K|},              \
    1.26 @@ -343,6 +343,19 @@
    1.27  qed "Spy_not_see_encrypted_key";
    1.28  
    1.29  
    1.30 +(*A's guarantee.  The Oops premise quantifies over NB because A cannot know
    1.31 +  what it is.*)
    1.32 +goal thy 
    1.33 + "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
    1.34 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
    1.35 +\           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
    1.36 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
    1.37 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    1.38 +\        ==> Key K ~: analz (spies evs)";
    1.39 +by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
    1.40 +qed "A_gets_good_key";
    1.41 +
    1.42 +
    1.43  (**** Authenticity properties relating to NB ****)
    1.44  
    1.45  (*Only OR2 can have caused such a part of a message to appear.  We do not
    1.46 @@ -363,8 +376,8 @@
    1.47  (** The Nonce NB uniquely identifies B's  message. **)
    1.48  
    1.49  goal thy 
    1.50 - "!!evs. [| evs : otway; B ~: bad |]                    \
    1.51 -\ ==> EX NA' A'. ALL NA A.                               \
    1.52 + "!!evs. [| evs : otway; B ~: bad |]  \
    1.53 +\ ==> EX NA' A'. ALL NA A.            \
    1.54  \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
    1.55  \      --> NA = NA' & A = A'";
    1.56  by (parts_induct_tac 1);
    1.57 @@ -387,8 +400,8 @@
    1.58  (*If the encrypted message appears, and B has used Nonce NB,
    1.59    then it originated with the Server!*)
    1.60  goal thy 
    1.61 - "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
    1.62 -\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
    1.63 + "!!evs. [| B ~: bad;  evs : otway |]                                    \
    1.64 +\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)                \
    1.65  \        --> (ALL X'. Says B Server                                      \
    1.66  \                       {|NA, Agent A, Agent B, X',                      \
    1.67  \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
    1.68 @@ -418,11 +431,11 @@
    1.69  (*Guarantee for B: if it gets a message with matching NB then the Server
    1.70    has sent the correct message.*)
    1.71  goal thy 
    1.72 - "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
    1.73 -\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    1.74 -\           Says B Server {|NA, Agent A, Agent B, X',              \
    1.75 + "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
    1.76  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
    1.77 -\            : set evs |]                                          \
    1.78 +\            : set evs;                                            \
    1.79 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
    1.80 +\           B ~: bad;  evs : otway |]                              \
    1.81  \        ==> Says Server B                                         \
    1.82  \                 {|NA,                                            \
    1.83  \                   Crypt (shrK A) {|NA, Key K|},                  \
    1.84 @@ -432,11 +445,21 @@
    1.85  qed "B_trusts_OR3";
    1.86  
    1.87  
    1.88 -B_trusts_OR3 RS Spy_not_see_encrypted_key;
    1.89 +(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
    1.90 +goal thy 
    1.91 + "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
    1.92 +\                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
    1.93 +\             : set evs;                                           \
    1.94 +\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
    1.95 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                \
    1.96 +\           A ~: bad;  B ~: bad;  evs : otway |]                   \
    1.97 +\        ==> Key K ~: analz (spies evs)";
    1.98 +by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
    1.99 +qed "B_gets_good_key";
   1.100  
   1.101  
   1.102  goal thy 
   1.103 - "!!evs. [| B ~: bad;  evs : otway |]                           \
   1.104 + "!!evs. [| B ~: bad;  evs : otway |]                            \
   1.105  \        ==> Says Server B                                       \
   1.106  \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   1.107  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   1.108 @@ -454,11 +477,11 @@
   1.109    We could probably prove that X has the expected form, but that is not
   1.110    strictly necessary for authentication.*)
   1.111  goal thy 
   1.112 - "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   1.113 -\           Says A B {|NA, Agent A, Agent B,                                \
   1.114 -\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.115 -\           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
   1.116 -\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   1.117 + "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
   1.118 +\           Says A  B {|NA, Agent A, Agent B,                                \
   1.119 +\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   1.120 +\           A ~: bad;  B ~: bad;  evs : otway |]                             \
   1.121 +\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,               \
   1.122  \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   1.123  \            : set evs";
   1.124  by (blast_tac (claset() addSDs [A_trusts_OR4]
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Feb 05 10:26:59 1998 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Feb 05 10:38:34 1998 +0100
     2.3 @@ -1,11 +1,11 @@
     2.4 -(*  Title:      HOL/Auth/OtwayRees
     2.5 +(*  Title:      HOL/Auth/OtwayRees_AN
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1996  University of Cambridge
     2.9  
    2.10  Inductive relation "otway" for the Otway-Rees protocol.
    2.11  
    2.12 -Simplified version with minimal encryption but explicit messages
    2.13 +Abadi-Needham version: minimal encryption, explicit messages
    2.14  
    2.15  From page 11 of
    2.16    Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    2.17 @@ -147,8 +147,8 @@
    2.18  
    2.19  (*The equality makes the induction hypothesis easier to apply*)
    2.20  goal thy  
    2.21 - "!!evs. evs : otway ==>                                    \
    2.22 -\  ALL K KK. KK <= Compl (range shrK) -->                   \
    2.23 + "!!evs. evs : otway ==>                                 \
    2.24 +\  ALL K KK. KK <= Compl (range shrK) -->                \
    2.25  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    2.26  \            (K : KK | Key K : analz (spies evs))";
    2.27  by (etac otway.induct 1);
    2.28 @@ -162,7 +162,7 @@
    2.29  
    2.30  
    2.31  goal thy
    2.32 - "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
    2.33 + "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>       \
    2.34  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
    2.35  \        (K = KAB | Key K : analz (spies evs))";
    2.36  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    2.37 @@ -280,6 +280,18 @@
    2.38  qed "Spy_not_see_encrypted_key";
    2.39  
    2.40  
    2.41 +(*A's guarantee.  The Oops premise quantifies over NB because A cannot know
    2.42 +  what it is.*)
    2.43 +goal thy 
    2.44 + "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
    2.45 +\            : set evs;                                                 \
    2.46 +\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
    2.47 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
    2.48 +\        ==> Key K ~: analz (spies evs)";
    2.49 +by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
    2.50 +qed "A_gets_good_key";
    2.51 +
    2.52 +
    2.53  (**** Authenticity properties relating to NB ****)
    2.54  
    2.55  (*If the encrypted message appears then it originated with the Server!*)
    2.56 @@ -301,12 +313,23 @@
    2.57  (*Guarantee for B: if it gets a well-formed certificate then the Server
    2.58    has sent the correct message in round 3.*)
    2.59  goal thy 
    2.60 - "!!evs. [| B ~: bad;  evs : otway;                                        \
    2.61 -\           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    2.62 -\            : set evs |]                                                   \
    2.63 + "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    2.64 +\             : set evs;                                                    \
    2.65 +\           B ~: bad;  evs : otway |]                                       \
    2.66  \        ==> EX NA. Says Server B                                           \
    2.67  \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
    2.68  \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
    2.69  \                     : set evs";
    2.70  by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1);
    2.71  qed "B_trusts_OR3";
    2.72 +
    2.73 +
    2.74 +(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
    2.75 +goal thy 
    2.76 + "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
    2.77 +\            : set evs;                                            \
    2.78 +\           ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                \
    2.79 +\           A ~: bad;  B ~: bad;  evs : otway |]                   \
    2.80 +\        ==> Key K ~: analz (spies evs)";
    2.81 +by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
    2.82 +qed "B_gets_good_key";
     3.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Feb 05 10:26:59 1998 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Feb 05 10:38:34 1998 +0100
     3.3 @@ -266,8 +266,8 @@
     3.4  (*Only it is FALSE.  Somebody could make a fake message to Server
     3.5            substituting some other nonce NA' for NB.*)
     3.6  goal thy 
     3.7 - "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                    \
     3.8 -\        ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
     3.9 + "!!evs. [| A ~: bad;  evs : otway |]                                \
    3.10 +\        ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) -->    \
    3.11  \            Says A B {|NA, Agent A, Agent B,                        \
    3.12  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}    \
    3.13  \             : set evs -->                                          \
     4.1 --- a/src/HOL/Auth/Recur.ML	Thu Feb 05 10:26:59 1998 +0100
     4.2 +++ b/src/HOL/Auth/Recur.ML	Thu Feb 05 10:38:34 1998 +0100
     4.3 @@ -22,7 +22,7 @@
     4.4  (*Simplest case: Alice goes directly to the server*)
     4.5  goal thy
     4.6   "!!A. A ~= Server                                                      \
     4.7 -\ ==> EX K NA. EX evs: recur.                                      \
     4.8 +\ ==> EX K NA. EX evs: recur.                                           \
     4.9  \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
    4.10  \                     Agent Server|}  : set evs";
    4.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    4.12 @@ -35,7 +35,7 @@
    4.13  (*Case two: Alice, Bob and the server*)
    4.14  goal thy
    4.15   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
    4.16 -\ ==> EX K. EX NA. EX evs: recur.                          \
    4.17 +\ ==> EX K. EX NA. EX evs: recur.                               \
    4.18  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
    4.19  \                  Agent Server|}  : set evs";
    4.20  by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
    4.21 @@ -54,7 +54,7 @@
    4.22    TOO SLOW to run every time!
    4.23  goal thy
    4.24   "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
    4.25 -\ ==> EX K. EX NA. EX evs: recur.                                 \
    4.26 +\ ==> EX K. EX NA. EX evs: recur.                                      \
    4.27  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
    4.28  \                  Agent Server|}  : set evs";
    4.29  by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
    4.30 @@ -223,8 +223,8 @@
    4.31  
    4.32  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
    4.33  goal thy  
    4.34 - "!!evs. evs : recur ==>                                    \
    4.35 -\  ALL K KK. KK <= Compl (range shrK) -->                   \
    4.36 + "!!evs. evs : recur ==>                                 \
    4.37 +\  ALL K KK. KK <= Compl (range shrK) -->                \
    4.38  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    4.39  \            (K : KK | Key K : analz (spies evs))";
    4.40  by (etac recur.induct 1);
    4.41 @@ -251,7 +251,7 @@
    4.42              (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
    4.43  
    4.44  goal thy
    4.45 - "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
    4.46 + "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>           \
    4.47  \        Key K : analz (insert (Key KAB) (spies evs)) =      \
    4.48  \        (K = KAB | Key K : analz (spies evs))";
    4.49  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    4.50 @@ -260,7 +260,7 @@
    4.51  
    4.52  (*Everything that's hashed is already in past traffic. *)
    4.53  goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
    4.54 -\                   evs : recur;  A ~: bad |]                       \
    4.55 +\                   evs : recur;  A ~: bad |]                     \
    4.56  \                ==> X : parts (spies evs)";
    4.57  by (etac rev_mp 1);
    4.58  by (parts_induct_tac 1);
    4.59 @@ -296,9 +296,9 @@
    4.60  val lemma = result();
    4.61  
    4.62  goalw thy [HPair_def]
    4.63 - "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts(spies evs); \
    4.64 -\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(spies evs); \
    4.65 -\        evs : recur;  A ~: bad |]                                     \
    4.66 + "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts (spies evs); \
    4.67 +\        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
    4.68 +\        evs : recur;  A ~: bad |]                                    \
    4.69  \      ==> B=B' & P=P'";
    4.70  by (REPEAT (eresolve_tac partsEs 1));
    4.71  by (prove_unique_tac lemma 1);
    4.72 @@ -357,7 +357,7 @@
    4.73  (*The last key returned by respond indeed appears in a certificate*)
    4.74  goal thy 
    4.75   "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
    4.76 -\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
    4.77 +\      ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
    4.78  by (etac respond.elim 1);
    4.79  by (ALLGOALS Asm_full_simp_tac);
    4.80  qed "respond_certificate";
    4.81 @@ -376,8 +376,8 @@
    4.82  by (expand_case_tac "K = KBC" 1);
    4.83  by (dtac respond_Key_in_parts 1);
    4.84  by (blast_tac (claset() addSIs [exI]
    4.85 -                       addSEs partsEs
    4.86 -                       addDs [Key_in_parts_respond]) 1);
    4.87 +                        addSEs partsEs
    4.88 +                        addDs [Key_in_parts_respond]) 1);
    4.89  by (expand_case_tac "K = KAB" 1);
    4.90  by (REPEAT (ares_tac [exI] 2));
    4.91  by (ex_strip_tac 1);
    4.92 @@ -400,7 +400,7 @@
    4.93  
    4.94  goal thy 
    4.95   "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
    4.96 -\        ==> ALL A A' N. A ~: bad & A' ~: bad -->                 \
    4.97 +\        ==> ALL A A' N. A ~: bad & A' ~: bad -->                   \
    4.98  \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
    4.99  \            Key K ~: analz (insert RB (spies evs))";
   4.100  by (etac respond.induct 1);
   4.101 @@ -495,8 +495,8 @@
   4.102  (*Certificates can only originate with the Server.*)
   4.103  goal thy 
   4.104   "!!evs. [| Crypt (shrK A) Y : parts (spies evs);    \
   4.105 -\           A ~: bad;  A ~= Spy;  evs : recur |]       \
   4.106 -\        ==> EX C RC. Says Server C RC : set evs  &     \
   4.107 +\           A ~: bad;  evs : recur |]                \
   4.108 +\        ==> EX C RC. Says Server C RC : set evs  &  \
   4.109  \                     Crypt (shrK A) Y : parts {RC}";
   4.110  by (etac rev_mp 1);
   4.111  by (parts_induct_tac 1);
     5.1 --- a/src/HOL/Auth/Yahalom.ML	Thu Feb 05 10:26:59 1998 +0100
     5.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Feb 05 10:38:34 1998 +0100
     5.3 @@ -255,6 +255,14 @@
     5.4  by (Fake_parts_insert_tac 1);
     5.5  qed "A_trusts_YM3";
     5.6  
     5.7 +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
     5.8 +goal thy
     5.9 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
    5.10 +\           Notes Spy {|na, nb, Key K|} ~: set evs;               \
    5.11 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    5.12 +\        ==> Key K ~: analz (spies evs)";
    5.13 +by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
    5.14 +qed "A_gets_good_key";
    5.15  
    5.16  (** Security Guarantees for B upon receiving YM4 **)
    5.17  
    5.18 @@ -541,11 +549,11 @@
    5.19    If this run is broken and the spy substitutes a certificate containing an
    5.20    old key, B has no means of telling.*)
    5.21  goal thy 
    5.22 - "!!evs. [| Says B Server                                                   \
    5.23 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    5.24 +\                       Crypt K (Nonce NB)|} : set evs;                     \
    5.25 +\           Says B Server                                                   \
    5.26  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
    5.27  \             : set evs;                                                    \
    5.28 -\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    5.29 -\                       Crypt K (Nonce NB)|} : set evs;                     \
    5.30  \           ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
    5.31  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    5.32  \         ==> Says Server A                                                 \
    5.33 @@ -564,6 +572,19 @@
    5.34  qed "B_trusts_YM4";
    5.35  
    5.36  
    5.37 +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
    5.38 +goal thy 
    5.39 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    5.40 +\                       Crypt K (Nonce NB)|} : set evs;                     \
    5.41 +\           Says B Server                                                   \
    5.42 +\             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
    5.43 +\             : set evs;                                                    \
    5.44 +\           ALL k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs;          \
    5.45 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    5.46 +\        ==> Key K ~: analz (spies evs)";
    5.47 +by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
    5.48 +qed "B_gets_good_key";
    5.49 +
    5.50  
    5.51  (*** Authenticating B to A ***)
    5.52  
    5.53 @@ -638,15 +659,15 @@
    5.54    Moreover, A associates K with NB (thus is talking about the same run).
    5.55    Other premises guarantee secrecy of K.*)
    5.56  goal thy 
    5.57 - "!!evs. [| Says B Server                                                   \
    5.58 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    5.59 +\                       Crypt K (Nonce NB)|} : set evs;                     \
    5.60 +\           Says B Server                                                   \
    5.61  \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
    5.62  \             : set evs;                                                    \
    5.63 -\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
    5.64 -\                       Crypt K (Nonce NB)|} : set evs;                     \
    5.65  \           (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs);     \
    5.66  \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
    5.67  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
    5.68 -by (dtac B_trusts_YM4 1);
    5.69 +by (forward_tac [B_trusts_YM4] 1);
    5.70  by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
    5.71  by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
    5.72  by (rtac lemma 1);
     6.1 --- a/src/HOL/Auth/Yahalom2.ML	Thu Feb 05 10:26:59 1998 +0100
     6.2 +++ b/src/HOL/Auth/Yahalom2.ML	Thu Feb 05 10:38:34 1998 +0100
     6.3 @@ -261,6 +261,15 @@
     6.4  by (Blast_tac 1);
     6.5  qed "A_trusts_YM3";
     6.6  
     6.7 +(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
     6.8 +goal thy
     6.9 + "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \
    6.10 +\           ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs;            \
    6.11 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
    6.12 +\        ==> Key K ~: analz (spies evs)";
    6.13 +by (blast_tac (claset() addSDs [A_trusts_YM3, Spy_not_see_encrypted_key]) 1);
    6.14 +qed "A_gets_good_key";
    6.15 +
    6.16  
    6.17  (** Security Guarantee for B upon receiving YM4 **)
    6.18  
    6.19 @@ -301,6 +310,17 @@
    6.20  qed "B_trusts_YM4";
    6.21  
    6.22  
    6.23 +(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
    6.24 +goal thy 
    6.25 + "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
    6.26 +\             : set evs;                                                 \
    6.27 +\           ALL na. Notes Spy {|na, Nonce NB, Key K|} ~: set evs;        \
    6.28 +\           A ~: bad;  B ~: bad;  evs : yahalom |]                \
    6.29 +\        ==> Key K ~: analz (spies evs)";
    6.30 +by (blast_tac (claset() addSDs [B_trusts_YM4, Spy_not_see_encrypted_key]) 1);
    6.31 +qed "B_gets_good_key";
    6.32 +
    6.33 +
    6.34  
    6.35  (*** Authenticating B to A ***)
    6.36  
    6.37 @@ -318,6 +338,7 @@
    6.38  by (Blast_tac 1);
    6.39  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
    6.40  
    6.41 +
    6.42  (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
    6.43  goal thy 
    6.44   "!!evs. evs : yahalom                                                   \