Design a protocol

Cryptographic protocols, Autumn 2008, 1st home exercise

A number of servers are offering the services for secure storage. A user can contact a server, pay a nominal fee, and upload his/her file, receiving back a small token. Later, the same user, or a different user can present that token to the server, and retrieve his/her file.

Design protocols for storing and retrieving files. Please assume the following:

There is a CA that issues certificates to storage servers. The users know the verification key of that CA (only).
The fee is represented by a message M_coin, signed by the CA. Initially, it is known by the user wanting to store its file. During the storage protocol, only the server storing the file should learn it.
The file that the user stores should not become known to the storage server (i.e. encrypt it).
If a server does not honour a legitimate request for a file, the user must be able to accuse him in front of others (i.e. we need non-repudiation).

There are some other obvious requirements. It is your task to find and formulate them, and design the protocols according to them.

Please argue that the protocols work and are secure. Please model the protocols in ProVerif and do a formal verification of them. If your design process turns out to be iterative, then please show me the intermediate results, too.