Worth One Minute (WOM) is a general-purpose rewarding system based on the exchange of anonymous vouchers. It is designed to support crowd-sensing applications that rely on the willingness of users to participate and invest in common causes. The platform rewards the e ort of users toward such causes, thus triggering virtuous circles contributing to the expected social value. The system's reliability depends on the security conditions of the voucher issuing and spending processes. These processes are based on two cryptographic protocols, which are discussed in this paper and formally validated through the automated veri cation tool ProVerif.
1.1
Many di erent kinds of systems rely on the participation of volunteers in order to complete tasks
and achieve their objectives. Tasks that are highly parallel in nature are especially well-suited
to being carried out by a distributed work force. Some of these tasks may require volunteers
to solve problems, collect data, perform measurements, or to provide creative input. This
approach, also known as \crowdsourcing", has been widely seen as a radical new paradigm of
problem-solving that harnesses the contributions of a distributed network of individuals [
In recent years, modern technology and the Web have been adopted to harvest distributed
intellect in order to collect huge amounts of knowledge (such as in Wikipedia), to solve creative
problems, or to perform menial tasks (see Amazon's `Mechanical Turk'). Other examples of
this approach include \volunteer computing", where volunteers o er part of the hardware
resources of their electronic devices in order to solve di cult problems [
Participants in a `crowd'-based system may devote signi cant e orts towards the shared
task, in the form of time, attention, hardware resources, creativity, or even giving access to
private information. Individuals may not be willing to contribute to the common task without
strong incentives for cooperation: thus, a primary aspect of crowdsourced systems is that of
providing incentives and reward schemes for participants, in order to ensure a number of users
that is su cient to guarantee coverage and reliability [
In this setting, a new platform, called \Worth One Minute" (WOM)1, has been proposed
recently to provide a general-purpose incentives system based on the exchange of anonymous
vouchers, simply called WOMs, each of which represents a reward for `one minute' of e ort
towards a common social goal. The platform allows any volunteer-based initiative to reward
the e orts of their participants, endowing them with vouchers that can be collected and spent
within a community that promotes and encourages volunteer activities aimed at the common
good [
The critical security aspects of such a platform are concerned with the privacy of individuals (no personal, sensitive information shall be disclosed as a consequence of the contributions provided and of the vouchers gained and spent) and the reliability of the vouchers management system (no vouchers shall be forged, stolen, double spent, revealed to unauthorized parties). 1.2
The security conditions of the WOM platform are guaranteed by means of ad-hoc cryptographic
protocols governing the interactions among the various parties, the complexity of which requires
strong veri cation. In this paper, we show how to formally verify some authentication and
con dentiality properties of these protocols, by using the proof-theoretic approach implemented
in the software tool ProVerif [
In the following, we discuss the main features of the Worth One Minute infrastructure (Section 2) and of the underlying cryptographic protocols. Then, we present the formal speci cations and veri cation of these protocols through ProVerif (Section 3). Some remarks and feedback about such a modeling and analysis experience are nally reported (Section 4).
1O cial Web site: https://wom.social.
The WOM platform is designed to provide an open and participative infrastructure, which is not bound to a single crowd-based initiative and leverages platform economy mechanics in order to multiply its impact. By decoupling the crowdsourcing system from its incentive scheme, the platform serves as a link between volunteers (who may contribute to one or more common good initiatives) and stakeholders (who wish to support the e orts of volunteers).
The platform is intended to attract volunteer-based initiatives on one side, allowing users to gain vouchers, and third-party subsidizers on the other one, allowing users to spend vouchers. In the context of the WOM platform, the crowd-based tools are called \Instruments" and subsidizers are known as \Merchants". While the platform is open to any volunteer and any Merchant, the addition of a new Instrument to the platform is carefully evaluated by a transparent ethical committee that evaluates whether the Instrument is compatible with the purpose of the platform and the shared goals of subsidizers. 2.1
WOM
The main operations of the WOM platform are concerned with voucher generation and transfer
to the intended user, in response to a legitimate request, as well as voucher veri cation and
spending during a transaction between a user and a Merchant. These operations rely on the
execution of two protocols [
The protocols require the interaction among multiple participants. In particular: the Instrument's client (CT ), which allows the user to perform the intended task and collects related information, and the Instrument's aggregation service (AS ), which gathers volunteer contributions and validates them in order to enable the generation of the related vouchers as a reward. The Registry (REG ) is the central trusted authority of the WOM platform, which manages vouchers and payments. The Pocket (PCK ) is a client-side software controlled by the volunteer, that allows him/her to collect and spend vouchers independently of the speci c Instruments that have been used previously to gain them. Finally, the Point of Sale (POS ) allows Merchants to request new payments, which can then be performed by volunteers by spending vouchers stored in their Pocket.
Table 1 describes the protocol that allows Instruments to gain new vouchers. In steps (a) and (b) the two Instrument-side components CT and AS exchange and transmit the user's contributions (represented by the abstract terms c1, c2, . . . , cn) and a fresh password Pwd (known by the user) to the Registry. Even if they do not include any user identity related information, contributions refer to a speci c task (what common cause was pursued) and where/when they have been generated. Hence, in order to trade for user's privacy, they may be (partially) obfuscated, turning them into c01, c02 . . . ,c0n, before their transfer to the central authority. Notice that communications between CT and AS are secured by the Instrument, by encrypting them with the shared, secret key SK ctas of a symmetric key algorithm. At step (b) a unique nonce N is generated and the identity of the Instrument is added to the message that is sent to the central authority, encrypted with the public key PK reg of the Registry2. Steps (c) to (e) are needed to transmit a unique one-time code (OTC gen ) back to the Instrument. In essence, this code identi es a pending voucher request and takes the form of an URL facilitating the interactions between mobile agents and the central authority. Notice that message (c) includes the nonce N , the identity of the Registry, and is encrypted with the public key PK instr 2With the usual notation PK a, SK a we mean the pair of public and secret keys of an asymmetric encryption algorithm, respectively, for agent a. (b) AS ! REG : (c01; c02; : : : ; c0n; Pwd ; N; IDinstr )PK reg (c) REG ! AS : (N; OTC gen ; IDreg )PK instr (d) AS ! REG : (OTC gen )PK reg (e) AS ! CT : (OTC gen )SK ctas (f) CT ! PCK : (OTC gen ) (g) PCK ! REG : (OTC gen ; Pwd ; Ks)PK reg (h) REG ! PCK : (v1; v2; : : : ; vn)Ks (i) REG ! AS : (N; con rm)PK instr of the Instrument. After the handshake phase between Instrument and Registry, the Instrument transmits the code as a clear text to the user's Pocket, see step (f), which will use it to enable the subsequent voucher claim. On step (g), the Pocket asks the user for the password Pwd again, and then provides the couple OTC gen and Pwd to the Registry. Message (g) includes a fresh key Ks, chosen by PCK. The Registry checks the validity of the pair (OTC gen , Pwd ) and, if the check is passed, sends back the set of vouchers v1, v2, . . . , vn (corresponding to rewards for c01, c02, . . . , c0n, respectively), encrypted with the key Ks. Finally, on step (i) the Registry con rms to AS that the vouchers have been generated and collected.
With respect to the security conditions of interest, it is worth verifying whether the whole process guarantees the con dentiality of the vouchers generated by the Registry, which shall be claimed by and made available to the legitimate user only, without any chance for the adversary to even distinguish between the issuance of di erent vouchers. Moreover, to ensure both the user's privacy and reliability of the protocol phase during which the user's contributions are exchanged, the authentication between Instrument and Registry must be guaranteed. During the protocol execution, it can be assumed that the unique trustworthy party is the Registry central authority, which cannot be impersonated by an adversary.
The second protocol, shown in Table 2, describes the mechanism by which Merchants can request new payments for services delivered to the users. The protocol bears many similarities to the one in Table 1. On steps (j) to (l), the Merchant's Point of Sale (POS ) and the Registry agree on a new payment request, which is speci ed in terms of how many (parameter k) and which type (parameter f ) of vouchers are required. The type can be related to the what/where/when dimensions associated with the user's contributions from which the vouchers derive. The POS component also supplies a code ACK pck which represents the value that will be disclosed to the Pocket on a successful payment. Similarly as in steps (a) and (b) of the previous protocol, in step (j) the POS component also sends a user-speci ed password Pwd, a fresh nonce N , and her identity IDpos . In response to the request, the Registry issues a unique one-time code OTC pay , which is then sent on step (m) as a clear text to the user's Pocket after the handshake phase between POS and Registry. The Pocket component employs the one-time code to request detailed information about the payment on step (n), by exposing also the password speci ed by the user, and a fresh session key Ks1 . In the following step (o) the Registry checks the (j) POS ! REG : (f; k; ACK pck ; Pwd ; N; IDpos )PK reg (k) REG ! POS : (N; OTC pay ; IDreg )PK pos (l) POS ! REG : (OTC pay )PK reg (m) POS ! PCK : (OTC pay ) (n) PCK ! REG : (OTC pay ; Pwd ; Ks1 )PK reg (o) REG ! PCK : (f; k; IDpos )Ks1 (p) PCK ! REG : (OTC pay ; Pwd ; v1; v2; : : : ; vk; h(S); Ks2 )PK reg (q) REG ! POS : (N )PK pos (r) REG ! PCK : (ACK pck )Ks2 pair (OTC pay , Pwd) and, if the check is passed, returns to the Pocket the parameters f and k, along with the Points of Sale identity IDpos , encrypted with the session key Ks1 . On step (p) OTC pay , Pwd , a set of vouchers v1, v2, . . . , vk ful lling the requirements, the hash h(S) of a random value S chosen by the Pocket, and a fresh session key Ks2 are sent by the Pocket to the Registry, which then con rms the payment to the POS on step (q), provided that the vouchers are valid and ful l the requirements. At the end of the exchange, on step (r) the PCK component obtains ACK pck as con rmation of the payment and stores privately the secret S in case of future disputes with the merchant.
The security properties that require validation are similar to the previous case. Indeed, it is worth verifying the authentication between Merchant's POS and Registry, as well as the reliability of the payment, which must be completed by using legitimate vouchers that can be neither stolen nor identi ed by the adversary. Again, it is worth assuming that the Registry is the unique trustworthy agent involved in the protocol execution. 3
The formal veri cation of the security properties of the two WOM protocols has been conducted
through ProVerif [
In the following section, we specify and analyze in detail the voucher generation protocol of
Table 1. The reader interested also in the spending protocol of Table 2 can refer to the o cial
website [
ProVerif speci cations include three sections: declarations, process macros, and the main process. Declarations specify names and types: free ch: channel. (* Public channel of communication *) (* Types *) type nonce. (* Nonce *) type pkey. (* Public key *) type skey. (* Secret key *) (* Names and costants *) free cn: bitstring [private]. (* contributions *) free vn: bitstring [private]. (* vouchers *) free confirm: bool. (* final confirmation *) (* Type converter *) fun nonce_to_bitstring(nonce): bitstring [data,typeConverter].
Notice that both user's contributions and vouchers are abstracted by terms cn and vn, respectively. The keyword [private] excludes the name to which it is applied from the adversary's knowledge. The declaration section includes also the de nition of the functions formalizing the behavior of the cryptographic primitives: (* Public key encryption *) fun pk(skey): pkey. fun aencrypt(bitstring, pkey): bitstring. reduc forall x: bitstring, y: skey; adecrypt(aencrypt(x, pk(y)), y) = x. (* Shared key encryption *) fun sencrypt(bitstring, skey): bitstring. reduc forall x: bitstring, y: skey; sdecrypt(sencrypt(x, y), y) = x.
Secrecy assumptions are then added to specify initial limitations of the adversary, who cannot know the secret key SKctas shared by CT and AS, the secret keys for asymmetric encryption possessed by AS (SKinstr) and REG (SKreg), and the password Pwd known by the user. Notice that the use of such assumptions preserves soundness of the veri cation, because the tool also checks that these secrets cannot be derived at any time. (* Secrecy assumptions *) not attacker(new SKctas). not attacker(new SKinstr). not attacker(new SKreg). not attacker(new Pwd).
Then, the declarations section terminates with the speci cation of the security properties of
interest, which are de ned as queries. The rst set of properties is related to the secrecy of
critical information:
(* Secrecy queries *)
(* To test secrecy of critical information *)
query secret Pwdreg; (* Pwd chosen at the Instrument side *)
secret Nreg; (* Nonce exchanged by AS and REG *)
attacker(vn).
noninterf vn. (* To test strong secrecy of vouchers *)
The keyword secret expresses a query testing the secrecy of bound variables inside the related
process, which are, in our case, the password shared by the Instrument components and known
to the agent (see name Pwdreg), and the nonce exchanged by Instrument and Registry (see
name Nreg). The meaning and scope of such names will be clear in the next section of the
speci cation dedicated to the formal description of the various agents' behavior. An alternative
way to test secrecy is through the command attacker, which in our example is used to check
whether the vouchers vn can be derived by the attacker. In such a case, we also model a strong
secrecy property based on a noninterference condition, i.e., we check (through observational
equivalence [
Mutual authentication (between AS and REG) is captured by asserting a one-to-one correspondence between speci c events in order to express conditions of the form \if event e2 occurs, then event e1 has been observed previously ". (* Authentication queries *) event beginREGAuthparam(pkey). event endREGAuthparam(pkey). event beginASAuthparam(pkey). event endASAuthparam(pkey). query x: pkey; inj-event(endREGAuthparam(x)) ==> inj-event(beginREGAuthparam(x)). query x: pkey; inj-event(endASAuthparam(x)) ==> inj-event(beginASAuthparam(x)). The speci c nature of the events will be determined within the description of the agents involved in the authentication.
In the second section of the ProVerif speci cation, process macros are used to de ne the agents and their behavior in the protocol. First of all, we have the CT agent, described by the following process term processCollectionTool: (* Collection Tool *) let processCollectionTool(SKctas: skey, Pwd: nonce) =
(* Message (a): transfer the contributions and the password to AS *) out(ch, sencrypt((cn, Pwd), SKctas)); in(ch, (message_e: bitstring));
(* Symmetric decryption with the shared key SKctas *) let (OTCgenX: bitstring) = sdecrypt(message_e, SKctas) in
(* Message (f): send OTCgenX to PCK in clear *) out(ch, OTCgenX).
The process has two arguments, which are the secret key SKctas of type skey and the password Pwd of type nonce, and is de ned in terms of the sequence of message exchanges in which it is involved, either as sender or as receiver (see Table 1). Firstly, the process sends to the public channel ch message (a) of the protocol, encrypted with the shared, secret key SKctas (see the out command), and then waits for the message (e) containing the encrypted one-time code (see the in command), which in turn is decrypted and nally sent to PCK in message (f), see the let and the subsequent out commands. Analogously, we have the AS agent: (* Aggregation Service *) let processAggregationService(PKreg: pkey, SKinstr: skey, SKctas: skey) = in(ch, message_a: bitstring);
(* Decrypt message (a) with the shared key SKctas *) let (c: bitstring, PwdX: nonce) = sdecrypt(message_a, SKctas) in (* BEGIN AUTHENTICATION WITH REG *) (* Await to read pkX on channel ch *) in(ch, pkX: pkey); if pkX = PKreg then
(* Start the run of the protocol with PKreg *) event beginREGAuthparam(pkX);
(* Generate a random nonce N *) new N: nonce;
(* Message (b): request vouchers generation *) out(ch, aencrypt((c, PwdX, N, pk(SKinstr)), pkX)); in(ch, message_c: bitstring); (* Asymmetric decryption of message (c) with secret key SKinstr
Check N and pkX using pattern matching. *) let (=N, OTCgenX: nonce, =pkX) = adecrypt(message_c, SKinstr) in
(* Message (d): send OTCgenX as confirmation *) out(ch, aencrypt(nonce_to_bitstring(OTCgenX), pkX));
(* Record the end of the protocol with pkX *) event endASAuthparam(pk(SKinstr)); (* END AUTHENTICATION WITH REG *) (* Message (e): send OTCgenX to CT *) out(ch, (sencrypt(nonce_to_bitstring(OTCgenX), SKctas))); in(ch, message_i: bitstring);
(* Decrypt message (i) and check the content via pattern matching *) let (=N, =confirm) = adecrypt(message_i, SKinstr) in 0.
The speci cation describes the phases of the protocol and the message exchanges in which AS is involved, as given in Table 1. For instance, the rst message, received from CT, is decrypted with SKctas and shall include the contributions and the password, represented by names c and PwdX. Then, the subsequent authenticated handshake is executed with the Registry agent, which is identi ed by the public key read from the channel, see name pkX and the equality check pkX = PKreg. Two events denote the beginning (with REG) and the end (by AS ) of such a handshake. The correctness of the content of received messages is veri ed through pattern matching, e.g., the incoming bitstring message_c is correct if it can be decrypted with SKinstr, and the resulting three elements are the nonce N previously generated and sent, a nonce assigned to name OTCgenX, and pkX (see the let command managing the bitstring message_c). In a similar way, we have the description of the agent REG: (* Registry *) let processRegistry(PKinstr: pkey, SKreg: skey) =
(* BEGIN AUTHENTICATION WITH AS *) in(ch, message_b: bitstring);
(* Asymmetric decryption of message (b) with secret key SKreg *) let (c: bitstring, PwdY: nonce, NY: nonce, pkY: pkey) = adecrypt(message_b, SKreg) in (* Start the run of the protocol with pkY *) event beginASAuthparam(pkY);
(* Generate one-time code OTCgen *) new OTCgen: nonce;
(* Message (c): issue OTGgen needed to claim the new vouchers *) out(ch, aencrypt((NY, OTCgen, pk(SKreg)), pkY)); in(ch, message_d: bitstring);
(* Check OTCgen *) if nonce_to_bitstring(OTCgen) = adecrypt(message_d, SKreg) then if pkY = PKinstr then
(* Record the end of the protocol with pkY *) event endREGAuthparam(pk(SKreg)); (* END AUTHENTICATION WITH AS *) (* Assign NY and PwdY to new names to test secrecy queries *) let Nreg = NY in let Pwdreg = PwdY in in(ch, (message_g: bitstring));
(* Check correctess of OTCgen and PwdY using pattern matching *) let (=OTCgen, =PwdY, KsY: skey) = adecrypt(message_g, SKreg) in
(* Message (h): vouchers sent to PCK using session key KsY *) out(ch, (sencrypt((vn), KsY)));
(* Message (i): notify the transfer of vouchers to AS *) out(ch, (aencrypt((NY, confirm), PKinstr))).
Notice that the Registry is available to start an authenticated session with the agent identi ed by the public key pkY received in message (b). As observed above, the handshake is delimited by the beginning (with AS ) and the end (by REG) events, which together with the two events of agent AS are used to de ne the mutual authentication queries. At the end of the handshake we can nd the speci cation of the names subject to the secrecy queries, i.e., the nonce and the password exchanged with the Instrument. The agent PCK is de ned as follows: (* Pocket *) let processPocket(PKreg: pkey, Pwd: nonce) =
(* Await to receive one-time code OTCgen *) in(ch, (OTCgenZ: nonce)); new Ks : skey; (* Generate a new session key Ks *)
(* Message (g): reedem request *) out(ch, (aencrypt((OTCgenZ, Pwd, Ks), PKreg))); in(ch, (message_h: bitstring));
(* Symmetric decryption of vouchers with secret key Ks *) let (=vn) = sdecrypt(message_h, Ks) in 0.
Finally, the main process describes the whole architecture of the system by declaring the instances of the agents involved and the knowledge possessed by such instances. In particular, the pairs of keys of asymmetric encryption must be declared and the public keys broadcast via the public channel. Moreover, the password Pwd must be in the initial knowledge of CT and PCK, while the secret key SKctas must be shared by CT and AS. process new SKctas: skey; new Pwd: nonce; (*** MAIN PROCESS ***) (* Create the key shared between CT and AS *) (* Create the user password used at the client side *) (* Create the secret key of Instrument *) new SKinstr: skey;
(* Create and transmit on channel ch the public key of Instrument *) let PKinstr = pk(SKinstr) in out(ch, PKinstr);
(* Create the secret key of Registry *) new SKreg: skey;
(* Create and transmit on channel ch the public key of Registry *) let PKreg = pk(SKreg) in out(ch, PKreg); ( (* Launch an unbounded number of sessions of the Collection Tool,
Aggregation Service, Registry, and Pocket *) (!processCollectionTool(SKctas, Pwd)) | (!processAggregationService(PKreg, SKinstr, SKctas)) | (!processRegistry(PKinstr, SKreg)) | (!processPocket(PKreg, Pwd)) ) The feedback provided by the automated veri cation reveals a vulnerability because of which the attacker may obtain the secret password Pwd. Indeed, in the last outgoing message (f), the CT agent simply forwards, without any check, the one-time code extracted from message (e). However, the attacker may drop message (e) and replay message (a), thus inducing CT to inadvertently disclose the password in message (f), as reconstructed by ProVerif in the form of an execution trace. Checking the content of message (f) is somehow implicit in the description of Table 1, but it cannot be given for granted in the protocol implementation, which could skip such a check because of some form of code optimization. Hence, to avoid the replay attack it is worth verifying that the bitstring in message (f) is not a tuple, by changing the last line of the CT component as follows:
if OTCgenX <> (cn, Pwd) then out(ch, OTCgenX).
The automated veri cation with such a modi cation demonstrates the satisfaction of the security queries: C:\...\proverif2.00>proverif WOM_vouchersGeneration.pv RESULT secret Pwdreg is true.
RESULT secret Nreg is true.
RESULT not attacker(vn[]) is true.
RESULT Non-interference vn is true (bad not derivable).
RESULT inj-event(endREGAuthparam(x_25)) ==> inj-event(beginREGAuthparam(x_25)) is true. RESULT inj-event(endASAuthparam(x_26)) ==> inj-event(beginASAuthparam(x_26)) is true. Therefore, ProVerif has been useful to reveal and avoid a potential attack, thus con rming that it is worth paying attention to the way in which even simple message exchanges are implemented. 4
The complexity of the two WOM cryptographic protocols|in terms of number of agents and communications involved|and the variety of security conditions to verify|from authentication, to secrecy and noninterference|demand a tool-supported formal analysis, which has been conducted in this paper by using ProVerif. The experimental results revealed that the two vouchers management protocols are secure with respect to the properties of interest. Also, by analyzing the voucher generation protocol some potential subtleties emerged, which emphasize the importance of strict and continuous interactions among software designers, developers, and experts in veri cation.
In general, the success of such a kind of veri cation process strictly depends on the usability and expressiveness of the analysis tool at hand. To give some useful feedback about our experience, the case study presented in this paper has been conducted with the e ort of a BSc student in Computer Science with some experience in concurrency theory, logic programming, formal veri cation, and model checking. The training period required to gain experience and familiarity with ProVerif was about one month, after which the speci cation of the WOM cryptographic protocols required three more weeks, the rst one of which was necessary for the study of the WOM platform. Hence, we believe that this experience shall convince the security protocol/system developer that formal veri cation is not only mandatory but also feasible with a reasonable e ort even in the case of complex systems.