Formal analysis of the Belenios VS protocol – Verifiability – 04_ROGUE_VOTING_SHEET_AUDIT

(* ROGUE VOTING SHEET AUDIT-------------------------------------------------- *)
let Rogue_Voting_Sheet_Audit(audit_channel:key) =
 (* The rogue auditing device always answers true--------------------- *)
 in (public,message:bitstring);
 let (
 spk_n:spkey,
 v:vote,
 vote_v:bitstring,r:rand
 )
 = dec(message,audit_channel) in
 out (public,(dec(message,audit_channel),audit_channel));
 out (public,enc((v,true),audit_channel))
 .