src/HOL/SET_Protocol/Purchase.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 59499 14095f771781
child 61984 cdea44c775fa
permissions -rw-r--r--
isabelle update_cartouches;
wenzelm@33028
     1
(*  Title:      HOL/SET_Protocol/Purchase.thy
wenzelm@32960
     2
    Author:     Giampaolo Bella
wenzelm@32960
     3
    Author:     Fabio Massacci
wenzelm@32960
     4
    Author:     Lawrence C Paulson
paulson@14199
     5
*)
paulson@14199
     6
wenzelm@58889
     7
section{*Purchase Phase of SET*}
paulson@14199
     8
wenzelm@33028
     9
theory Purchase
wenzelm@33028
    10
imports Public_SET
wenzelm@33028
    11
begin
paulson@14199
    12
paulson@14199
    13
text{*
paulson@14199
    14
Note: nonces seem to consist of 20 bytes.  That includes both freshness
paulson@14199
    15
challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
paulson@14199
    16
paulson@14199
    17
This version omits @{text LID_C} but retains @{text LID_M}. At first glance
paulson@14199
    18
(Programmer's Guide page 267) it seems that both numbers are just introduced
paulson@14199
    19
for the respective convenience of the Cardholder's and Merchant's
paulson@14199
    20
system. However, omitting both of them would create a problem of
paulson@14199
    21
identification: how can the Merchant's system know what transaction is it
paulson@14199
    22
supposed to process?
paulson@14199
    23
paulson@14199
    24
Further reading (Programmer's guide page 309) suggest that there is an outside
paulson@14199
    25
bootstrapping message (SET initiation message) which is used by the Merchant
paulson@14199
    26
and the Cardholder to agree on the actual transaction. This bootstrapping
paulson@14199
    27
message is described in the SET External Interface Guide and ought to generate
paulson@14199
    28
@{text LID_M}. According SET Extern Interface Guide, this number might be a
paulson@14199
    29
cookie, an invoice number etc. The Programmer's Guide on page 310, states that
paulson@14199
    30
in absence of @{text LID_M} the protocol must somehow ("outside SET") identify
paulson@14199
    31
the transaction from OrderDesc, which is assumed to be a searchable text only
paulson@14199
    32
field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed
paulson@14199
    33
out-of-bad on the value of @{text LID_M} (for instance a cookie in a web
paulson@14199
    34
transaction etc.). This out-of-band agreement is expressed with a preliminary
paulson@14199
    35
start action in which the merchant and the Cardholder agree on the appropriate
paulson@14199
    36
values. Agreed values are stored with a suitable notes action.
paulson@14199
    37
paulson@14199
    38
"XID is a transaction ID that is usually generated by the Merchant system,
paulson@14199
    39
unless there is no PInitRes, in which case it is generated by the Cardholder
paulson@14199
    40
system. It is a randomly generated 20 byte variable that is globally unique
paulson@14199
    41
(statistically). Merchant and Cardholder systems shall use appropriate random
paulson@14199
    42
number generators to ensure the global uniqueness of XID."
paulson@14199
    43
--Programmer's Guide, page 267.
paulson@14199
    44
paulson@14199
    45
PI (Payment Instruction) is the most central and sensitive data structure in
paulson@14199
    46
SET. It is used to pass the data required to authorize a payment card payment
paulson@14199
    47
from the Cardholder to the Payment Gateway, which will use the data to
paulson@14199
    48
initiate a payment card transaction through the traditional payment card
paulson@14199
    49
financial network. The data is encrypted by the Cardholder and sent via the
paulson@14199
    50
Merchant, such that the data is hidden from the Merchant unless the Acquirer
paulson@14199
    51
passes the data back to the Merchant.
paulson@14199
    52
--Programmer's Guide, page 271.*}
paulson@14199
    53
paulson@14199
    54
consts
paulson@14199
    55
paulson@14199
    56
    CardSecret :: "nat => nat"
paulson@15481
    57
     --{*Maps Cardholders to CardSecrets.
paulson@15481
    58
         A CardSecret of 0 means no cerificate, must use unsigned format.*}
paulson@14199
    59
paulson@14199
    60
    PANSecret :: "nat => nat"
paulson@15481
    61
     --{*Maps Cardholders to PANSecrets.*}
paulson@14199
    62
berghofe@23755
    63
inductive_set
berghofe@23755
    64
  set_pur :: "event list set"
berghofe@23755
    65
where
paulson@14199
    66
paulson@14199
    67
  Nil:   --{*Initial trace is empty*}
wenzelm@32960
    68
         "[] \<in> set_pur"
paulson@14199
    69
berghofe@23755
    70
| Fake:  --{*The spy MAY say anything he CAN say.*}
wenzelm@32960
    71
         "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]
wenzelm@32960
    72
          ==> Says Spy B X  # evsf \<in> set_pur"
paulson@14199
    73
paulson@14199
    74
berghofe@23755
    75
| Reception: --{*If A sends a message X to B, then B might receive it*}
wenzelm@32960
    76
             "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]
wenzelm@32960
    77
              ==> Gets B X  # evsr \<in> set_pur"
paulson@14199
    78
berghofe@23755
    79
| Start: 
paulson@14199
    80
      --{*Added start event which is out-of-band for SET: the Cardholder and
wenzelm@32960
    81
          the merchant agree on the amounts and uses @{text LID_M} as an
paulson@14199
    82
          identifier.
wenzelm@32960
    83
          This is suggested by the External Interface Guide. The Programmer's
wenzelm@32960
    84
          Guide, in absence of @{text LID_M}, states that the merchant uniquely
wenzelm@32960
    85
          identifies the order out of some data contained in OrderDesc.*}
paulson@14199
    86
   "[|evsStart \<in> set_pur;
paulson@14199
    87
      Number LID_M \<notin> used evsStart;
paulson@14199
    88
      C = Cardholder k; M = Merchant i; P = PG j;
paulson@14199
    89
      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
    90
      LID_M \<notin> range CardSecret;
paulson@14199
    91
      LID_M \<notin> range PANSecret |]
paulson@14199
    92
     ==> Notes C {|Number LID_M, Transaction|}
paulson@14199
    93
       # Notes M {|Number LID_M, Agent P, Transaction|}
paulson@14199
    94
       # evsStart \<in> set_pur"
paulson@14199
    95
berghofe@23755
    96
| PInitReq:
paulson@14199
    97
     --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
paulson@14199
    98
   "[|evsPIReq \<in> set_pur;
paulson@14199
    99
      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   100
      Nonce Chall_C \<notin> used evsPIReq;
paulson@14199
   101
      Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;
paulson@14199
   102
      Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
paulson@14199
   103
    ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
paulson@14199
   104
berghofe@23755
   105
| PInitRes:
paulson@14199
   106
     --{*Merchant replies with his own label XID and the encryption
wenzelm@32960
   107
         key certificate of his chosen Payment Gateway. Page 74 of Formal
paulson@14199
   108
         Protocol Desc. We use @{text LID_M} to identify Cardholder*}
paulson@14199
   109
   "[|evsPIRes \<in> set_pur;
paulson@14199
   110
      Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;
paulson@14199
   111
      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   112
      Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;
paulson@14199
   113
      Nonce Chall_M \<notin> used evsPIRes;
paulson@14199
   114
      Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;
paulson@14199
   115
      Number XID \<notin> used evsPIRes;
paulson@14199
   116
      XID \<notin> range CardSecret; XID \<notin> range PANSecret|]
paulson@14199
   117
    ==> Says M C (sign (priSK M)
wenzelm@32960
   118
                       {|Number LID_M, Number XID,
wenzelm@32960
   119
                         Nonce Chall_C, Nonce Chall_M,
wenzelm@32960
   120
                         cert P (pubEK P) onlyEnc (priSK RCA)|})
paulson@14199
   121
          # evsPIRes \<in> set_pur"
paulson@14199
   122
berghofe@23755
   123
| PReqUns:
paulson@14199
   124
      --{*UNSIGNED Purchase request (CardSecret = 0).
wenzelm@32960
   125
        Page 79 of Formal Protocol Desc.
wenzelm@32960
   126
        Merchant never sees the amount in clear. This holds of the real
wenzelm@32960
   127
        protocol, where XID identifies the transaction. We omit
wenzelm@32960
   128
        Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
wenzelm@32960
   129
        the CardSecret is 0 and because AuthReq treated the unsigned case
wenzelm@32960
   130
        very differently from the signed one anyway.*}
berghofe@23755
   131
   "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
berghofe@23755
   132
    [|evsPReqU \<in> set_pur;
paulson@14199
   133
      C = Cardholder k; CardSecret k = 0;
paulson@14199
   134
      Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
paulson@14199
   135
      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   136
      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
paulson@14199
   137
      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};
paulson@14199
   138
      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
paulson@14199
   139
      Gets C (sign (priSK M)
wenzelm@32960
   140
                   {|Number LID_M, Number XID,
wenzelm@32960
   141
                     Nonce Chall_C, Nonce Chall_M,
wenzelm@32960
   142
                     cert P EKj onlyEnc (priSK RCA)|})
wenzelm@32960
   143
        \<in> set evsPReqU;
paulson@14199
   144
      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;
paulson@14199
   145
      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]
paulson@14199
   146
    ==> Says C M
wenzelm@32960
   147
             {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
wenzelm@32960
   148
               OIData, Hash{|PIHead, Pan (pan C)|} |}
wenzelm@32960
   149
          # Notes C {|Key KC1, Agent M|}
wenzelm@32960
   150
          # evsPReqU \<in> set_pur"
paulson@14199
   151
berghofe@23755
   152
| PReqS:
paulson@14199
   153
      --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
paulson@14199
   154
          We could specify the equation
wenzelm@32960
   155
          @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
wenzelm@32960
   156
          Formal Desc. gives PIHead the same format in the unsigned case.
wenzelm@32960
   157
          However, there's little point, as P treats the signed and 
paulson@14199
   158
          unsigned cases differently.*}
berghofe@23755
   159
   "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData
berghofe@23755
   160
      OIDualSigned OrderDesc P PANData PIData PIDualSigned
berghofe@23755
   161
      PIHead PurchAmt Transaction XID evsPReqS k.
berghofe@23755
   162
    [|evsPReqS \<in> set_pur;
paulson@14199
   163
      C = Cardholder k;
paulson@14199
   164
      CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
paulson@14199
   165
      Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   166
      HOD = Hash{|Number OrderDesc, Number PurchAmt|};
paulson@14199
   167
      OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};
paulson@14199
   168
      PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
wenzelm@32960
   169
                  Hash{|Number XID, Nonce (CardSecret k)|}|};
paulson@14199
   170
      PANData = {|Pan (pan C), Nonce (PANSecret k)|};
paulson@14199
   171
      PIData = {|PIHead, PANData|};
paulson@14199
   172
      PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},
wenzelm@32960
   173
                       EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};
paulson@14199
   174
      OIDualSigned = {|OIData, Hash PIData|};
paulson@14199
   175
      Gets C (sign (priSK M)
wenzelm@32960
   176
                   {|Number LID_M, Number XID,
wenzelm@32960
   177
                     Nonce Chall_C, Nonce Chall_M,
wenzelm@32960
   178
                     cert P EKj onlyEnc (priSK RCA)|})
wenzelm@32960
   179
        \<in> set evsPReqS;
paulson@14199
   180
      Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;
paulson@14199
   181
      Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]
paulson@14199
   182
    ==> Says C M {|PIDualSigned, OIDualSigned|}
wenzelm@32960
   183
          # Notes C {|Key KC2, Agent M|}
wenzelm@32960
   184
          # evsPReqS \<in> set_pur"
paulson@14199
   185
paulson@14199
   186
  --{*Authorization Request.  Page 92 of Formal Protocol Desc.
paulson@14199
   187
    Sent in response to Purchase Request.*}
berghofe@23755
   188
| AuthReq:
paulson@14199
   189
   "[| evsAReq \<in> set_pur;
paulson@14199
   190
       Key KM \<notin> used evsAReq;  KM \<in> symKeys;
paulson@14199
   191
       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   192
       HOD = Hash{|Number OrderDesc, Number PurchAmt|};
paulson@14199
   193
       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,
wenzelm@32960
   194
                  Nonce Chall_M|};
paulson@14199
   195
       CardSecret k \<noteq> 0 -->
wenzelm@32960
   196
         P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
paulson@14199
   197
       Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;
paulson@14199
   198
       Says M C (sign (priSK M) {|Number LID_M, Number XID,
wenzelm@32960
   199
                                  Nonce Chall_C, Nonce Chall_M,
wenzelm@32960
   200
                                  cert P EKj onlyEnc (priSK RCA)|})
wenzelm@32960
   201
         \<in> set evsAReq;
wenzelm@32960
   202
        Notes M {|Number LID_M, Agent P, Transaction|}
wenzelm@32960
   203
           \<in> set evsAReq |]
paulson@14199
   204
    ==> Says M P
wenzelm@32960
   205
             (EncB (priSK M) KM (pubEK P)
wenzelm@32960
   206
               {|Number LID_M, Number XID, Hash OIData, HOD|}   P_I)
wenzelm@32960
   207
          # evsAReq \<in> set_pur"
paulson@14199
   208
paulson@14199
   209
  --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
paulson@14199
   210
    Page 99 of Formal Protocol Desc.
paulson@14199
   211
    PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and
paulson@14199
   212
    HOIData occur independently in @{text P_I} and in M's message.
paulson@14199
   213
    The authCode in AuthRes represents the baggage of EncB, which in the
paulson@14199
   214
    full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
paulson@14199
   215
    optional items for split shipments, recurring payments, etc.*}
paulson@14199
   216
berghofe@23755
   217
| AuthResUns:
paulson@14199
   218
    --{*Authorization Response, UNSIGNED*}
paulson@14199
   219
   "[| evsAResU \<in> set_pur;
paulson@14199
   220
       C = Cardholder k; M = Merchant i;
paulson@14199
   221
       Key KP \<notin> used evsAResU;  KP \<in> symKeys;
paulson@14199
   222
       CardSecret k = 0;  KC1 \<in> symKeys;  KM \<in> symKeys;
paulson@14199
   223
       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
paulson@14199
   224
       P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));
paulson@14199
   225
       Gets P (EncB (priSK M) KM (pubEK P)
wenzelm@32960
   226
               {|Number LID_M, Number XID, HOIData, HOD|} P_I)
wenzelm@32960
   227
           \<in> set evsAResU |]
paulson@14199
   228
   ==> Says P M
wenzelm@32960
   229
            (EncB (priSK P) KP (pubEK M)
wenzelm@32960
   230
              {|Number LID_M, Number XID, Number PurchAmt|}
wenzelm@32960
   231
              authCode)
paulson@14199
   232
       # evsAResU \<in> set_pur"
paulson@14199
   233
berghofe@23755
   234
| AuthResS:
paulson@14199
   235
    --{*Authorization Response, SIGNED*}
paulson@14199
   236
   "[| evsAResS \<in> set_pur;
paulson@14199
   237
       C = Cardholder k;
paulson@14199
   238
       Key KP \<notin> used evsAResS;  KP \<in> symKeys;
paulson@14199
   239
       CardSecret k \<noteq> 0;  KC2 \<in> symKeys;  KM \<in> symKeys;
paulson@14199
   240
       P_I = {|sign (priSK C) {|Hash PIData, HOIData|},
wenzelm@32960
   241
               EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};
paulson@14199
   242
       PANData = {|Pan (pan C), Nonce (PANSecret k)|};
paulson@14199
   243
       PIData = {|PIHead, PANData|};
paulson@14199
   244
       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
wenzelm@32960
   245
                  Hash{|Number XID, Nonce (CardSecret k)|}|};
paulson@14199
   246
       Gets P (EncB (priSK M) KM (pubEK P)
wenzelm@32960
   247
                {|Number LID_M, Number XID, HOIData, HOD|}
wenzelm@32960
   248
               P_I)
wenzelm@32960
   249
           \<in> set evsAResS |]
paulson@14199
   250
   ==> Says P M
wenzelm@32960
   251
            (EncB (priSK P) KP (pubEK M)
wenzelm@32960
   252
              {|Number LID_M, Number XID, Number PurchAmt|}
wenzelm@32960
   253
              authCode)
paulson@14199
   254
       # evsAResS \<in> set_pur"
paulson@14199
   255
berghofe@23755
   256
| PRes:
paulson@14199
   257
    --{*Purchase response.*}
paulson@14199
   258
   "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
paulson@14199
   259
       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
paulson@14199
   260
       Gets M (EncB (priSK P) KP (pubEK M)
wenzelm@32960
   261
              {|Number LID_M, Number XID, Number PurchAmt|}
wenzelm@32960
   262
              authCode)
wenzelm@32960
   263
          \<in> set evsPRes;
paulson@14199
   264
       Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
paulson@14199
   265
       Says M P
wenzelm@32960
   266
            (EncB (priSK M) KM (pubEK P)
wenzelm@32960
   267
              {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
wenzelm@32960
   268
         \<in> set evsPRes;
paulson@14199
   269
       Notes M {|Number LID_M, Agent P, Transaction|}
wenzelm@32960
   270
          \<in> set evsPRes
paulson@14199
   271
      |]
paulson@14199
   272
   ==> Says M C
wenzelm@32960
   273
         (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
wenzelm@32960
   274
                           Hash (Number PurchAmt)|})
wenzelm@32960
   275
         # evsPRes \<in> set_pur"
paulson@14199
   276
paulson@14199
   277
paulson@14199
   278
specification (CardSecret PANSecret)
paulson@14199
   279
  inj_CardSecret:  "inj CardSecret"
paulson@14199
   280
  inj_PANSecret:   "inj PANSecret"
paulson@14199
   281
  CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
paulson@14199
   282
    --{*No CardSecret equals any PANSecret*}
huffman@35703
   283
  apply (rule_tac x="curry prod_encode 0" in exI)
huffman@35703
   284
  apply (rule_tac x="curry prod_encode 1" in exI)
huffman@35703
   285
  apply (simp add: prod_encode_eq inj_on_def)
paulson@14199
   286
  done
paulson@14199
   287
paulson@14199
   288
declare Says_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14199
   289
declare parts.Body [dest]
paulson@14199
   290
declare analz_into_parts [dest]
paulson@14199
   291
declare Fake_parts_insert_in_Un [dest]
paulson@14199
   292
paulson@14199
   293
declare CardSecret_neq_PANSecret [iff] 
paulson@14199
   294
        CardSecret_neq_PANSecret [THEN not_sym, iff]
paulson@14199
   295
declare inj_CardSecret [THEN inj_eq, iff] 
paulson@14199
   296
        inj_PANSecret [THEN inj_eq, iff]
paulson@14199
   297
paulson@14199
   298
paulson@14199
   299
subsection{*Possibility Properties*}
paulson@14199
   300
paulson@14199
   301
lemma Says_to_Gets:
paulson@14199
   302
     "Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"
paulson@14199
   303
by (rule set_pur.Reception, auto)
paulson@14199
   304
paulson@14206
   305
text{*Possibility for UNSIGNED purchases. Note that we need to ensure
paulson@14206
   306
that XID differs from OrderDesc and PurchAmt, since it is supposed to be
paulson@14206
   307
a unique number!*}
paulson@14199
   308
lemma possibility_Uns:
paulson@14206
   309
    "[| CardSecret k = 0;
paulson@14206
   310
        C = Cardholder k;  M = Merchant i;
wenzelm@32960
   311
        Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
wenzelm@32960
   312
        KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
wenzelm@32960
   313
        KC < KM; KM < KP;
wenzelm@32960
   314
        Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   315
        Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
wenzelm@32960
   316
        Chall_C < Chall_M; 
paulson@14206
   317
        Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   318
        Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   319
        LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 
paulson@14206
   320
   ==> \<exists>evs \<in> set_pur.
paulson@14206
   321
          Says M C
paulson@14206
   322
               (sign (priSK M)
paulson@14206
   323
                    {|Number LID_M, Number XID, Nonce Chall_C, 
paulson@14206
   324
                      Hash (Number PurchAmt)|})
paulson@14206
   325
                  \<in> set evs" 
paulson@14199
   326
apply (intro exI bexI)
paulson@14199
   327
apply (rule_tac [2]
wenzelm@32960
   328
        set_pur.Nil
paulson@14206
   329
         [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
wenzelm@32960
   330
          THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
paulson@14206
   331
          THEN Says_to_Gets, 
wenzelm@32960
   332
          THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
paulson@14206
   333
          THEN Says_to_Gets,
wenzelm@32960
   334
          THEN set_pur.PReqUns [of concl: C M KC],
paulson@14206
   335
          THEN Says_to_Gets, 
wenzelm@32960
   336
          THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
paulson@14206
   337
          THEN Says_to_Gets, 
wenzelm@32960
   338
          THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
paulson@14206
   339
          THEN Says_to_Gets, 
wenzelm@32960
   340
          THEN set_pur.PRes]) 
wenzelm@30607
   341
apply basic_possibility
paulson@14206
   342
apply (simp_all add: used_Cons symKeys_neq_imp_neq) 
paulson@14199
   343
done
paulson@14199
   344
paulson@14199
   345
lemma possibility_S:
paulson@14206
   346
    "[| CardSecret k \<noteq> 0;
paulson@14206
   347
        C = Cardholder k;  M = Merchant i;
wenzelm@32960
   348
        Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
wenzelm@32960
   349
        KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
wenzelm@32960
   350
        KC < KM; KM < KP;
wenzelm@32960
   351
        Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   352
        Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
wenzelm@32960
   353
        Chall_C < Chall_M; 
paulson@14206
   354
        Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   355
        Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
paulson@14206
   356
        LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 
paulson@14206
   357
   ==>  \<exists>evs \<in> set_pur.
paulson@14206
   358
            Says M C
paulson@14206
   359
                 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, 
paulson@14206
   360
                                   Hash (Number PurchAmt)|})
paulson@14206
   361
               \<in> set evs"
paulson@14199
   362
apply (intro exI bexI)
paulson@14199
   363
apply (rule_tac [2]
wenzelm@32960
   364
        set_pur.Nil
paulson@14206
   365
         [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
wenzelm@32960
   366
          THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
paulson@14206
   367
          THEN Says_to_Gets, 
wenzelm@32960
   368
          THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
paulson@14206
   369
          THEN Says_to_Gets,
wenzelm@32960
   370
          THEN set_pur.PReqS [of concl: C M _ _ KC],
paulson@14206
   371
          THEN Says_to_Gets, 
wenzelm@32960
   372
          THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
paulson@14206
   373
          THEN Says_to_Gets, 
wenzelm@32960
   374
          THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
paulson@14206
   375
          THEN Says_to_Gets, 
wenzelm@32960
   376
          THEN set_pur.PRes]) 
wenzelm@30607
   377
apply basic_possibility
paulson@14206
   378
apply (auto simp add: used_Cons symKeys_neq_imp_neq) 
paulson@14199
   379
done
paulson@14199
   380
paulson@15481
   381
text{*General facts about message reception*}
paulson@14199
   382
lemma Gets_imp_Says:
paulson@14199
   383
     "[| Gets B X \<in> set evs; evs \<in> set_pur |]
paulson@14199
   384
   ==> \<exists>A. Says A B X \<in> set evs"
paulson@14199
   385
apply (erule rev_mp)
paulson@14199
   386
apply (erule set_pur.induct, auto)
paulson@14199
   387
done
paulson@14199
   388
paulson@14199
   389
lemma Gets_imp_knows_Spy:
paulson@14199
   390
     "[| Gets B X \<in> set evs; evs \<in> set_pur |]  ==> X \<in> knows Spy evs"
paulson@14199
   391
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
paulson@14199
   392
paulson@14199
   393
declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
paulson@14199
   394
paulson@14199
   395
text{*Forwarding lemmas, to aid simplification*}
paulson@14199
   396
paulson@14199
   397
lemma AuthReq_msg_in_parts_spies:
paulson@14199
   398
     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
paulson@14199
   399
        evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"
paulson@14199
   400
by auto
paulson@14199
   401
paulson@14199
   402
lemma AuthReq_msg_in_analz_spies:
paulson@14199
   403
     "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
paulson@14199
   404
        evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
paulson@14199
   405
by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
paulson@14199
   406
paulson@14199
   407
paulson@14199
   408
subsection{*Proofs on Asymmetric Keys*}
paulson@14199
   409
paulson@14199
   410
text{*Private Keys are Secret*}
paulson@14199
   411
paulson@14199
   412
text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
paulson@14199
   413
lemma Spy_see_private_Key [simp]:
paulson@14199
   414
     "evs \<in> set_pur
paulson@14199
   415
      ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
paulson@14199
   416
apply (erule set_pur.induct)
paulson@14199
   417
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   418
apply auto
paulson@14199
   419
done
paulson@14199
   420
declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
paulson@14199
   421
paulson@14199
   422
lemma Spy_analz_private_Key [simp]:
paulson@14199
   423
     "evs \<in> set_pur ==>
paulson@14199
   424
     (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
paulson@14199
   425
by auto
paulson@14199
   426
declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
paulson@14199
   427
paulson@14199
   428
text{*rewriting rule for priEK's*}
paulson@14199
   429
lemma parts_image_priEK:
paulson@14199
   430
     "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
paulson@14199
   431
        evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"
paulson@14199
   432
by auto
paulson@14199
   433
paulson@15481
   434
text{*trivial proof because @{term"priEK C"} never appears even in
paulson@15481
   435
  @{term "parts evs"}. *}
paulson@14199
   436
lemma analz_image_priEK:
paulson@14199
   437
     "evs \<in> set_pur ==>
paulson@14199
   438
          (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   439
          (priEK C \<in> KK | C \<in> bad)"
paulson@14199
   440
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   441
paulson@15481
   442
paulson@14199
   443
subsection{*Public Keys in Certificates are Correct*}
paulson@14199
   444
paulson@14199
   445
lemma Crypt_valid_pubEK [dest!]:
paulson@14199
   446
     "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
paulson@14199
   447
           \<in> parts (knows Spy evs);
paulson@14199
   448
         evs \<in> set_pur |] ==> EKi = pubEK C"
paulson@15481
   449
by (erule rev_mp, erule set_pur.induct, auto)
paulson@14199
   450
paulson@14199
   451
lemma Crypt_valid_pubSK [dest!]:
paulson@14199
   452
     "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
paulson@14199
   453
           \<in> parts (knows Spy evs);
paulson@14199
   454
         evs \<in> set_pur |] ==> SKi = pubSK C"
paulson@15481
   455
by (erule rev_mp, erule set_pur.induct, auto)
paulson@14199
   456
paulson@14199
   457
lemma certificate_valid_pubEK:
paulson@14199
   458
    "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   459
        evs \<in> set_pur |]
paulson@14199
   460
     ==> EKi = pubEK C"
paulson@14199
   461
by (unfold cert_def signCert_def, auto)
paulson@14199
   462
paulson@14199
   463
lemma certificate_valid_pubSK:
paulson@14199
   464
    "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
paulson@14199
   465
        evs \<in> set_pur |] ==> SKi = pubSK C"
paulson@14199
   466
by (unfold cert_def signCert_def, auto)
paulson@14199
   467
paulson@14199
   468
lemma Says_certificate_valid [simp]:
paulson@14199
   469
     "[| Says A B (sign SK {|lid, xid, cc, cm,
paulson@14199
   470
                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
paulson@14199
   471
         evs \<in> set_pur |]
paulson@14199
   472
      ==> EK = pubEK C"
paulson@14199
   473
by (unfold sign_def, auto)
paulson@14199
   474
paulson@14199
   475
lemma Gets_certificate_valid [simp]:
paulson@14199
   476
     "[| Gets A (sign SK {|lid, xid, cc, cm,
paulson@14199
   477
                           cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
paulson@14199
   478
         evs \<in> set_pur |]
paulson@14199
   479
      ==> EK = pubEK C"
paulson@14199
   480
by (frule Gets_imp_Says, auto)
paulson@14199
   481
wenzelm@24123
   482
method_setup valid_certificate_tac = {*
wenzelm@30549
   483
  Args.goal_spec >> (fn quant =>
wenzelm@51798
   484
    fn ctxt => SIMPLE_METHOD'' quant (fn i =>
wenzelm@59499
   485
      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
wenzelm@58963
   486
             assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
wenzelm@42814
   487
*}
paulson@14199
   488
paulson@14199
   489
paulson@14199
   490
subsection{*Proofs on Symmetric Keys*}
paulson@14199
   491
paulson@14199
   492
text{*Nobody can have used non-existent keys!*}
paulson@14199
   493
lemma new_keys_not_used [rule_format,simp]:
paulson@14199
   494
     "evs \<in> set_pur
paulson@14199
   495
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
paulson@14199
   496
          K \<notin> keysFor (parts (knows Spy evs))"
paulson@14199
   497
apply (erule set_pur.induct)
wenzelm@24123
   498
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   499
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   500
apply auto
paulson@14199
   501
apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
paulson@14199
   502
done
paulson@14199
   503
paulson@14199
   504
lemma new_keys_not_analzd:
paulson@14199
   505
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
paulson@14199
   506
      ==> K \<notin> keysFor (analz (knows Spy evs))"
paulson@14199
   507
by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used)
paulson@14199
   508
paulson@14199
   509
lemma Crypt_parts_imp_used:
paulson@14199
   510
     "[|Crypt K X \<in> parts (knows Spy evs);
paulson@14199
   511
        K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
paulson@14199
   512
apply (rule ccontr)
paulson@14199
   513
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
paulson@14199
   514
done
paulson@14199
   515
paulson@14199
   516
lemma Crypt_analz_imp_used:
paulson@14199
   517
     "[|Crypt K X \<in> analz (knows Spy evs);
paulson@14199
   518
        K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
paulson@14199
   519
by (blast intro: Crypt_parts_imp_used)
paulson@14199
   520
paulson@14199
   521
text{*New versions: as above, but generalized to have the KK argument*}
paulson@14199
   522
paulson@14199
   523
lemma gen_new_keys_not_used:
paulson@14199
   524
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
paulson@14199
   525
      ==> Key K \<notin> used evs --> K \<in> symKeys -->
paulson@14199
   526
          K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
paulson@14199
   527
by auto
paulson@14199
   528
paulson@14199
   529
lemma gen_new_keys_not_analzd:
paulson@14199
   530
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
paulson@14199
   531
      ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
paulson@14199
   532
by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used)
paulson@14199
   533
paulson@14199
   534
lemma analz_Key_image_insert_eq:
paulson@14199
   535
     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
paulson@14199
   536
      ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
paulson@14199
   537
          insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
paulson@14199
   538
by (simp add: gen_new_keys_not_analzd)
paulson@14199
   539
paulson@14199
   540
paulson@14199
   541
subsection{*Secrecy of Symmetric Keys*}
paulson@14199
   542
paulson@14199
   543
lemma Key_analz_image_Key_lemma:
paulson@14199
   544
     "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
paulson@14199
   545
      ==>
paulson@14199
   546
      P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
paulson@14199
   547
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   548
paulson@14199
   549
paulson@14199
   550
lemma symKey_compromise:
paulson@15205
   551
     "evs \<in> set_pur \<Longrightarrow>
paulson@14199
   552
      (\<forall>SK KK. SK \<in> symKeys \<longrightarrow>
paulson@15205
   553
        (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow>
paulson@15205
   554
               (Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) =
paulson@15205
   555
               (SK \<in> KK \<or> Key SK \<in> analz (knows Spy evs)))"
paulson@14199
   556
apply (erule set_pur.induct)
paulson@14199
   557
apply (rule_tac [!] allI)+
paulson@14199
   558
apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
paulson@14199
   559
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
wenzelm@24123
   560
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   561
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   562
apply (simp_all
paulson@14199
   563
         del: image_insert image_Un imp_disjL
paulson@14199
   564
         add: analz_image_keys_simps disj_simps
paulson@14199
   565
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   566
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   567
  --{*8 seconds on a 1.6GHz machine*}
paulson@14199
   568
apply spy_analz --{*Fake*}
paulson@14199
   569
apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}
paulson@14199
   570
done
paulson@14199
   571
paulson@14199
   572
paulson@14199
   573
paulson@14199
   574
subsection{*Secrecy of Nonces*}
paulson@14199
   575
paulson@14199
   576
text{*As usual: we express the property as a logical equivalence*}
paulson@14199
   577
lemma Nonce_analz_image_Key_lemma:
paulson@14199
   578
     "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
paulson@14199
   579
      ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
paulson@14199
   580
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   581
paulson@14199
   582
text{*The @{text "(no_asm)"} attribute is essential, since it retains
paulson@14199
   583
  the quantifier and allows the simprule's condition to itself be simplified.*}
paulson@14199
   584
lemma Nonce_compromise [rule_format (no_asm)]:
paulson@14199
   585
     "evs \<in> set_pur ==>
paulson@14199
   586
      (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C))   -->
paulson@14256
   587
              (Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) =
paulson@14199
   588
              (Nonce N \<in> analz (knows Spy evs)))"
paulson@14199
   589
apply (erule set_pur.induct)
paulson@14199
   590
apply (rule_tac [!] allI)+
paulson@14199
   591
apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
paulson@14199
   592
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
wenzelm@24123
   593
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   594
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   595
apply (simp_all
paulson@14199
   596
         del: image_insert image_Un imp_disjL
paulson@14199
   597
         add: analz_image_keys_simps disj_simps symKey_compromise
paulson@14199
   598
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   599
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   600
  --{*8 seconds on a 1.6GHz machine*}
paulson@14199
   601
apply spy_analz --{*Fake*}
paulson@14199
   602
apply (blast elim!: ballE) --{*PReqS*}
paulson@14199
   603
done
paulson@14199
   604
paulson@14199
   605
lemma PANSecret_notin_spies:
paulson@14256
   606
     "[|Nonce (PANSecret k) \<in> analz (knows Spy evs);  evs \<in> set_pur|]
paulson@14256
   607
      ==> 
paulson@14199
   608
       (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
paulson@14199
   609
          Says (Cardholder k) M
paulson@14199
   610
               {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
paulson@14199
   611
                 V|}  \<in>  set evs)"
paulson@14256
   612
apply (erule rev_mp)
paulson@14199
   613
apply (erule set_pur.induct)
paulson@14199
   614
apply (frule_tac [9] AuthReq_msg_in_analz_spies)
wenzelm@24123
   615
apply (valid_certificate_tac [8]) --{*PReqS*}
paulson@14199
   616
apply (simp_all
paulson@14199
   617
         del: image_insert image_Un imp_disjL
paulson@14199
   618
         add: analz_image_keys_simps disj_simps
paulson@14199
   619
              symKey_compromise pushes sign_def Nonce_compromise
paulson@14199
   620
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   621
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   622
  --{*2.5 seconds on a 1.6GHz machine*}
paulson@14199
   623
apply spy_analz
paulson@14199
   624
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
paulson@14199
   625
apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
paulson@14199
   626
                   Gets_imp_knows_Spy [THEN analz.Inj])
paulson@14199
   627
apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*}
paulson@14199
   628
apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
paulson@14199
   629
                   Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*}
paulson@14199
   630
done
paulson@14199
   631
paulson@14199
   632
text{*This theorem is a bit silly, in that many CardSecrets are 0!
paulson@14199
   633
  But then we don't care.  NOT USED*}
paulson@14199
   634
lemma CardSecret_notin_spies:
paulson@14199
   635
     "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"
paulson@14199
   636
by (erule set_pur.induct, auto)
paulson@14199
   637
paulson@15214
   638
paulson@14199
   639
subsection{*Confidentiality of PAN*}
paulson@14199
   640
paulson@14199
   641
lemma analz_image_pan_lemma:
paulson@14199
   642
     "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
paulson@14199
   643
      (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
paulson@14199
   644
by (blast intro: analz_mono [THEN [2] rev_subsetD])
paulson@14199
   645
paulson@14199
   646
text{*The @{text "(no_asm)"} attribute is essential, since it retains
paulson@14199
   647
  the quantifier and allows the simprule's condition to itself be simplified.*}
paulson@14199
   648
lemma analz_image_pan [rule_format (no_asm)]:
paulson@14199
   649
     "evs \<in> set_pur ==>
paulson@14199
   650
       \<forall>KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
paulson@14199
   651
            (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
paulson@14199
   652
            (Pan P \<in> analz (knows Spy evs))"
paulson@14199
   653
apply (erule set_pur.induct)
paulson@14199
   654
apply (rule_tac [!] allI impI)+
paulson@14199
   655
apply (rule_tac [!] analz_image_pan_lemma)+
paulson@14199
   656
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
wenzelm@24123
   657
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   658
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   659
apply (simp_all
paulson@14199
   660
         del: image_insert image_Un imp_disjL
paulson@14199
   661
         add: analz_image_keys_simps
paulson@14199
   662
              symKey_compromise pushes sign_def
paulson@14199
   663
              analz_Key_image_insert_eq notin_image_iff
paulson@14199
   664
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   665
  --{*7 seconds on a 1.6GHz machine*}
paulson@14199
   666
apply spy_analz --{*Fake*}
paulson@14199
   667
apply auto
paulson@14199
   668
done
paulson@14199
   669
paulson@14199
   670
lemma analz_insert_pan:
paulson@14199
   671
     "[| evs \<in> set_pur;  K \<notin> range(\<lambda>C. priEK C) |] ==>
paulson@14199
   672
          (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
paulson@14199
   673
          (Pan P \<in> analz (knows Spy evs))"
paulson@14199
   674
by (simp del: image_insert image_Un
paulson@14199
   675
         add: analz_image_keys_simps analz_image_pan)
paulson@14199
   676
paulson@14199
   677
text{*Confidentiality of the PAN, unsigned case.*}
paulson@15214
   678
theorem pan_confidentiality_unsigned:
paulson@14199
   679
     "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
paulson@14199
   680
         CardSecret k = 0;  evs \<in> set_pur|]
paulson@14199
   681
    ==> \<exists>P M KC1 K X Y.
paulson@14199
   682
     Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
paulson@14199
   683
          \<in> set evs  &
paulson@14199
   684
     P \<in> bad"
paulson@14199
   685
apply (erule rev_mp)
paulson@14199
   686
apply (erule set_pur.induct)
paulson@14199
   687
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
wenzelm@24123
   688
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   689
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   690
apply (simp_all
paulson@14199
   691
         del: image_insert image_Un imp_disjL
paulson@14199
   692
         add: analz_image_keys_simps analz_insert_pan analz_image_pan
paulson@14199
   693
              notin_image_iff
paulson@14199
   694
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   695
  --{*3 seconds on a 1.6GHz machine*}
paulson@14199
   696
apply spy_analz --{*Fake*}
paulson@14199
   697
apply blast --{*PReqUns: unsigned*}
paulson@14199
   698
apply force --{*PReqS: signed*}
paulson@14199
   699
done
paulson@14199
   700
paulson@14199
   701
text{*Confidentiality of the PAN, signed case.*}
paulson@15214
   702
theorem pan_confidentiality_signed:
paulson@15214
   703
 "[|Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
paulson@15214
   704
    CardSecret k \<noteq> 0;  evs \<in> set_pur|]
paulson@15214
   705
  ==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.
paulson@15214
   706
      Says C M {|{|PIDualSign_1, 
paulson@15214
   707
                   EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, 
paulson@15214
   708
       OIDualSign|} \<in> set evs  &  P \<in> bad"
paulson@14199
   709
apply (erule rev_mp)
paulson@14199
   710
apply (erule set_pur.induct)
paulson@14199
   711
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
wenzelm@24123
   712
apply (valid_certificate_tac [8]) --{*PReqS*}
wenzelm@24123
   713
apply (valid_certificate_tac [7]) --{*PReqUns*}
paulson@14199
   714
apply (simp_all
paulson@14199
   715
         del: image_insert image_Un imp_disjL
paulson@14199
   716
         add: analz_image_keys_simps analz_insert_pan analz_image_pan
paulson@14199
   717
              notin_image_iff
paulson@14199
   718
              analz_insert_simps analz_image_priEK)
wenzelm@24123
   719
  --{*3 seconds on a 1.6GHz machine*}
paulson@14199
   720
apply spy_analz --{*Fake*}
paulson@14199
   721
apply force --{*PReqUns: unsigned*}
paulson@14199
   722
apply blast --{*PReqS: signed*}
paulson@14199
   723
done
paulson@14199
   724
paulson@14199
   725
text{*General goal: that C, M and PG agree on those details of the transaction
paulson@14199
   726
     that they are allowed to know about.  PG knows about price and account
paulson@14199
   727
     details.  M knows about the order description and price.  C knows both.*}
paulson@14199
   728
paulson@14199
   729
paulson@14199
   730
subsection{*Proofs Common to Signed and Unsigned Versions*}
paulson@14199
   731
paulson@14199
   732
lemma M_Notes_PG:
paulson@14199
   733
     "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;
paulson@14199
   734
        evs \<in> set_pur|] ==> \<exists>j. P = PG j"
paulson@15481
   735
by (erule rev_mp, erule set_pur.induct, simp_all)
paulson@14199
   736
paulson@14199
   737
text{*If we trust M, then @{term LID_M} determines his choice of P
paulson@14199
   738
      (Payment Gateway)*}
paulson@14199
   739
lemma goodM_gives_correct_PG:
paulson@14199
   740
     "[| MsgPInitRes = 
paulson@14199
   741
            {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
paulson@14199
   742
         Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
paulson@14199
   743
         evs \<in> set_pur; M \<notin> bad |]
paulson@14199
   744
      ==> \<exists>j trans.
paulson@14199
   745
            P = PG j &
paulson@14199
   746
            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"
paulson@14199
   747
apply clarify
paulson@14199
   748
apply (erule rev_mp)
paulson@14199
   749
apply (erule set_pur.induct)
paulson@14199
   750
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   751
apply simp_all
paulson@14199
   752
apply (blast intro: M_Notes_PG)+
paulson@14199
   753
done
paulson@14199
   754
paulson@14199
   755
lemma C_gets_correct_PG:
paulson@14199
   756
     "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,
paulson@14199
   757
                              cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;
paulson@14199
   758
         evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
   759
      ==> \<exists>j trans.
paulson@14199
   760
            P = PG j &
paulson@14199
   761
            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
paulson@14199
   762
            EKj = pubEK P"
paulson@14199
   763
by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)
paulson@14199
   764
paulson@14199
   765
text{*When C receives PInitRes, he learns M's choice of P*}
paulson@14199
   766
lemma C_verifies_PInitRes:
paulson@14199
   767
 "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
wenzelm@32960
   768
           cert P EKj onlyEnc (priSK RCA)|};
paulson@14199
   769
     Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
paulson@14199
   770
     evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
   771
  ==> \<exists>j trans.
paulson@14199
   772
         Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
paulson@14199
   773
         P = PG j &
paulson@14199
   774
         EKj = pubEK P"
paulson@14199
   775
apply clarify
paulson@14199
   776
apply (erule rev_mp)
paulson@14199
   777
apply (erule set_pur.induct)
paulson@14199
   778
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   779
apply simp_all
paulson@14199
   780
apply (blast intro: M_Notes_PG)+
paulson@14199
   781
done
paulson@14199
   782
paulson@14199
   783
text{*Corollary of previous one*}
paulson@14199
   784
lemma Says_C_PInitRes:
paulson@14199
   785
     "[|Says A C (sign (priSK M)
paulson@14199
   786
                      {|Number LID_M, Number XID,
paulson@14199
   787
                        Nonce Chall_C, Nonce Chall_M,
paulson@14199
   788
                        cert P EKj onlyEnc (priSK RCA)|})
paulson@14199
   789
           \<in> set evs;  M \<notin> bad;  evs \<in> set_pur|]
paulson@14199
   790
      ==> \<exists>j trans.
paulson@14199
   791
           Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
paulson@14199
   792
           P = PG j &
paulson@14199
   793
           EKj = pubEK (PG j)"
paulson@14199
   794
apply (frule Says_certificate_valid)
paulson@14199
   795
apply (auto simp add: sign_def)
paulson@14199
   796
apply (blast dest: refl [THEN goodM_gives_correct_PG])
paulson@14199
   797
apply (blast dest: refl [THEN C_verifies_PInitRes])
paulson@14199
   798
done
paulson@14199
   799
paulson@14199
   800
text{*When P receives an AuthReq, he knows that the signed part originated 
paulson@14199
   801
      with M. PIRes also has a signed message from M....*}
paulson@14199
   802
lemma P_verifies_AuthReq:
paulson@14199
   803
     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
paulson@14199
   804
         Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})
paulson@14199
   805
           \<in> parts (knows Spy evs);
paulson@14199
   806
         evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
   807
      ==> \<exists>j trans KM OIData HPIData.
paulson@14199
   808
            Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
paulson@14199
   809
            Gets M {|P_I, OIData, HPIData|} \<in> set evs &
paulson@14199
   810
            Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
paulson@14199
   811
              \<in> set evs"
paulson@14199
   812
apply clarify
paulson@14199
   813
apply (erule rev_mp)
paulson@14199
   814
apply (erule set_pur.induct, simp_all)
paulson@14199
   815
apply (frule_tac [4] M_Notes_PG, auto)
paulson@14199
   816
done
paulson@14199
   817
paulson@14199
   818
text{*When M receives AuthRes, he knows that P signed it, including
paulson@15481
   819
  the identifying tags and the purchase amount, which he can verify.
paulson@14199
   820
  (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
paulson@16474
   821
   send the same message to M.)  The conclusion is weak: M is existentially
paulson@16474
   822
  quantified! That is because Authorization Response does not refer to M, while
paulson@16474
   823
  the digital envelope weakens the link between @{term MsgAuthRes} and
paulson@16474
   824
  @{term"priSK M"}.  Changing the precondition to refer to 
paulson@16474
   825
  @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
paulson@16474
   826
  otherwise the Spy could create that message.*}
paulson@15214
   827
theorem M_verifies_AuthRes:
paulson@16474
   828
  "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 
paulson@16474
   829
                     Hash authCode|};
paulson@14199
   830
      Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
paulson@16474
   831
      PG j \<notin> bad;  evs \<in> set_pur|]
paulson@16474
   832
   ==> \<exists>M KM KP HOIData HOD P_I.
wenzelm@32960
   833
        Gets (PG j)
wenzelm@32960
   834
           (EncB (priSK M) KM (pubEK (PG j))
wenzelm@32960
   835
                    {|Number LID_M, Number XID, HOIData, HOD|}
wenzelm@32960
   836
                    P_I) \<in> set evs &
wenzelm@32960
   837
        Says (PG j) M
wenzelm@32960
   838
             (EncB (priSK (PG j)) KP (pubEK M)
wenzelm@32960
   839
              {|Number LID_M, Number XID, Number PurchAmt|}
wenzelm@32960
   840
              authCode) \<in> set evs"
paulson@14199
   841
apply clarify
paulson@14199
   842
apply (erule rev_mp)
paulson@14199
   843
apply (erule set_pur.induct)
paulson@14199
   844
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   845
apply simp_all
paulson@14199
   846
apply blast+
paulson@14199
   847
done
paulson@14199
   848
paulson@14199
   849
paulson@14199
   850
subsection{*Proofs for Unsigned Purchases*}
paulson@14199
   851
paulson@14199
   852
text{*What we can derive from the ASSUMPTION that C issued a purchase request.
paulson@14199
   853
   In the unsigned case, we must trust "C": there's no authentication.*}
paulson@14199
   854
lemma C_determines_EKj:
paulson@14199
   855
     "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
paulson@14199
   856
                    OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;
paulson@14199
   857
         PIHead = {|Number LID_M, Trans_details|};
paulson@14199
   858
         evs \<in> set_pur;  C = Cardholder k;  M \<notin> bad|]
paulson@14199
   859
  ==> \<exists>trans j.
paulson@14199
   860
               Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
paulson@14199
   861
               EKj = pubEK (PG j)"
paulson@14199
   862
apply clarify
paulson@14199
   863
apply (erule rev_mp)
paulson@14199
   864
apply (erule set_pur.induct, simp_all)
wenzelm@24123
   865
apply (valid_certificate_tac [2]) --{*PReqUns*}
paulson@14199
   866
apply auto
paulson@14199
   867
apply (blast dest: Gets_imp_Says Says_C_PInitRes)
paulson@14199
   868
done
paulson@14199
   869
paulson@14199
   870
paulson@14199
   871
text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}
paulson@14199
   872
lemma unique_LID_M:
paulson@14199
   873
     "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;
paulson@14199
   874
        Notes C {|Number LID_M, Agent M, Agent C, Number OD,
paulson@14199
   875
             Number PA|} \<in> set evs;
paulson@14199
   876
        evs \<in> set_pur|]
paulson@14199
   877
      ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
paulson@14199
   878
apply (erule rev_mp)
paulson@14199
   879
apply (erule rev_mp)
paulson@14199
   880
apply (erule set_pur.induct, simp_all)
paulson@14199
   881
apply (force dest!: Notes_imp_parts_subset_used)
paulson@14199
   882
done
paulson@14199
   883
paulson@14199
   884
text{*Unicity of @{term LID_M}, for two Merchant Notes events*}
paulson@14199
   885
lemma unique_LID_M2:
paulson@14199
   886
     "[|Notes M {|Number LID_M, Trans|} \<in> set evs;
paulson@14199
   887
        Notes M {|Number LID_M, Trans'|} \<in> set evs;
paulson@14199
   888
        evs \<in> set_pur|] ==> Trans' = Trans"
paulson@14199
   889
apply (erule rev_mp)
paulson@14199
   890
apply (erule rev_mp)
paulson@14199
   891
apply (erule set_pur.induct, simp_all)
paulson@14199
   892
apply (force dest!: Notes_imp_parts_subset_used)
paulson@14199
   893
done
paulson@14199
   894
paulson@14199
   895
text{*Lemma needed below: for the case that
paulson@14199
   896
  if PRes is present, then @{term LID_M} has been used.*}
paulson@14199
   897
lemma signed_imp_used:
paulson@14199
   898
     "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);
paulson@14199
   899
         M \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
paulson@14199
   900
apply (erule rev_mp)
paulson@14199
   901
apply (erule set_pur.induct)
paulson@14199
   902
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   903
apply simp_all
paulson@14199
   904
apply safe
paulson@14199
   905
apply blast+
paulson@14199
   906
done
paulson@14199
   907
paulson@14199
   908
text{*Similar, with nested Hash*}
paulson@14199
   909
lemma signed_Hash_imp_used:
paulson@14199
   910
     "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
paulson@14199
   911
         C \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
paulson@14199
   912
apply (erule rev_mp)
paulson@14199
   913
apply (erule set_pur.induct)
paulson@14199
   914
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   915
apply simp_all
paulson@14199
   916
apply safe
paulson@14199
   917
apply blast+
paulson@14199
   918
done
paulson@14199
   919
paulson@14199
   920
text{*Lemma needed below: for the case that
paulson@14199
   921
  if PRes is present, then @{text LID_M} has been used.*}
paulson@14199
   922
lemma PRes_imp_LID_used:
paulson@14199
   923
     "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);
paulson@14199
   924
         M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"
paulson@14199
   925
by (drule signed_imp_used, auto)
paulson@14199
   926
paulson@14199
   927
text{*When C receives PRes, he knows that M and P agreed to the purchase details.
paulson@14199
   928
  He also knows that P is the same PG as before*}
paulson@14199
   929
lemma C_verifies_PRes_lemma:
paulson@14199
   930
     "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);
paulson@14199
   931
         Notes C {|Number LID_M, Trans |} \<in> set evs;
paulson@14199
   932
         Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
paulson@14199
   933
         MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
paulson@14199
   934
                Hash (Number PurchAmt)|};
paulson@14199
   935
         evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
   936
  ==> \<exists>j KP.
paulson@14199
   937
        Notes M {|Number LID_M, Agent (PG j), Trans |}
paulson@14199
   938
          \<in> set evs &
paulson@14199
   939
        Gets M (EncB (priSK (PG j)) KP (pubEK M)
paulson@14199
   940
                {|Number LID_M, Number XID, Number PurchAmt|}
paulson@14199
   941
                authCode)
paulson@14199
   942
          \<in> set evs &
paulson@14199
   943
        Says M C (sign (priSK M) MsgPRes) \<in> set evs"
paulson@14199
   944
apply clarify
paulson@14199
   945
apply (erule rev_mp)
paulson@14199
   946
apply (erule rev_mp)
paulson@14199
   947
apply (erule set_pur.induct)
paulson@14199
   948
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   949
apply simp_all
paulson@14199
   950
apply blast
paulson@14199
   951
apply blast
paulson@14199
   952
apply (blast dest: PRes_imp_LID_used)
paulson@14199
   953
apply (frule M_Notes_PG, auto)
paulson@14199
   954
apply (blast dest: unique_LID_M)
paulson@14199
   955
done
paulson@14199
   956
paulson@15214
   957
text{*When the Cardholder receives Purchase Response from an uncompromised
paulson@15214
   958
Merchant, he knows that M sent it. He also knows that M received a message signed
paulson@15214
   959
by a Payment Gateway chosen by M to authorize the purchase.*}
paulson@15214
   960
theorem C_verifies_PRes:
paulson@14199
   961
     "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
paulson@14199
   962
                     Hash (Number PurchAmt)|};
paulson@14199
   963
         Gets C (sign (priSK M) MsgPRes) \<in> set evs;
paulson@14199
   964
         Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
paulson@14199
   965
                   Number PurchAmt|} \<in> set evs;
paulson@14199
   966
         evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
   967
  ==> \<exists>P KP trans.
paulson@14199
   968
        Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
paulson@14199
   969
        Gets M (EncB (priSK P) KP (pubEK M)
paulson@14199
   970
                {|Number LID_M, Number XID, Number PurchAmt|}
paulson@15214
   971
                authCode)  \<in>  set evs &
paulson@14199
   972
        Says M C (sign (priSK M) MsgPRes) \<in> set evs"
paulson@14199
   973
apply (rule C_verifies_PRes_lemma [THEN exE])
paulson@14199
   974
apply (auto simp add: sign_def)
paulson@14199
   975
done
paulson@14199
   976
paulson@14199
   977
subsection{*Proofs for Signed Purchases*}
paulson@14199
   978
paulson@14199
   979
text{*Some Useful Lemmas: the cardholder knows what he is doing*}
paulson@14199
   980
paulson@14199
   981
lemma Crypt_imp_Says_Cardholder:
paulson@14199
   982
     "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
paulson@14199
   983
           \<in> parts (knows Spy evs);
paulson@14199
   984
         PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
paulson@14199
   985
         Key K \<notin> analz (knows Spy evs);
paulson@14199
   986
         evs \<in> set_pur|]
paulson@14199
   987
  ==> \<exists>M shash EK HPIData.
paulson@14199
   988
       Says (Cardholder k) M {|{|shash,
paulson@14199
   989
          Crypt K
paulson@14199
   990
            {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
paulson@14199
   991
           Crypt EK {|Key K, PANData|}|},
paulson@14199
   992
          OIData, HPIData|} \<in> set evs"
paulson@14199
   993
apply (erule rev_mp)
paulson@14199
   994
apply (erule rev_mp)
paulson@14199
   995
apply (erule rev_mp)
paulson@14199
   996
apply (erule set_pur.induct, analz_mono_contra)
paulson@14199
   997
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
   998
apply simp_all
paulson@14199
   999
apply auto
paulson@14199
  1000
done
paulson@14199
  1001
paulson@14199
  1002
lemma Says_PReqS_imp_trans_details_C:
paulson@14199
  1003
     "[| MsgPReqS = {|{|shash,
paulson@14199
  1004
                 Crypt K
paulson@14199
  1005
                  {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
paulson@14199
  1006
            cryptek|}, data|};
paulson@14199
  1007
         Says (Cardholder k) M MsgPReqS \<in> set evs;
paulson@14199
  1008
         evs \<in> set_pur |]
paulson@14199
  1009
   ==> \<exists>trans.
paulson@14199
  1010
           Notes (Cardholder k) 
paulson@14199
  1011
                 {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
paulson@14199
  1012
            \<in> set evs"
paulson@14199
  1013
apply (erule rev_mp)
paulson@14199
  1014
apply (erule rev_mp)
paulson@14199
  1015
apply (erule set_pur.induct)
paulson@14199
  1016
apply (simp_all (no_asm_simp))
paulson@14199
  1017
apply auto
paulson@14199
  1018
done
paulson@14199
  1019
paulson@14199
  1020
text{*Can't happen: only Merchants create this type of Note*}
paulson@14199
  1021
lemma Notes_Cardholder_self_False:
paulson@14199
  1022
     "[|Notes (Cardholder k)
paulson@14199
  1023
          {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;
paulson@14199
  1024
        evs \<in> set_pur|] ==> False"
paulson@15481
  1025
by (erule rev_mp, erule set_pur.induct, auto)
paulson@14199
  1026
paulson@14199
  1027
text{*When M sees a dual signature, he knows that it originated with C.
paulson@14199
  1028
  Using XID he knows it was intended for him.
paulson@14199
  1029
  This guarantee isn't useful to P, who never gets OIData.*}
paulson@15214
  1030
theorem M_verifies_Signed_PReq:
paulson@15214
  1031
 "[| MsgDualSign = {|HPIData, Hash OIData|};
paulson@15214
  1032
     OIData = {|Number LID_M, etc|};
paulson@15214
  1033
     Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
paulson@15214
  1034
     Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
paulson@15214
  1035
     M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
paulson@15214
  1036
  ==> \<exists>PIData PICrypt.
wenzelm@32960
  1037
        HPIData = Hash PIData &
wenzelm@32960
  1038
        Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
wenzelm@32960
  1039
          \<in> set evs"
paulson@14199
  1040
apply clarify
paulson@14199
  1041
apply (erule rev_mp)
paulson@14199
  1042
apply (erule rev_mp)
paulson@14199
  1043
apply (erule set_pur.induct)
paulson@14199
  1044
apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
paulson@14199
  1045
apply simp_all
paulson@14199
  1046
apply blast
paulson@32404
  1047
apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used)
paulson@32404
  1048
apply (metis unique_LID_M)
paulson@14199
  1049
apply (blast dest!: Notes_Cardholder_self_False)
paulson@14199
  1050
done
paulson@14199
  1051
paulson@14199
  1052
text{*When P sees a dual signature, he knows that it originated with C.
paulson@14199
  1053
  and was intended for M. This guarantee isn't useful to M, who never gets
paulson@14199
  1054
  PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
paulson@14199
  1055
  assuming @{term "M \<notin> bad"}.*}
paulson@15214
  1056
theorem P_verifies_Signed_PReq:
paulson@14199
  1057
     "[| MsgDualSign = {|Hash PIData, HOIData|};
paulson@14199
  1058
         PIData = {|PIHead, PANData|};
paulson@14199
  1059
         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
paulson@14199
  1060
                    TransStain|};
paulson@14199
  1061
         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
paulson@14199
  1062
         evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
paulson@14199
  1063
    ==> \<exists>OIData OrderDesc K j trans.
paulson@14199
  1064
          HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
paulson@14199
  1065
          HOIData = Hash OIData &
paulson@14199
  1066
          Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
paulson@14199
  1067
          Says C M {|{|sign (priSK C) MsgDualSign,
paulson@14199
  1068
                     EXcrypt K (pubEK (PG j))
paulson@14199
  1069
                                {|PIHead, Hash OIData|} PANData|},
paulson@14199
  1070
                     OIData, Hash PIData|}
paulson@14199
  1071
            \<in> set evs"
paulson@14199
  1072
apply clarify
paulson@14199
  1073
apply (erule rev_mp)
paulson@14199
  1074
apply (erule set_pur.induct, simp_all)
paulson@14199
  1075
apply (auto dest!: C_gets_correct_PG)
paulson@14199
  1076
done
paulson@14199
  1077
paulson@14199
  1078
lemma C_determines_EKj_signed:
paulson@14199
  1079
     "[| Says C M {|{|sign (priSK C) text,
paulson@14199
  1080
                      EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;
paulson@14199
  1081
         PIHead = {|Number LID_M, Number XID, W|};
paulson@14199
  1082
         C = Cardholder k;  evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
  1083
  ==> \<exists> trans j.
paulson@14199
  1084
         Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
paulson@14199
  1085
         EKj = pubEK (PG j)"
paulson@14199
  1086
apply clarify
paulson@14199
  1087
apply (erule rev_mp)
paulson@14199
  1088
apply (erule set_pur.induct, simp_all, auto)
paulson@14199
  1089
apply (blast dest: C_gets_correct_PG)
paulson@14199
  1090
done
paulson@14199
  1091
paulson@14199
  1092
lemma M_Says_AuthReq:
paulson@14199
  1093
     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
paulson@14199
  1094
         sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);
paulson@14199
  1095
         evs \<in> set_pur;  M \<notin> bad|]
paulson@14199
  1096
   ==> \<exists>j trans KM.
paulson@14199
  1097
           Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
paulson@14199
  1098
             Says M (PG j)
paulson@14199
  1099
               (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
paulson@14199
  1100
              \<in> set evs"
paulson@14199
  1101
apply (rule refl [THEN P_verifies_AuthReq, THEN exE])
paulson@14199
  1102
apply (auto simp add: sign_def)
paulson@14199
  1103
done
paulson@14199
  1104
paulson@14199
  1105
text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information.
paulson@14199
  1106
  Even here we cannot be certain about what C sent to M, since a bad
paulson@14199
  1107
  PG could have replaced the two key fields.  (NOT USED)*}
paulson@14199
  1108
lemma Signed_PReq_imp_Says_Cardholder:
paulson@14199
  1109
     "[| MsgDualSign = {|Hash PIData, Hash OIData|};
paulson@14199
  1110
         OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};
paulson@14199
  1111
         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
paulson@14199
  1112
                    TransStain|};
paulson@14199
  1113
         PIData = {|PIHead, PANData|};
paulson@14199
  1114
         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
paulson@14199
  1115
         M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
paulson@14199
  1116
      ==> \<exists>KC EKj.
paulson@14199
  1117
            Says C M {|{|sign (priSK C) MsgDualSign,
paulson@14199
  1118
                       EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
paulson@14199
  1119
                       OIData, Hash PIData|}
paulson@14199
  1120
              \<in> set evs"
paulson@14199
  1121
apply clarify
thomas@57492
  1122
apply hypsubst_thin
paulson@14199
  1123
apply (erule rev_mp)
paulson@14199
  1124
apply (erule rev_mp)
paulson@14199
  1125
apply (erule set_pur.induct, simp_all, auto)
paulson@14199
  1126
done
paulson@14199
  1127
paulson@14199
  1128
text{*When P receives an AuthReq and a dual signature, he knows that C and M
paulson@14199
  1129
  agree on the essential details.  PurchAmt however is never sent by M to
paulson@14199
  1130
  P; instead C and M both send 
paulson@14199
  1131
     @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}
paulson@14199
  1132
  and P compares the two copies of HOD.
paulson@14199
  1133
paulson@14199
  1134
  Agreement can't be proved for some things, including the symmetric keys
paulson@14199
  1135
  used in the digital envelopes.  On the other hand, M knows the true identity
paulson@14199
  1136
  of PG (namely j'), and sends AReq there; he can't, however, check that
paulson@14199
  1137
  the EXcrypt involves the correct PG's key.
paulson@14199
  1138
*}
paulson@15214
  1139
theorem P_sees_CM_agreement:
paulson@14199
  1140
     "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
paulson@14199
  1141
         KC \<in> symKeys;
paulson@14199
  1142
         Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
paulson@14199
  1143
           \<in> set evs;
paulson@14199
  1144
         C = Cardholder k;
paulson@14199
  1145
         PI_sign = sign (priSK C) {|Hash PIData, HOIData|};
paulson@14199
  1146
         P_I = {|PI_sign,
paulson@14199
  1147
                 EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};
paulson@14199
  1148
         PANData = {|Pan (pan C), Nonce (PANSecret k)|};
paulson@14199
  1149
         PIData = {|PIHead, PANData|};
paulson@14199
  1150
         PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
paulson@14199
  1151
                    TransStain|};
paulson@14199
  1152
         evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
paulson@14199
  1153
  ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.
paulson@14199
  1154
           HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
paulson@14199
  1155
           HOIData = Hash OIData &
paulson@14199
  1156
           Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &
paulson@14199
  1157
           Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &
paulson@14199
  1158
           Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
paulson@14199
  1159
                           AuthReqData P_I'')  \<in>  set evs &
paulson@14199
  1160
           P_I' = {|PI_sign,
paulson@14199
  1161
             EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &
paulson@14199
  1162
           P_I'' = {|PI_sign,
paulson@14199
  1163
             EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"
paulson@14199
  1164
apply clarify
paulson@14199
  1165
apply (rule exE)
paulson@14199
  1166
apply (rule P_verifies_Signed_PReq [OF refl refl refl])
paulson@14199
  1167
apply (simp (no_asm_use) add: sign_def EncB_def, blast)
paulson@14199
  1168
apply (assumption+, clarify, simp)
paulson@14199
  1169
apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
paulson@14199
  1170
apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2)
paulson@14199
  1171
done
paulson@14199
  1172
paulson@14199
  1173
end