? V believes Kj-is-decrypting-key-for-{X}K )

A6: Every party believes that if a verifier V has a signed message {X}K?1 , a key KQ, and a message X, and V believes that the key KQ is referred to the party Q, then V believes that Q has sent the message X.P believes ( V has {X}K?1

KQ

? V has (KQ, X) ? V believes (?? Q) )

? V believes (Q says X)

Protocol-specific Assumptions

No Disclosure of Private Information to Verifier

A7: Every party does not believe that a verifier V has payment information, the private keys of other parties, and order descriptions.

¬P believes V has PI, where V is not the same party as P G.

¬P believes V has K?1, where V is not the same party as P .

¬P believes V has OD

Payment Information

A8: The client and the merchant believe that they have order information, or- der descriptions and price, and all parties believe that they are internal parties.

Q believes Q has (OI, OD, P rice),

R believes R’-is-internal-party

where Q stands for the client and the merchant, and R and Rj stand for

the client, the issuer, the merchant, and the payment gateway.

Sending and Receiving Messages

A9: Every party believes that {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex has

been sent by the client and received by the issuer.

P believes C says {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex ,

P believes I sees {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex

where P stands for the client, the issuer, the merchant, and the payment gateway.

Shared Secrets

A10: Both client and issuer believe that they possess the shared key Kex, and both of them believe that Kex is shared between them.

Q believes Q has K , Q believes (C ?K?ex I)

where Q stands for the client or the issuer.

Payment Authorizations

A11: Every party believes that she can prove to a verifier V that if the client has sent the message containing the issuer’s identity and the date of transac- tion, then the client has authorization on transaction request to the issuer.

P believes P Can prove C says (IDI, Date)

C authorized transaction-request(C, I, Date) to V

Outline of the Proof

In order to prove the goals of the analysis outlined in section 7.5.1, we transform all protocol messages into the form of our logic. For example, the following protocol step:

C?M : {X}K can be transformed into M sees {X}K

We then construct the receiver’s belief, followed by the possession, of the received message by using the axioms C1 and H1, respectively. Then we can derive the following statement:

M believes M has {X}K

If K is the C’s private key, we can apply the axiom P3. If K is the symmetric key shared between C and M , we apply the axiom P3′ instead. For the latter case, if the condition in the axiom P3′ that X cannot be generated by M holds, we can derive the following statement:

M believes M Can prove (C says (X, IDM )) to V

If X contains P rice and Date, by applying the axiom K and the assump- tion A12, we can achieve the goal G1:

M believes M Can prove (

C authorized payment-order(C, M, P rice, Date)) to V

Analyzing the Proposed SET Framework on Accountability

Guideline of the Proof

We show how to read the proof statement in order to help the reader under- stand the proof. For example,

1, C1: C believes C sees {X}K (2)

This means that this is the statement (2) which is derived from applying the statement (1) with the axiom C1.

Proving the Goal G1

G1: I believes I Can prove (

C authorized transaction-request(C, I, Date) to V

Consider Step 2 of the proposed SET framework,

C?I: {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex

It can be transformed into:

I sees {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex

C) (7)

5, 6, 7, H6, M: I believes I has (IDI, h(P ReqGen)) (8)

A1, A2, P2, M: I believes I Can prove (?K?C

5, 6, 8, 9, P3, M:C) to V (9)

I believes I Can prove ( C says (IDI, h(P ReqGen)) ) to V (10)

10, P6, M:

I believes I Can prove (C says h(P ReqGen)) to V (11) 3, 8, H2, M: I believes I has (P ReqGen, h(P ReqGen)) (12) 12, A4, P2, M:

I believes I Can prove (

h(P ReqGen)-is-fingerprint-of-P ReqGen ) to V (13) 11, 13, P4, M: I believes I Can prove (C says PReqGen) to V (14) 14, P6, M: I believes I Can prove (C says Date) to V (15) 10, 15, P6, M:

I believes I Can prove (C says (IDI, Date)) to V (16)

16, A11, K:

I believes I Can prove (

C authorized transaction-request(C, I, Date)) to V (17)

The proof of the goal G1 is successful.

Proving the Goal G2

G2: C believes C Can prove (

C authorized transaction-request(C, I, Date)) to I

Consider Step 2 of the proposed SET framework,

C?I: {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex

It can be transformed into:

C says {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex

Details of the Proof

C says {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex (1)

1, C2, M:

C believes C says {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex (2)

2, SA2, M:

C believes C has {P ReqGen, {IDI, h(P ReqGen)}K?1 }Kex (3)

3, A10, H4, M:

C believes C has (P ReqGen, {IDI, h(P ReqGen)}K?1 ) (4)

4, H2, M: C believes C has {IDI, h(P ReqGen)}K?1

(5)

A1, H2, M: C believes C has KC (6)

A1, A2, K: C believes C believes (?K?C

C)(7)

5, 6, 7, H6, M: C believes C has (IDI, h(P ReqGen)) (8)

A1, A2, P2, M: C believes C Can prove (?K?C