Formal analysis of the Belenios VS protocol – Verifiability – 06_ROGUE_VOTING_SERVER

(* ROGUE VOTING SERVER------------------------------------------------------- *)
let     Rogue_Voting_Server(server_channel:key,public_channel:key) =
        new     ack:rand;
        out     (public,server_channel);
        in      (public,message:bitstring);
        let     (
                (n:name,pwd_n:bitstring,spk_n:spkey,val_n:bitstring),
                (ballot:bitstring,signature:bitstring)
                )
                = dec(message,server_channel) 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
        then    (
                event   GOING_TO_TALLY(n,spk_n,ballot,adec(ballot,sk_e));
                (* 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,enc((n,pwd_n,spk_n,ack),public_channel));
                out     (public,(spk_n,ballot,signature))
                )
	else
		(
		0
		)
        .