fixed a faulty proof
authorpaulson
Mon Jun 20 15:54:39 2005 +0200 (2005-06-20)
changeset 16474c3c0208988c0
parent 16473 b24c820a0b85
child 16475 8f3ba52a7937
fixed a faulty proof
src/HOL/SET-Protocol/Purchase.thy
     1.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Mon Jun 20 15:54:22 2005 +0200
     1.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Mon Jun 20 15:54:39 2005 +0200
     1.3 @@ -814,19 +814,26 @@
     1.4  text{*When M receives AuthRes, he knows that P signed it, including
     1.5    the identifying tags and the purchase amount, which he can verify.
     1.6    (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
     1.7 -   send the same message to M.)*}
     1.8 +   send the same message to M.)  The conclusion is weak: M is existentially
     1.9 +  quantified! That is because Authorization Response does not refer to M, while
    1.10 +  the digital envelope weakens the link between @{term MsgAuthRes} and
    1.11 +  @{term"priSK M"}.  Changing the precondition to refer to 
    1.12 +  @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
    1.13 +  otherwise the Spy could create that message.*}
    1.14  theorem M_verifies_AuthRes:
    1.15 -  "[| MsgAuthRes = {|Number LID_M, Number XID, Number PurchAmt|};
    1.16 +  "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 
    1.17 +                     Hash authCode|};
    1.18        Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
    1.19 -      evs \<in> set_pur;  PG j \<notin> bad|]
    1.20 -   ==> \<exists>i KM HOIData HOD P_I.
    1.21 +      PG j \<notin> bad;  evs \<in> set_pur|]
    1.22 +   ==> \<exists>M KM KP HOIData HOD P_I.
    1.23  	Gets (PG j)
    1.24 -	   (EncB (priSK (Merchant i)) KM (pubEK (PG j))
    1.25 +	   (EncB (priSK M) KM (pubEK (PG j))
    1.26  		    {|Number LID_M, Number XID, HOIData, HOD|}
    1.27  		    P_I) \<in> set evs &
    1.28 -	Says (PG j) (Merchant i)
    1.29 -	     (Crypt (pubEK (Merchant i)) (sign (priSK (PG j)) MsgAuthRes))
    1.30 -          \<in> set evs"
    1.31 +	Says (PG j) M
    1.32 +	     (EncB (priSK (PG j)) KP (pubEK M)
    1.33 +	      {|Number LID_M, Number XID, Number PurchAmt|}
    1.34 +	      authCode) \<in> set evs"
    1.35  apply clarify
    1.36  apply (erule rev_mp)
    1.37  apply (erule set_pur.induct)