Formal and Automatic Security Analysis of the Micropayment Scheme

Along this Section we provide a formal analysis of our micropayment scheme des-cribed in §3.4 to analyze the achievement of the required security properties as stated in the security model described in §3.2.3.

7.1.1 Unforgeability

Theorem 7.1.1 Taking into account the underlying RSA factorization problem from the partially blind signature and the one-wayness and collision resistance of a cryp-tographic hash function, the micropayment scheme explained in §3.4 is unforgeable w.r.t. the Definition 3.2.4.

Proof.As stated by the unforgeabilityDefinition 3.2.4, there are some forge in-stance that should be verified in order to prove that the micropayment scheme meets the unforgeability requirement. Summarizing, to forge the micropayment scheme, an adversary has either to forge the partially blind signature or to find a collision in the cryptographic hash function.

Concerning the unforgeability game 0, as described in theDefinition 3.2.4, sev-eral forge scenarios could meet the condition that_A0tries to spend a microcoupon not really belonging _C(mc_6∈C). The first considered case may happen when _A0 tries to forge the micropayment spending a microcoupon^¡mc₌^£_ω(i+1)C,ωiC¤¢

be-yond the limits set by_C. It means that_A0uses a microcoupon whose index is either i>2N ori≤0. The coin identifier(ω0C,ω0M)is bound to the common informa-tion^¡_Γ=^¡2N,v,τexp,4τop,4τr

¢¢during theWithdrawalprotocol by using the partially blind signature scheme. The common information contains the number of microcoupons held by_C (i.e. 2N hash identifiers, thusN microcouponsmc). So, either the merchant or the bank can verify whether the received index and the cor-responding microcoupon are within the limits of_C. It is clear that if the index is i>2N ori≤0, both merchant and bank does not accept the microcoupon. Related to the former case,_A0could try to use a microcoupon not belonging_Cbut providing an index within the limits specified by the common information (i≤2N ori>0). In that case, applying the hash chain properties, the verifier can easily determine that the provided index does not belong the provided microcoupon. As before, the verifier does not accept the microcoupon because it does not belong_C(mc_6∈C).

Another forge scenario may take place if_A0has found and used a microcoupon really not belonging_Cwhile the verifier does not detect it. It would mean that_A0 has actually found a collision in the hash function. However, this case has negligible probability to happen as we use a secure cryptographic one-way hash function with resistance to collisions (inK).

The third case consists on an adversary_A0trying to modify some of the elements described by the common information. Recall that the common information field contains the number of microcoupons, their value and a list of time marks. To modify any content within the common information,_A0 must modify_C, in particular the partially blind signature (CP BS). However, _{CP BS} cannot be modified without either merchant of bank detecting it due to the fact that the partially blind signature is unforgeable (inK) (refer to §3.3 from [55]).

The last unforgeability case is defined as the self-withdrawn_C. Since the auto-generated_Chas not been created by a recognized bank (i.e.,_Chas not been signed by a private key whose owner should be a recognized bank and certified by a trusted CA), a verifier does not accept_Cas he only accepts genuine coins correctly issued from a recognized bank.

Therefore, w.r.t. the game 0, the micropayment scheme is unforgeable under the collision resistance of the cryptographic one-way hash function and the unforge-ability of the partially blind signature scheme. Besides, an adversary cannot create self-withdrawn coins as they will not be accepted by either merchant or bank since they have been withdrawn by an unrecognized bank.

Regarding to the unforgeability game 1,_A1 may try to deposit more coupons that the number he had received from honest customers. However,_A1cannot do it as it would mean that_A1has successfully forged either the partially blind signature or a microcoupon and we have proved above that it is unfeasible for an adversary with non-negligible probability (inK).

In a formal way and following the Definition 3.2.4 together with the above proofs, if an adversary_A(A0,A1)can forge a coin_C, it means that the adversary_A has success in one of the forge instances: forge the partially blind signature or find a collision of a cryptographic one-way hash function. However, both instances have negligible probability to happen (inK). On one hand,_A has to factorize the modulus used by the partially blind signature scheme. As long as the partially blind signature scheme is based on the discrete logarithm problem, it is assumed that it is unfeasible for_A to find a solution to this problem (find the modulus factorization) with non-negligible probability (inK). On the other hand,_A cannot find with non-negligible probability (inK) a collision, since it is not feasible under the fact that we have used a secure one-way collision resistant hash function. As a result, neither_A(A0,A1) can win any forge game with non-negligible probability (inK).

7.1.2 Anonymity of Customers

Lemma 7.1.2 The micropayment scheme described in §3.4 protects the anonymity of customers w.r.t. the Definition 3.2.5 because the coin_Cdoes not contain any data about the customer’s identity and besides, during a call to theSpendprotocol, no information is exchanged that could be used to infer the customer’s identity.

Proof.During theWithdrawalprotocol,_C has to authenticate herself in order to be allowed by_B to withdraw money and issue the coin_C. Indeed, in the first step of theWithdrawal protocol,_C sends _B the common information signed (SC(Γ,α))along with her digital certificate from a trusted CA(C er t_C). This way,_B authenticated_C while she also states that she wants to withdraw a coin with a value equivalent tov_C=(Γ.N·Γ.v). Despite the fact theWithdrawalprotocol is not an

anonymous process by construction, the final result (i.e. the coin_C) is anonymous.

The withdrawn_Cconveys two types of data: the chained list of microcoupons(C_ω) and the partially blind signature(C_{P BS}). Neither field have any information about the identity of _C even if during the Withdrawalprotocol _C provides _B with her real identity to obtain the _{CP BS} element. Therefore, during the process of Withdrawal,_Bissues coins without any customer identification.

Concerning the anonymity game 0 from theDefinition 3.2.5, an adversary _A acting as a malicious_M, cannot successfully identify the customer who runs the Spendprotocol, examining data in _VA^Spend. _C sends a single or a set of micro-coupons to_A during the exchange of theSpendprotocol. As stated before, no information about her identity is carried by microcoupons since they are only hash identifiers derived from a random seed element, applying the hash chain properties.

Besides,_{CP BS} neither contains information about the identity of_C.

As a result,_A cannot identify_C while she is spending microcoupons by using theSpendprotocol.

7.1.3 Unlinkability

Theorem 7.1.3 Under the unlinkability of the partially blind signature scheme, the micropayment scheme described in §3.4 is 2N-unlinkable w.r.t. the Definition 3.2.6.

Proof. Microcoupons from different coins (i.e. _{ωiC ∈Cω} and_ω⁰_{iC ∈C}⁰_ω,_∀i) cannot be linked. It is due to the fact that chain identifiers from two different coins are generated iteratively from a unrelated and random seed identifier(ω2NC). In-deed, by hash chain properties, it can be proved that from two different and ran-dom seed identifiers, the process outputs two different and unrelated coin identifiers

³ω0C 6=ω⁰_0C´

. So, it means that even two microcoupons from the same coin can be linked by hash chain properties (i.e. _ωiC,_{ω(i+j)C ∈C}can be linked to the same_C applying_H^i+j−1¡_ω(i+j)C^¢_=ωiC), two microcoupons from different coins cannot be linked.

In case of unlinkability game 0, if the adversary_A0 can be able to link two Spend(_A0has two views_VA^Spend0

0 and_VA^Spend1

0 ) executions to the same customer, it means that_A0has broken the unlinkability of the underlying partially blind signa-ture. However, it only happens with non-negligible probability thanks to the use of a secure partially blind signature (refer to §3.3 from [55] to show the proof).

In case of unlinkability game 1, we should prove that an adversary_A1cannot link _C (in particular_{CP BS}) to theWithdrawalprotocol in which_C had been withdrawn. As defined by the game 1,_A1 has obtained a view_VB^Withdrawal from an execution of aWithdrawalprotocol by a corrupted_B. This view contains the messages exchanged between_C and_Bwhen they had been engaged in a previous Withdrawalprotocol, so it also contains the digital certificate of_C. However,

due to the way_C completes locally the generation of_{CP BS} (remember that_C un-blinds the last message received by_Bduring theWithdrawalprotocol, obtaining actually the final_{CP BS}),_Bneither knows the final coin identifier(ω0C,ω0M). So, the latter element is not present in the provided view. Consider that_A1executes a Spendprotocol with a customer that he does not know certainly whether she is the same customer as who had executed theWithdrawalprotocol. Then, if_A1can link_{CP BS} with the correspondingWithdrawalrun in which it had been with-drawn,_A1has success in breaking the unlinkability of the underlying partially blind signature scheme. However, it only happens with non-negligible probability (inK) under the assumption that the partially blind signature is unlinkable, similarly as in the game 0 (refer also to §3.3 from [55]).

As a result, no p.p.t. adversary_A(A0,A1)can win any unlinkability game with non-negligible advantage over random guess (inK). Thus, the micropayment scheme is2N-unlinkable.

7.1.4 Untraceability

Theorem 7.1.4 Under both the anonymity of customers and the unlinkability proofs, the micropayment scheme presented in §3.4 meets the untraceability property as defined by the Definition 3.2.7.

Proof. Considering the proofs of both Lemma 7.1.2 and the Theorem 7.1.3, a p.p.t. adversary_A0acting as a malicious merchant (even colluding with a corrupted B) can neither discover the identity of the customer who runs the Spend proto-col nor can link twoSpendtransactions made by using different coins(C1and_C2) with non-negligible advantage over random guess (inK). Moreover, although using microcoupons from the same coin_C1,_A0cannot know the real identity of_C even microcoupon can be linked easily by hash chain properties.

It is also worthy to remark that although _C is merchant-specific, _B does not know the merchant a customer wishes to use the coin with. So, if the bank issuesn coins for a particular customer,_Bcannot assure whether it has issuedncoins forn different merchants or for the same merchant.

As a consequence, we can remark the following:

Remark7.1.1 Customers are protected from profiling made by malicious parties, in particular malicious merchants.

7.1.5 Microcoupon Reuse Avoidance

Theorem 7.1.5 Under the unforgeability of the partially blind signature scheme (thus, the unforgeability of the micropayment scheme itself) and the one-wayness and

collision resistance of the cryptographic hash function, the micropayment scheme described in §3.4 detects and avoids the microcoupon reuse w.r.t. the Definition 3.2.8.

Proof.Although coins are self-contained, in a sense that any party can verify_C because it carries all the required information for its verification, both_Mand_Bhave to maintain their own database to store partially and still valid coins together with the microcoupons already used belonging that coins. So, every row of that databases encloses a tuple(C,ωiC,i)with the aim to control the last received microcoupon (ωiC)along with its position within the microcoupon chain(i)and the corresponding coin(C). With checking this tuple of elements, both_Band_M are able to determine whether a single microcoupon had already been used before.

As exposed in §3.2.8, three types of microcoupon reuse instances can be de-fined based on who tries to cheat. First, during the microcoupon reuse game 0, an adversary_A0can try to execute theSpendprotocol using an already used micro-coupon with the honest merchant. Secondly, during the micromicro-coupon reuse game 1, an adversary_A1can try to run theDepositprotocol with_Bsending an already de-posited microcoupon. Finally, and similarly to the above case, an adversary_A2can try to perform theRefundprotocol trying to cheat_B using a microupon already used, deposited or refunded before. In every case, the verifier can check whether the coupon has already spent, deposited or refunded earlier checking whether the provided microcoupon is either in_M’s database or in_B’s database. Based on the proof of the unforgeability Theorem 7.1.1, no adversary_A(A0,A1,A2)has success on playing any microcoupon reuse game without it being detected and avoided by the corresponding verifier (for instance, either_Bor_M) with non-negligible prob-ability (inK). Note that, when_C tries to cheat_M, he cannot know her identity so he only is able to deny the currentSpendtransaction. Instead, as both_C and_M has to be authenticated as to access their bank accounts,_B can know immediately who are the cheaters trying to reuse a microcoupon already deposited or refunded, so_Bcan undertake measures against them. Finally, as deposit and refund periods are totally disjoint it is not possible that_C asks for a refund of a set of already used microcoupons but not yet deposited by_M.

7.1.6 Overspending Protection

Lemma 7.1.6 The debit-based micropayment scheme described in §3.4 avoids cus-tomers overspend w.r.t. the Definition 3.2.9, because there is no customer able to spend more money than the funds she currently holds in her bank account at the moment of withdrawn.

Proof. _B is in charge of storing bank accounts of customers (acc_C). So, B always knows the remaining funds at every customer account^¡v^acc_C ^¢. When a

customer executes theWithdrawalprotocol with_B, she has to provide the pre-agreed common information that contains the value and the number of microcoupons she want to withdrawn. It is trivial to prove that whether the value she is willing to withdrawn is larger than the amount of money she currently holds in her bank ac-count^¡v^Withdrawal_{C >}v^acc_C ^¢,_Bdenies the withdrawn and returns an error describing the situation with an anotation reporting the remaining funds.

7.1.7 Fairness

Lemma 7.1.7 The micropayment scheme presented in §3.4 meets the controlled fairness requirement w.r.t. the Definition 3.2.13, because the scheme can either as-sure a the fairness with a resolution procedure implemented in theDepositand Refundprotocols or it can provide an improved efficiency without resolution pro-cedures but providing a limited and controlled risk of loss.

Proof. TheSpendprotocol has been designed in such a way that, once it fin-ishes, both_C and_Mwill have the desired items from the other party, if they honestly follow each protocol step. Indeed, if involved parties in theSpendprotocol behave correctly, then the exchange becomes fair. So,_M gets the required microcoupon from_C while_C obtains the item she has willing to purchase from_M.

However, the exchange could became unfair whether _C or _M decides to not follow theSpendprotocol honestly.

The first case happens whether it is_C who does not act in accordance with the Spendprotocol. Certainly, if_C does not send the third message of theSpend protocol with the proof microcoupon^¡_ω(i+1)C^¢,_C has the desired item while _M does not have the corresponding proof microcoupon. However, in order to repair the fairness of the purchase transaction,_M can run theDepositprotocol within the available period (see Figure 3.2 from §3.4.1) defined by the corresponding time mark^¡_τd=τexp+Γ.4τop

¢allocated inside the common information field and par-tially blind signed by_B. During theDepositprotocol,_M sends the last received payment microcoupon(ωiC)which index position within the microcoupon chain has odd valuei, together with the corresponding product previously sent by_M to_C._B executes theCase1from theDepositprotocol resolution. Therefore,_Bstores the product for the exception case explained in the next claim and_Bdeposits the correct amount into the merchant’s bank account. Thus,_M is paid by the product sold and as a result, the fairness is restored.

The second situation is due to the malicious behavior of_M during theSpend protocol. In fact, if_M does not send the second message of the Spendprotocol with the item requested by_C, she will be actually involved in an unfair situation if M executes theDepositprotocol. As stated in the previous case,_M can get the full value of a microcoupon using this protocol even he has not received the proof

information. In this case, _B executes the Case1of the Refund protocol. As a result, the last index stored by_Bin its database is odd and_Bhas the item sent by M, as said before. So,_B can provide the item to_C and it can refund the rest of unused microcoupons from_Cto_C. Therefore,_C has received the item and whether she has had unused microcoupons, she has received the corresponding refund. So, the fairness has been restored again.

We have analyzed the fairness taking into account a procedure split between DepositandRefundprotocols to recover the fairness from an unfair situation due to a malicious behavior. However, this resolution implies the participation of_B storing a provided item by_M during theDepositprotocol to sent it afterward to the harmed_C during theRefundprotocol. As stated in §3.2.10 and §3.4.1, there are some services in which acontrolled fairnessshould be assumed either to improve the efficiency or simply because the resolution does not have sense for the concrete service provisioning (e.g. a streaming service). For these cases, our micropayment scheme allows relaxing the initial fairness avoiding the previous resolutions. There-fore, under thecontrolled fairnessproperty (seeDefinition 3.2.13from §3.2.10), the scheme remains somehow fair but with a controlled and limited risk of loss. The risk the involved parties have to assume is the loss of a single microcoupon per coin C. Since we are dealing on a micropayment for low-value items, in which a single microcoupon represents a small amount of money (up to few cents), the risk is com-pletely reasonable. Besides, if a single party presents a repeated malicious behavior causing that in most of the transactions it tries to cheat the other party, the malicious one has the risk to suffer a partial loss of his reputation. We refer the reader to the formal and automatic analysis of the fairness by the use of the CPN methodology in §7.1.8 to be convinced that harmed party in the last supposition only may loss a single microcoupon. Moreover, we complete the analysis of the first micropayment solution with resolutions with the same formal method.

Remark7.1.2 The micropayment scheme allows tweaking its efficiency in exchange of a controlled and limited risk of loss.

7.1.8 Automatic Formal Fairness Verification with Colored Petri Net In spite fairness has been discussed and proved during the above security discussion, we want to provide further proofs to demonstrate how the micropayment scheme from §3.4 meets the controlled fairness property as described by the Definition 3.2.13. To do it, we present an automatic and formal analysis of this property us-ing the knowledge acquired in Chapter 6. So, first we describe the CPN model that allows us to perform the automatic analysis by using CPNTools. Therefore, we have applied the CPN method to our micropayment proposal taking into account both available versions: either considering the resolutions with the support of_Bor