Cryptographic protocols 2009, second home exercise

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:

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

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.