Formal analysis of the Belenios VS protocol – Verifiability – 01_ROGUE_REGISTRAR

(* ROGUE REGISTRAR----------------------------------------------------------- *)
let Rogue_Registrar(voting_sheet_channel:key,a:vote,b:vote) =
 (* Since the Rogue Registrar is under the control of the attacker, it ge
 nerates the signature key and gives it to the attacker as well as it giv
 es the control of the channel used to transmit the voting sheets----- *)
 new ssk:sskey;
 out (public,(voting_sheet_channel,ssk,spk(ssk),valid(spk(ssk))))
 .