(* Post-review: Unified ProVerif specification, version 14, for Scytl's Voting Protocol. All variants included. Tabulation size : 8 spaces. *) (* Reachability ............ : For Cast as Intended and Tallied as Cast properties; from study_v14.pve with the 'REA' option. *) (* Observational Equivalence : For Ballot Provivacy; 2 honest + many dishonest in the challenge; [..] with the 'OBS' option w/ or w/o HH. *) (* 0. Maintenance informations. *) (* Notation changes from Report to Paper *) (* Report : pCC, CC, sCC -> Paper : pRC, RC, sRC *) (* Report : CM_table, CMtable -> Paper : M_table, M *) (* Report : S_VCC -> Paper : CRF, aka SigFC *) (* Report : VCCssk, VCCspk -> Paper : Skc, Pkc *) (* idem vccssk/skc .. *) (* Report : VCC, sVCC -> Paper : FC, sFC *) (* Report : BCKid, bck -> Paper : CCid, cc *) (* Report : VCksid -> Paper : Ks *) (* and obtained through decryption *) (* Report : VCidsk, VCidpk -> Paper : Skid, Pkid *) (* Report : KSpwd, VCid -> Paper : Kid, Id *) (* Kid not in the spec, used as deltaKey(SVKid) *) (* Report : Csk, csk -> Paper : Ska, ska *) (* Report : EBpk, EBsk -> Paper : Pkb, Skb *) (* instead of Pk,Sk because too confusing with other keys *) (* Report : ebpk, ebsk -> Paper : pkb, skb *) (* alias pk,sk *) (* Notation changes from Scytl to Paper *) (* Types : agent_id -> agentId private_ekey -> ekey public_ekey -> epkey symmetric_ekey -> symkey *) (* private_skey -> skey public_skey -> spkey symmetric_key -> symkey -- for Ska, fused with symkey *) (* Functions : Enc_c1 -> aenc1 Enc_c2 -> aenc2 Enc -> aenc Enc_s -> enc Dec -> adec Dec_s -> dec *) (* Role Alice : Alice -> Voter sRC_Received -> sRC' GetVoterData(... reordered) Confirmed/HappyUser with InitData -> SVK *) (* Role Cmp : Cmp -> Device Computer -> VDevice *) (* ZKP : Remove tild from ZKP; also in EC; Ballot: C -> E; phi -> (..,..); *) (* Fonction v(..) : nat -> bitstring en résultat; pRC(.. nat) --> bitstring; cc(..) : nat -> bitstring; sRC(..nat) --> bitstring; *) (* Retour : conserver CCid at sFCid dans Voter, Device, et Voter_Device, pour éviter le conflit avec cc(..) et sFC(..). *) (* InsertBB : encryption E au leiu de ballot (E, ..); Type : nat -> int *) (* NOTE : The notations in this model matches the ones in the EuroSP'17 submission. However, small differences may exist. *) (* For example : Ska in this model is called gka in the submission. A password pwd in the submission is called svk here. *) (* The ProVerif model is also more precise. For example, it makes the difference between voting choices (the index of a candidate *) (* in the list) and voting options (the prime number associated to this index). Also, Tallied-as-Cast -> Individual Verifiability *) set ignoreTypes=false. (* 1. Objects and Types *) type agentId . fun t_agentId(agentId) : bitstring [data,typeConverter]. (* The type for any IDs like e.g. voter's Id. *) type password. fun t_password(password) : bitstring [data,typeConverter]. (* The type for user passwords. *) type int . fun t_int(int) : bitstring [data,typeConverter]. (* The type for integers (modulo). *) free c : channel . (* Public Channel for communications with the intruder # public *) fun v(int) : int [data] . (* The function from voting choices to voting options # public , invertible *) table bb(agentId,bitstring) . (* The Ballot Box, storing the ballots for each agent # private *) table cb(agentId,bitstring,bitstring) . (* The Confirm. Box, storing FC/CRF for each agent id # private *) free svka, svkb : password [private]. (* Defines two SVK for two honest voters Alice and Bob # public *) free ja1,jb1,ja2,jb2 : int . (* Voting choices for the Honest voters -- REA or OBS # public *) free a1,a2 : int . (* MODELING : an indexed set of int atoms, for disquality tests -- only in Test. *) (* 2. Intruder capabilities and functions extracted from the CryptoPaper. *) (* Encryption scheme -- from CryptoPaper, page 4 -- expected to be ElGamal -- Key pairs generated through Gen_e, which is implicit. *) type ekey . fun t_ekey(ekey) : bitstring [data,typeConverter]. (* The type for private keys + type converter. *) type epkey. fun t_epkey(epkey) : bitstring [data,typeConverter]. (* The type for public keys + type converter. *) fun ske(agentId) : ekey [private] . (* The private enc. key associated to an agentId # private *) fun pube(ekey) : epkey . (* The function to rebuild a public key from the private # public , noninvertible *) letfun pke(Id:agentId) = pube(ske(Id)) . (* The public enc. key associated to an agent id # public , invertible *) fun aenc1( int) : int . (* The c1 part of the asymmetric encryption function with explicit random number. *) fun aenc2(epkey,bitstring,int) : bitstring . (* The c2 part of the asymmetric encryption function with explicit random number. *) letfun aenc(Pk:epkey,M:bitstring,R:int) = (aenc1(R),aenc2(Pk,M,R)). (* Encryption *) reduc forall Sk:ekey , M:bitstring, R:int; adec(Sk,(aenc1(R),aenc2(pube(Sk),M,R))) = M . (* Decryption *) reduc forall Pk:epkey, M:bitstring, R:int; VerifE(Pk,(aenc1(R),aenc2(Pk,M,R))) = true. (* Checks key *) reduc forall Id:agentId; Get_Id(pube(ske(Id))) = Id . (* Extract Id *) (* Signature scheme -- from CryptoPaper, page 4 & 5 -- expected to be the RSA Probabilistic Signature Scheme (PSS) -- Gen_s implicit. *) type skey . fun t_skey(skey) : bitstring [data,typeConverter]. (* The type for private keys + type converter. *) type spkey. fun t_spkey(spkey) : bitstring [data,typeConverter]. (* The type for public keys + type converter. *) fun sks(agentId) : skey [private] . (* The private sig. key associated to an agentId # private *) fun pubs(skey) : spkey . (* The function to rebuild a public key from the private # public , noninvertible *) letfun pks(Id:agentId) = pubs(sks(Id)) . (* The public sig. key associated to an agent id # public , invertible *) fun Sign(skey,bitstring) : bitstring . (* The digital signature function with explicit random number. (Signature) *) reduc forall Sk:skey, M:bitstring; Verify(pubs(Sk),M,Sign(Sk,M)) = true. (* Verification *) reduc forall Sk:skey, M:bitstring; Checks(pubs(Sk),Sign(Sk,M)) = M . (* More expressive than Verify. *) reduc forall Sk:skey, M:bitstring; Get_Message(Sign(Sk,M)) = M . (* Worst case for modeling only *) (* Modeling of the Non-Interactive Zero-Knowledge Proofs of Knowledge -- from CryptoPaper, pages 5 & 6 -- Names changed for abstractions. *) (* Both the 'Equality of discrete logarithms' (used in two variants) and the 'Knowledge of encryption exponent' are abstracted inside the *) (* ZKP and VerifP operators. Consequently, the c1~ and c2~, which are intermediate values, are not needed anymore and thus abstracted away. *) (* Moreover, the 'Correct decryption' is not needed for this modeling w.r.t the expected security properties. *) fun pRC(ekey,int) : int. (* The built of partial Return Codes (ski,vi) = vi^ski # public , noninvertible *) reduc forall Sk:ekey, V:int; Get_Vote1(pRC(Sk,V),Sk) = V . (* Worst case for modeling only *) fun ZKP(epkey, epkey, bitstring, int,int, int, ekey) : bitstring. (* Modeling of the proof generation *) reduc forall Pkb:epkey, Skid:ekey, v1:int,v2:int, R:int; (* Modeling of the proof verification *) VerifP(Pkb, pube(Skid), (aenc1(R),aenc2(Pkb,(t_int(v1),t_int(v2)),R)), pRC(Skid,v1),pRC(Skid,v2), ZKP(Pkb, pube(Skid), (aenc1(R),aenc2(Pkb,(t_int(v1),t_int(v2)),R)), pRC(Skid,v1),pRC(Skid,v2), R,Skid)) = true. (* Consequently to abstracting c1~ and c2~ away from ZKP/VerifP, we do not need anymore the 4 variants of this reduction shown previously. *) (* Remaining limitation : the agregation function phi(..) is commutative, but modeled as a pair; otherwise far too many cases for ProVerif. *) (* Symmetric encryption scheme -- from CryptoPaper Draft update, page 3 -- expected to be based on AES *) type symkey. fun t_symkey(symkey) : bitstring [data,typeConverter]. (* The type for symetric encryption keys. *) fun enc(symkey,bitstring) : bitstring. (* Encryption (symmetric key) *) reduc forall SymK:symkey, M:bitstring; dec(SymK,enc(SymK,M)) = M. (* Decyption (symmetric key) *) (* Key and IDs derivation scheme -- from CryptoPaper Draft update, page 3 *) (* free IDseed : bitstring . *) (* A public seed for IDs -- Not needed: value fixed # public *) (* free KEYseed : bitstring . *) (* A public seed for KEYs -- Not needed: value fixed # public *) fun deltaId(password) : agentId . (* The delta function, for agents IDs # public *) fun deltaKey(password) : symkey . (* The delta function, for symmetric encryption keys # public *) (* Keyed Pseudo-Random and hash functions -- from cryptoPaper, pages 7 & 8 -- Note: Not the same keys as for symmetric encryption *) fun H(symkey) : bitstring . (* The hash function -- from CryptoPaper page 5 # public , noninvertible *) fun f(symkey,int) : symkey . (* The keyed pseudo-random function f -- page 7 # public , noninvertible *) (* 3. Initialization sequence (done off-line in this modeling). *) (* Setup(...) i.e. the initialisation step from the Registrar -- done off-line in this modeling -- from CryptoPaper page 9 *) free election : agentId . (* The election id - used to derive public/private keys # public (sk is private) *) free signature : agentId . (* The signature id - used to derive public/private keys # public (sk is private) *) letfun pkb = pke(election) . (* The Election public key (for the Board) in (Pkb,Skb) # public *) letfun skb = ske(election) . (* The Election private key (for the Board) in (Pkb,Skb) # private *) free ska : symkey [private] . (* The Global Audit key 'Ska' (for f(...) function) # private *) letfun pkc = pks(signature) . (* The Global Confirmation public key in pair (Pkc,Skc) # public *) letfun skc = sks(signature) . (* The Global Confirmation private key in pair (Pkc,Skc) # private *) (* Register(..,id,ska,skc) ie. the registration step for any new voter -- done off-line through functions -- from CryptoPaper page 9 *) fun cc(agentId) : int [private] . (* The Confirmation Code 'CC^id' of an agent id # private *) fun sRC(symkey,agentId,int) : bitstring [private] . (* The short Return Code 'sRC^id_i' of an agent id + voting option # private *) fun sFC(symkey,agentId) : bitstring [private] . (* The short Finalization Code 'sFC^id' of an agent id # private *) reduc forall SVK:password; GetKs(deltaId(SVK)) = enc(deltaKey(SVK), t_ekey(ske(deltaId(SVK)))). (* CryptoPaperDraft upd.page 4 *) fun M_table(symkey,agentId) : bitstring . (* The Mapping Table ('M_id', unbounded) -- opened with readRC/FC(). *) reduc forall Ska:symkey, Id:agentId, J:int; readRC(H(f(Ska, pRC(ske(Id),v(J) ))), M_table(Ska,Id)) = enc(f(Ska, pRC(ske(Id),v(J) )), sRC(Ska,Id,v(J))). (* enc(RC,sRC) *) reduc forall Ska:symkey, Id:agentId; readFC(H(f(Ska, pRC(ske(Id),cc(Id)))), M_table(Ska,Id)) = enc(f(Ska, pRC(ske(Id),cc(Id))), sFC(Ska,Id)) . (* enc(FC,sFC) *) (* For any voter id, generates Pkid,Skid ............ : pke(id) and ske(id) and GetKs(id) -- distributed in encrypted private data. *) (* For any voter id, chooses a confirmation key ..... : cc(id) as defined above; -- distributed in VoterData and Mapping. *) (* For any voter id, computes a list of Return Codes RC(id,i) ......... : with f(..) and pRC(..) and v(i) -- used to build the Mapping. *) (* for any voter id, computes the Finalization Code FC(id) ........... : with f(..) and pRC(..) and cc(id) -- used to build the Mapping. *) (* for any voter id, chooses the short RC and short FC ................ : with sRC(..) and sFC(..) -- distributed in VoterData and Mapping. *) (* For any voter id, computes the signature of the Finalization Code .. : Sign(skc,sFC(id)) -- distributed in ServData. *) (* For any voter id, stores a list of hashed Return Codes {H(RC(id,i))}_i=1..inf ..... : through MakeRFList -- distributed in ServData. *) (* Registration data for any voter id -- VoterData(svk,ska) produced by the Registrar for Voter -- opened with a reduction *) fun VoterData(password,symkey) : bitstring [private]. reduc forall Ska:symkey, SVK:password, J1:int,J2:int; GetVoterData(VoterData(SVK,Ska),J1,J2) = (SVK, sRC(Ska,deltaId(SVK),v(J1)),sRC(Ska,deltaId(SVK),v(J2)), cc(deltaId(SVK)), sFC(Ska,deltaId(SVK))). (* Note: The set of sRC(id,v(J)) is a selection of sRC corresponding to the {J$i|$i=1..2}, decided at Voter's initialisation. *) (* Registration data for the server (Bulletin Board) -- ServData(pke,Ska,sks) produced by the Registrar -- opened with a reduction *) fun ServData(epkey,symkey,skey) : bitstring [private]. reduc forall Pkb:epkey, Ska:symkey, Skc:skey, SVK:password; (* Note : Id = deltaId(SVK) *) GetServData(ServData(Pkb,Ska,Skc),deltaId(SVK)) = (Pkb, Ska, pubs(Skc), enc(deltaKey(SVK),t_ekey(ske(deltaId(SVK)))), M_table(Ska,deltaId(SVK)), Sign(Skc,sFC(Ska,deltaId(SVK))) ). (* 4. Algebraic properties and List of Events *) (* Equational theory commented out -- Kept for reference but this property is not supported by ProVerif. *) (* equation forall {V$i:bitstring|$i=1..2}; ({t_int(V$i)|$i=1..2}) = ({t_int(V$i)|$i=1..2 'mixed' }). *) (* Commutativity *) event Confirmed(password, int,int). (* Issued by the voter when he/she confirms his/her vote. *) event HappyUser(password, int,int). (* Issued by the voter when he/she terminates successfuly. *) event InsertBB( agentId, bitstring). (* Issued by the server when it adds someting in BB. *) event HasVoted( bitstring, agentId, bitstring, bitstring, bitstring). (* Issued by the server when it gets a voter's confirmation. *) event NeverTrue. (* An event that is never activated, and thus, never true. *) event Results(int,int,int,int). (* Issued by the Tally when it publishes the results. *) (* 5. Methods and Agents processes *) (* GetID(SVKid) -- VDevice generates the Voter's identifier -- Directly replaced by deltaId(SVKid) -- from CryptoPaper update page 4. *) (* letfun GetID(SVKid:password) = deltaId(SVKid). *) (* GetKey(SVKid,Ks) -- VDevice retreives the Voter's private voting key from the keystore -- from CryptoPaper update page 4. *) letfun GetKey(SVKid:password,Ks:bitstring) = let t_ekey(Skid:ekey) = dec(deltaKey(SVKid),Ks) in Skid . (* CreateVote(Pkb,Id,Vopt,Skid) -- VDevice creates the ballot -- from CryptoPaper pages 9 & 10. *) (* NOTE : Change w.r.t. the CryptoPaper Update page 4 : Pkb added as 1st argument, because it is needed by this method. *) letfun CreateVote(Pkb:epkey,Id:agentId,J1:int,J2:int,Pkid:epkey,Skid:ekey) = let V = (t_int(v(J1)),t_int(v(J2))) in new R:int; let E = aenc(Pkb, V, R) in let P = ZKP(Pkb,Pkid,E,pRC(Skid,v(J1)),pRC(Skid,v(J2)), R,Skid) in (E, pRC(Skid,v(J1)),pRC(Skid,v(J2)), Pkid, P) . (* ProcessVote(bb,Id,B) -- Server checks and processes the ballot -- bb tested and filled outside -- from CryptoPaper page 10. *) letfun ProcessVoteCheck(Pkb:epkey,Id:agentId,B:bitstring) = let (E:bitstring, W1:int,W2:int, =pke(Id), P:bitstring) = B in let Ok1 = VerifP(Pkb,pke(Id),E,W1,W2, P) in (* let Ok2 = VerifE(Pkb, E) in NOTE : Commented out because this is not shown in the last version of the CryptoPaper (02/2017). *) true . (* CreateRC(B,ska,M) -- Server prepares the Return Codes -- aka. CreatePallotProof -- from CryptoPaper page 10. *) letfun CreateRC(B:bitstring,Ska:symkey,M:bitstring) = let (E:bitstring, W1:int,W2:int, Pkid:epkey, P:bitstring) = B in let (RC1:symkey,RC2:symkey) = (f(Ska,W1),f(Ska,W2)) in let sRC1 = dec(RC1,readRC(H(RC1),M)) in let sRC2 = dec(RC2,readRC(H(RC2),M)) in (sRC1,sRC2) . (* Confirm(Id,B,Skid,CCid) -- VDevice generates a Confirmation Message -- Done directly inside 'Device' and 'Voter_Device'. *) (* AuditBallotProof(({sRC'$i|$i=1..2}),({sRCid$i|$i=1..2})) -- Voter checks if all expected RC were indeed received. *) (* According to the CryptoPaper update, instead of a method, this is done directly inside the 'Voter' and 'Voter_Device' processes. *) (* ProcessConfirm(bb,Id,CMid,Ska,Skc,..) -- Server checks the retreived short Finalization Code. *) (* Instead of a method, this is done directly inside the 'Serv' process. *) (* Typing of the messages -- between Voter and his VDevice only *) free mAC1, mAC2, mCA1, mCA2 : bitstring. (* Voter -- The client process *) let Voter(Ch1:channel,InitData:bitstring,J1:int,J2:int) = (* Checks that the voting choices are all different *) if (J1 = J1 && a1 <> a1) || (J1 = J2 && a1 <> a2) then 0 else if (J2 = J1 && a2 <> a1) || (J2 = J2 && a2 <> a2) then 0 else (* No honest voter can use twice the same option *) (* Retrieves registration data obtained from the Registrar -- Set of initial data given to Voter by the Registrar. *) let (SVK:password, sRC1:bitstring,sRC2:bitstring, CCid:int, sFCid:bitstring) = GetVoterData(InitData,J1,J2) in (* Voting part -- The voting process followed by agent Voter *) out(Ch1, ( mAC1,SVK,J1,J2)); in( Ch1, (=mCA1,(sRC'1:bitstring,sRC'2:bitstring))); if ((sRC'1=sRC1) || (sRC'2=sRC1)) && ((sRC'1=sRC2) || (sRC'2=sRC2)) then (* Compares the short Return Codes. *) ( event Confirmed(SVK, J1,J2); out(Ch1, ( mAC2,CCid)); in( Ch1, (=mCA2,=sFCid)); (* Voter checks the Finalization Code's value. *) event HappyUser(SVK, J1,J2) ) . (* VDevice -- The Voter's computer *) let Device(Ch1:channel,Ch2:channel,Pkb:epkey) = in( Ch1, (=mAC1,SVK:password,J1:int,J2:int)); (* The Voter password plus the Voting options. *) let Id:agentId = deltaId(SVK) in (* The GetID method; CryptoPaperUpdate page 4. *) out(Ch2, Id); (* Sends the Voter's Id to the Bulletin Board. *) in( Ch2, Ks:bitstring); (* Receives the associated Voter's keystore. *) let Skid = GetKey(SVK,Ks) in (* Retreives the associated Voter's private key. *) out(Ch2, CreateVote(Pkb,Id,J1,J2,pube(Skid),Skid)); (* Sends the ballot (ie. 'Vote') to the server. *) in( Ch2, sRC_Set:bitstring); (* Transmits the Return Codes to the voter. *) out(Ch1, ( mCA1,sRC_Set)); in( Ch1, (=mAC2,CCid:int)); out(Ch2, pRC(Skid,CCid)); (* The Confirm(Id,_,Skid,CCid) voter's method. *) in( Ch2, sFCid:bitstring); (* Transmits the Finalization Code to the voter. *) out(Ch1, ( mCA2,sFCid)) . (* MODELING -- Voter plus her VDevice together (if both honest, to avoid useless secure communications). *) let Voter_Device(InitData:bitstring,J1:int,J2:int,Ch2:channel,Pkb:epkey) = (* Checks that the voting choices are all different *) if (J1 = J1 && a1 <> a1) || (J1 = J2 && a1 <> a2) then 0 else if (J2 = J1 && a2 <> a1) || (J2 = J2 && a2 <> a2) then 0 else (* No honest voter can use twice the same option *) (* Retrieves registration data obtained from the Registrar -- Set of initial data given to Voter by the Registrar. *) let (SVK:password, sRC1:bitstring,sRC2:bitstring, CCid:int, sFCid:bitstring) = GetVoterData(InitData,J1,J2) in (* Voting part -- The voting process followed by agent Voter *) let Id:agentId = deltaId(SVK) in (* The GetID method; CryptoPaperUpdate page 4. *) out(Ch2, Id); (* Sends the Voter's Id to the Bulletin Board. *) in( Ch2, Ks:bitstring); (* Receives the associated Voter's keystore. *) let Skid = GetKey(SVK,Ks) in (* Retreives the associated Voter's private key. *) out(Ch2, CreateVote(Pkb,Id,J1,J2,pube(Skid),Skid)); (* Sends the ballot (ie. 'Vote') to the server. *) in( Ch2, (sRC'1:bitstring,sRC'2:bitstring)); (* Receives the short Return Codes from server. *) if ((sRC'1=sRC1) || (sRC'2=sRC1)) && ((sRC'1=sRC2) || (sRC'2=sRC2)) then (* Compares the short Return Codes. *) ( event Confirmed(SVK, J1,J2); out(Ch2, pRC(Skid,CCid)); (* The Confirm(Id,_,Skid,CCid) voter's method. *) in( Ch2, =sFCid); (* Voter checks the Finalization Code's value. *) event HappyUser(SVK, J1,J2) ) . (* Server -- The election server -- With infinitly iterated Finalization Code (ie. Finalization/ProcessConfirm) part. *) let Serv(Ch2:channel,InitData:bitstring,CTally:channel) = in(Ch2, Id:agentId); (* Retrieves Registration data for this Voter identifier Id *) let (Pkb:epkey,Ska:symkey,Pkc:spkey,Ks:bitstring,M:bitstring,CRF:bitstring) = GetServData(InitData,Id) in (* Provides Ks to the voting device, and asks for the ballot (alias 'vote') *) out(Ch2, Ks); in( Ch2, B:bitstring); let (E:bitstring, W1:int,W2:int, =pke(Id), P:bitstring) = B in (* Voting part -- the Ballot processing and confirmation followed by the Server *) let Ok1 = ProcessVoteCheck(Pkb,Id,B) in ( get bb(=Id,B2) in 0 else ( event InsertBB(Id,E); insert bb(Id,B); (* Add ballot to the Ballot Box 'bb'; InsertBB for enc. *) let sRC_Set = CreateRC(B,Ska,M) in (* Gets the set of RC; Blocks the process if this fails. *) ( out(Ch2, sRC_Set); !( in( Ch2, CM:int); let FCid:symkey = f(Ska,CM) in (* The ProcessConfirm(bb,Id,CM,Ska,Pkc,..) method. *) let sFCid:bitstring = dec(FCid, readFC(H(FCid),M)) in let Ok2 = Verify(Pkc,sFCid,CRF) in ( insert cb(Id,sFCid,CRF); event HasVoted(InitData,Id,B,sFCid,CRF); (* Add confirmation to the Confirmation Box 'cb'. *) out(Ch2, sFCid); out(CTally, (Id,B,sFCid,CRF)) (* Phase 1 -- Sends the ballot to the Tally. *) ) ) ) ) ) . (* 6. Second Phase -- The Tally after all votes are collected. *) (* Tally -- the election tally -- Honest voter's part : mix only two honest voters. *) free mix:channel [private]. let TallyH(CTally:channel,Skb:ekey,Pkc:spkey,Id1:agentId,Id2:agentId) = in(CTally, (=Id1,B1:bitstring,sFC1:bitstring,CRF1:bitstring)); in(CTally, (=Id2,B2:bitstring,sFC2:bitstring,CRF2:bitstring)); (* Validation of the Ballots in the bulletin board. *) let Ok1 = ProcessVoteCheck(pube(Skb),Id1,B1) in let Ok1b = Verify(Pkc,sFC1,CRF1) in let Ok2 = ProcessVoteCheck(pube(Skb),Id2,B2) in let Ok2b = Verify(Pkc,sFC2,CRF2) in if Id1 <> Id2 then let (E1:bitstring, W11:int,W12:int, =pke(Id1), P1:bitstring) = B1 in let (E2:bitstring, W21:int,W22:int, =pke(Id2), P2:bitstring) = B2 in (* MixNet Modeling -- The data to be mixed is sent concurrently on a specific channel *) out(mix, choice[E1,E2]) | out(mix, choice[E2,E1]) | in(mix, ME1:bitstring); in(mix, ME2:bitstring); (* Decrypting -- The mixed ciphers are opened and decrypted. *) let (t_int(v(J11)),t_int(v(J12))) = adec(Skb,ME1) in let (t_int(v(J21)),t_int(v(J22))) = adec(Skb,ME2) in (* Publishing -- The intruder receices the election's result. *) out(c, (J11,J12)); out(c, (J21,J22)) . (* Tally -- the election tally -- Dishonest (or other Honest) voter's part : tallied but unmixed. *) let TallyD(CTally:channel,Skb:ekey,Pkc:spkey,Id1:agentId,Id2:agentId) = in(CTally, (Id3:agentId,B3:bitstring,sFC3:bitstring,CRF3:bitstring)); (* Validation of the Ballots in the bulletin board. *) let Ok3 = ProcessVoteCheck(pube(Skb),Id3,B3) in let Ok3b = Verify(Pkc,sFC3,CRF3) in if Id1 <> Id3 && Id2 <> Id3 then let (E3:bitstring, W31:int,W32:int, =pke(Id3), P3:bitstring) = B3 in (* Decrypting -- The mixed ciphers are opened and decrypted. *) let (t_int(v(J31)),t_int(v(J32))) = adec(Skb, E3) in (* Publishing -- The intruder receices the election's result. *) out(c, (J31,J32)) . (* 7. Security properties *) (* Single-vote Property : Only one ballot is stored in the table for each agent Id -- Impossible with ProVerif, need thread exclusion. *) (* Moreover, the protocol specification we used did not ensure this property, which is implementation dependant. *) (* Remark : If we combine this prop with our cast-as-intended and tallied-as-cast proved properties, then the expected cast-as-intended *) (* and tallied-as-cast, with only one ballot, immediately follows. If however the single-vote property cannot be guarantied by *) (* the implementation, then the protocol is vulnerable: a dishonest voter's computer may cast multiple ballots concurrently so *) (* that one with other choices that the voter's ones is finally accepted. The simple table's tests do not prevent this behaviour. *) (* query Id:agentId, E1:bitstring, E2:bitstring; event(InsertBB(Id,E1)) && event(InsertBB(Id,E2)) ==> E1 = E2. *) (* 8. Main process -- initiates the election *) process (* Public output from Setup(..) -- Gives the election's parameters to the Intruder. *) out(c, pkb); out(c, pkc); (* Gives the honest voter's public data to the Intruder *) out(c, deltaId(svka)); out(c,pke(deltaId(svka))); out(c, deltaId(svkb)); out(c,pke(deltaId(svkb))); (* Roles for honest voter(s) -- one for Reachability, two for Observational Equivalence. *) Voter_Device(VoterData(svka,ska),choice[ja1,ja2],choice[ja2,ja1],c,pkb) | Voter_Device(VoterData(svkb,ska),choice[ja2,ja1],choice[ja1,ja2],c,pkb) (* Dishonest voter(s) : As many as possible for Reachability, need only one for Obervational equivalence. *) | !(new svki:password; out(c,svki); out(c, pke(deltaId(svki))); out(c,VoterData(svki,ska))) (* Bulletin Board (ie. Server) : is Honest for Reachability, but Dishonest for Observational Equivalence. *) | out(c,ServData(pkb,ska,skc)) (* The Tally phase -- only after the honest voters have voted. *) | TallyH(c,skb,pkc,deltaId(svka),deltaId(svkb)) | !TallyD(c,skb,pkc,deltaId(svka),deltaId(svkb))