Formal analysis of the Belenios VS protocol – Verifiability – 05_ROGUE_VOTING_DEVICE

(* ROGUE VOTING DEVICE------------------------------------------------------- *)
let Rogue_Voting_Device(voting_device_channel:key,server_channel:key) =
 in (public,message:bitstring);
 let (
 n:name,pwd_n:bitstring,
 spk_n:spkey,val_n:bitstring,
 vote_v:bitstring,sign_v:bitstring
 )
 = dec(message,voting_device_channel) in
 (* The rogue voting device gives everything to the attacker---------- *)
 out (public,(dec(message,voting_device_channel),server_channel))
 .