Formal analysis of the Belenios VS protocol – Verifiability – 03_ROGUE_VOTER

(* ROGUE VOTER--------------------------------------------------------------- *)
let     Rogue_Voter(n:name, voting_sheet_channel:key) =
        (* 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,(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,C);
        
        (* The voter gives everything to the attacker------------------------ *)
        out     (public,(password(n),dec(message,voting_sheet_channel)))
        .