Formal analysis of the Belenios VS protocol – Verifiability – 00_SETUP

(* 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.
type status.


(* 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.

(* H = Honest Voter, C = Corrupted Voter------------------------------------- *)
free H:status.
free C:status.


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


(* EVENTS-------------------------------------------------------------------- *)
(* The events names respect our notation------------------------------------- *)

(* The voter has their voting material--------------------------------------- *)
event VOTER(name,spkey,status).

(* The voter voted----------------------------------------------------------- *)
event VOTE(name,bitstring,rand).

(* The voter verified their vote appears on the Public Bulletin Board-------- *)
event VERIFIED(name,bitstring).

(* The ballot is going to be tallied----------------------------------------- *)
event GOING_TO_TALLY(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)
 ).

reduc forall message:bitstring,pubk:pkey,sp:spkey,r:rand,s:rand;
 get_rand (
 aenc(message,pubk,sp,r,s)
 )
 = (r,s)
 [private].


 
 
(* 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.