Formal analysis of the Belenios VS protocol – Vote Confidentiality – Voting server, voting device, authentication credentials compromised and voter does not audit the voting sheet

(* CORRUPTION SCENARIO------------------------------------------------------- *)

(* HONEST REGISTRAR---------------------------------------------------------- *)
(* NO LEAK OF VOTING SHEET--------------------------------------------------- *)
(* HONEST VOTER NO AUDIT----------------------------------------------------- *)
(* NO NEED FOR VOTING SHEET AUDIT PROCESS------------------------------------ *)
(* ROGUE VOTING DEVICE------------------------------------------------------- *)
(* ROGUE VOTING SERVER NO ROGUE REGISTRAR------------------------------------ *)
(* LOGIN-PWD STOLEN---------------------------------------------------------- *)

(* TYPES--------------------------------------------------------------------- *)
(* Since we do not use private channels to model secure network, we do that with
symmetric encryption, thus we need a type "key"------------------------------ *)
type key.

(* Asymmetric encryption types----------------------------------------------- *)
type skey.
type pkey.

(* Signature types----------------------------------------------------------- *)
type sskey.
type spkey.

(* Other types used in the protocol------------------------------------------ *)
type rand.
type name.
type vote.

(* NAMES--------------------------------------------------------------------- *)
(* We define a public channel------------------------------------------------ *)
free public:channel.

(* This name is used to generate the election asymmetric keys---------------- *)
free election:name.

(* Two possible votes-------------------------------------------------------- *)
free A:vote.
free B:vote.

(* Two honest voters--------------------------------------------------------- *)
free Eowyn:name.
free Mulan:name.

(* A private channel for the tally model------------------------------------- *)
free tally_channel:channel[private].

(* TABLES-------------------------------------------------------------------- *)
(* The Public Bulletin Board------------------------------------------------- *)
table BULLETIN_BOARD(name,spkey,bitstring,bitstring).


(* SYMMETRIC ENCRYPTION------------------------------------------------------ *)
(* To model secure channels-------------------------------------------------- *)
fun enc(bitstring,key):bitstring.

reduc forall message:bitstring,k:key;
 dec(enc(message,k),k) = message.


 
 
(* RANDOMIZED ASYMMETRIC ENCRYPTION------------------------------------------ *)
fun sk(name):skey [private].
fun pk(skey):pkey.
fun aenc(bitstring,pkey,spkey,rand,rand):bitstring.

reduc forall message:bitstring, seck:skey, spubk:spkey, r:rand, t:rand;
 adec(aenc(message,pk(seck),spubk,r,t), seck) = message.


 
 
(* RANDOMIZED SIGNATURE------------------------------------------------------ *)
fun spk(sskey):spkey.
fun sign(bitstring, pkey, sskey, rand, rand):bitstring.

reduc forall message:bitstring, pubk:pkey, sseck:sskey, r:rand, t:rand, s:rand, u:rand;
 verify(aenc(message,pubk,spk(sseck),r,t), sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u),spk(sseck)) = true.


 
 
(* RANDOMIZATION------------------------------------------------------------- *)
reduc forall message:bitstring, pubk:pkey, sseck:sskey,
 r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
 randomize_aenc (
 aenc(message,pubk,spk(sseck),r,v),
 sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),
 pubk, spk(sseck),t,u
 )
 = aenc(message,pubk,spk(sseck),r,t).

reduc forall message:bitstring, pubk:pkey, sseck:sskey,
 r:rand, s:rand, t:rand, u:rand, v:rand, w:rand;
 randomize_sign (
 aenc(message,pubk,spk(sseck),r,v),
 sign(aenc(message,pubk,spk(sseck),r,v),pubk,sseck,s,w),
 pubk,spk(sseck),t,u
 )
 = sign(aenc(message,pubk,spk(sseck),r,t),pubk,sseck,s,u) .

letfun randomize (
 ballot:bitstring,signature:bitstring,
 pke:pkey,spk_n:spkey,r:rand,s:rand
 )
 = (
 randomize_aenc(ballot,signature,pke,spk_n,r,s),
 randomize_sign(ballot,signature,pke,spk_n,r,s)
 ).


(* ELECTION SETUP------------------------------------------------------------ *)
(* The election asymetric pair of keys--------------------------------------- *)
letfun sk_e = sk(election).
letfun pk_e = pk(sk(election)).

(* The password associated to a voter ID------------------------------------- *)
fun password(name):bitstring [private].

(* The voter ID. To check if a voter ID is a valid one, is_registered is used *)
fun voter_registration(name):name [private].
reduc forall n:name;
 is_registered(voter_registration(n)) = true.


 
 
(* REGISTRAR FUNCTIONS------------------------------------------------------- *)
(* Type converting function-------------------------------------------------- *)
fun tc_vote(vote):bitstring [data, typeConverter].

(* A voting sheet generation function. It takes a vote and a signature key in in
put and outputs the encrypted vote, its signature and the nonces (rand) used to 
generate the ballot---------------------------------------------------------- *)
letfun voting_sheet(v:vote,ssk:sskey) =
 new r:rand;
 new s:rand;
 (
 aenc (tc_vote(v),pk_e,spk(ssk),r,r),
 sign (aenc(tc_vote(v),pk_e,spk(ssk),r,r),pk_e,ssk,s,s),
 r, s
 )
 .
 
(* The list of valid credentials generated by the registrar is public. The funct
ion valid generates a certificate for the public signature key (it can only be u
sed by the registrar) and is_valid is run to check if a public credential was in
deed produced by the registrar----------------------------------------------- *)
fun valid(spkey):bitstring [private].
reduc forall s:spkey;
 is_valid(valid(s),s)=true.


(* HONEST REGISTRAR---------------------------------------------------------- *)
(* The honest registrar process with rogue voters. It produces the voting sheets
and outputs them on the public channel since voters are rogue---------------- *)
let Honest_Registrar_Rogue_Voter() =
 new ssk:sskey;
 out (public, (
 spk(ssk),valid(spk(ssk)),
 A,voting_sheet(A,ssk),
 B,voting_sheet(B,ssk)))
 .

(* HONEST VOTER-------------------------------------------------------------- *)
(* VOTER DOES NOT AUDIT VOTING SHEET AND CASTS BALLOT WITH ROGUE VOTING DEVICE*)
let Honest_Voter_no_audit(n:name,v:vote) =
 (* Freshly generated nonce used during the process. They are generated a
 t the beginning of the process to help ProVerif---------------------- *)
 new ssk_n:sskey;
 new rv:rand;
 new sv:rand;
 
 (* We model the registrar process alltogether with the voter process sin
 ce it is a honest entity. The public signature credentials are publicly 
 output--------------------------------------------------------------- *)
 let spk_n = spk(ssk_n) in
 let val_n = valid(spk(ssk_n)) in 
 out (public,(spk_n,val_n));
 
 (* Since the registrar is honest, the ballot scanned by the voter matche
 s her voting choice-------------------------------------------------- *)
 let vote_v = aenc(tc_vote(v),pk_e,spk_n,rv,rv) in
 let sign_v = sign(vote_v,pk_e,ssk_n,sv,sv) in
 
 (* For the election tally model, we need to send the association of the 
 voter and her credential to the process modeling the tally----------- *) 
 out (tally_channel, (n,spk_n));
 
 (* The voting device is rogue so the ballot is publicly output along the
 voter's authentication credentials----------------------------------- *) 
 out (public, ((n,password(n),spk_n,val_n),(vote_v,sign_v)));
 
 (* The voter verifies her vote appears on the Public Bulletin Board-- *) 
 get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in
 out (tally_channel, (n,spk_n))
 .

(* ROGUE VOTING SERVER NO ROGUE REGISTRAR------------------------------------ *)
let Rogue_Voting_Server() =
 in (public,message:bitstring);
 let (
 (n:name,pwd_n:bitstring,spk_n:spkey,val_n:bitstring),
 (ballot:bitstring,signature:bitstring)
 )
 = message in
 
 (* Since the Bulletin Board can be audited by anyone, we made the assump
 tion that at least all displayed ballots are correctly signed-------- *)
 if (
 verify(ballot,signature,spk_n) = true
 && is_valid(val_n,spk_n)=true
 )
 then (
 (* The rogue voting server does not proceed to any verification
 other than the signature and publish all ballots it gets----- *)
 insert BULLETIN_BOARD(n,spk_n,ballot,signature);
 out (public,(spk_n,ballot,signature))
 )
 .

(* TALLY PROCESS------------------------------------------------------------- *)
(* The tally process is separated into two subprocesses. One that only tally the
ballots (Tally_Honest_Voter) and the other one that tally all ballots coming fro
m all voters except our two honest ones (Tally)------------------------------ *)

let Tally_Honest_Voter() =
 (* The association between a honest voter and her public verification ke
 y is made------------------------------------------------------------ *)
 in (tally_channel, (=voter_registration(Eowyn),spk_Eowyn:spkey));
 in (tally_channel, (=voter_registration(Mulan),spk_Mulan:spkey));
 if spk_Eowyn <> spk_Mulan
 
 (* The tallying authority retrieves the ballots registered with our two 
 honest voters' public signature verification key--------------------- *)
 then (
 get BULLETIN_BOARD(m_E,=spk_Eowyn,rand_ballot_Eowyn,sign_rand_ballot_Eowyn) in
 get BULLETIN_BOARD(m_M,=spk_Mulan,rand_ballot_Mulan,sign_rand_ballot_Mulan) in
 
 (* We model a mixnet ---------------------------------------- *)
 new mixnet:channel;
 (
 (
 out (mixnet,choice[rand_ballot_Eowyn,rand_ballot_Mulan])
 |
 out (mixnet,choice[rand_ballot_Mulan,rand_ballot_Eowyn])
 )
 |
 in (mixnet,b1:bitstring);
 in (mixnet,b2:bitstring);
 out (public,(adec(b1,sk_e),adec(b2,sk_e)))
 )
 )
 .
 
let Tally(spk_n:spkey) =
 (* The association between a honest voter and her public verification ke
 y is made------------------------------------------------------------ *)
 in (tally_channel, (=voter_registration(Eowyn),spk_Eowyn:spkey));
 in (tally_channel, (=voter_registration(Mulan),spk_Mulan:spkey));
 
 in (public, (=spk_n,b_n:bitstring,sign_n:bitstring));
 
 (* If the signature verification key used to cast the ballot is differen
 t from our honest voters' one, the ballot is simply decrypted and public
 ly output------------------------------------------------------------ *)
 if (
 spk_n <> spk_Eowyn
 && spk_n <> spk_Mulan
 && verify(b_n,sign_n,spk_n) = true
 )
 then (
 out (public, adec(b_n,sk_e))
 )
 . 
 
 
(* MAIN PROCESS-------------------------------------------------------------- *)
process (
 (
 out (public,pk_e);
 out (public,voter_registration(Eowyn));
 out (public,voter_registration(Mulan))
 )
 |
 out (public, password(voter_registration(Eowyn)));
 out (public, password(voter_registration(Mulan)))
 |
 ! (
 new n:name;
 out (public, (n,voter_registration(n),password(voter_registration(n))))
 )
 |
 ! (
 Rogue_Voting_Server()
 )
 |
 ! (
 Honest_Registrar_Rogue_Voter()
 )
 |
 (
 Honest_Voter_no_audit(voter_registration(Eowyn),choice[A,B])
 )
 |
 (
 Honest_Voter_no_audit(voter_registration(Mulan),choice[B,A])
 )
 |
 (
 Tally_Honest_Voter()
 )
 |
 ! (
 in (public,spk_n:spkey);
 Tally(spk_n)
 )
 )