When paying for goods in a store, one can use either cash or debit/credit card. One major difference between those modes of payment is, that using a card creates a link between the buyer and the purchase, but cash payments remain anonymous. The first proposal for anonymous electronic payments [Chaum, CRYPTO '82] involved the use of blind signatures as follows:
To get a coin C, Alice contacts the Bank and sends it a blinded token blind(t,r) that the Bank signs. From this signature Alice can compute bank's signature s on t. The bank will learn nothing about t. Simultaneously with signing, the Bank debits Alice's account by 1 EEK. The certificate for the Bank's public key states that this key is intended for signing 1 EEK bills.
To pay Bob, Alice will hand him the token t and its signature s. Bob sends them to the Bank. Bank verifies the signature and checks that it has not received the same token t before. If the checks are successful then the Bank credits Bob's account by 1 EEK.
Blind signatures are easy to create if the RSA signature scheme is used. Let (n,e) be the Bank's public key and let d be the corresponding secret exponent. To blind a token t, Alice will generate a random r in Zn and send tre mod n to the Bank The Bank will sign it, resulting in (tre)d = tdr mod n. This value is sent back to Alice who will then divide it by r, giving her the signature td of t.
Your exercise is to model the previous protocol in ProVerif and also secure it as necessary, such that the following obvious properties will hold
Alice's account will only be debited if a coin is issued to her (the coin can get lost in transit, but noone else should learn it). Also, the Bank will issue a coin only after debiting someones account.
The coin issued to Alice can only be used by her (if she guards it well before spending).
A coin can be spent only once (that is probably hard to verify with ProVerif).
When the Bank credits Bob's account, it will not learn who payed Bob.
Any other obvious properties that I may have forgotten...
Please model these properties as secrecy, authenticity, or process equivalence properties, as you see fit. Blinding can be modeled by having a constructor blind and a destructor unblind. Please send me the descriptions of protocols, and the ProVerif model files.