Formal analysis of the Belenios VS protocol – Verifiability – 02_HONEST_VOTER_NO_AUDIT

(* HONEST VOTER-------------------------------------------------------------- *)
(* VOTER DOES NOT AUDIT VOTING SHEET----------------------------------------- *)
let Honest_Voter_A_no_audit(n:name,voting_sheet_channel:key,voting_device_channel:key,public_channel:key) =
 (* vote_id is used to prevent revoting------------------------------- *)
 new vote_id:rand;
 
 (* The voter receives the Voting Sheet------------------------------- *)
 in (public, message:bitstring);
 let (
 spk_n:spkey,val_n:bitstring,
 =A,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand),
 b:vote,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)
 )
 = dec(message,voting_sheet_channel) in
 
 (* The voter is then associated to the voting credential------------- *)
 event VOTER(n,spk_n,H);
 
 (* The voter scans their vote through the voting device-------------- *)
 event VOTE(n,tc_vote(A),vote_id);
 out (public, enc((

n,password(n),
 spk_n,val_n,
 vote_a,sign_a),

voting_device_channel));

in (public,ack:bitstring);
 let (
 =n,=password(n),=spk_n,r:rand
 )
 = dec(ack,public_channel) in
 
 (* The voter verifies their vote appears on the Public Bulletin Board *)
 get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in
 event VERIFIED(n,tc_vote(A))
 .

let Honest_Voter_B_no_audit(n:name,voting_sheet_channel:key,voting_device_channel:key,public_channel:key) =
 (* vote_id is used to prevent revoting------------------------------- *)
 new vote_id:rand;
 
 (* The voter receives the Voting Sheet------------------------------- *)
 in (public, message:bitstring);
 let (
 spk_n:spkey,val_n:bitstring,
 a:vote,(vote_a:bitstring,sign_a:bitstring,ra:rand,sa:rand),
 =B,(vote_b:bitstring,sign_b:bitstring,rb:rand,sb:rand)
 )
 = dec(message,voting_sheet_channel) in
 
 (* The voter is then associated to the voting credential------------- *)
 event VOTER(n,spk_n,H);
 
 (* The voter scans their vote through the voting device-------------- *)
 event VOTE(n,tc_vote(B),vote_id);
 out (public, enc((

n,password(n),
 spk_n,val_n,
 vote_b,sign_b),

voting_device_channel));

in (public,ack:bitstring);
 let (
 =n,=password(n),=spk_n,r:rand
 )
 = dec(ack,public_channel) in
 
 (* The voter verifies their vote appears on the Public Bulletin Board *)
 get BULLETIN_BOARD(m,=spk_n,rand_ballot,sign_rand_ballot) in
 event VERIFIED(n,tc_vote(B))
 .