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

(* HONEST VOTING SHEET AUDIT------------------------------------------------- *)
let     Honest_Voting_Sheet_Audit(audit_channel:key) =
        in      (public,message:bitstring);
        
        (* The auditing device verifies the ballot matches the vote it is suppos
        ed to encrypt and sign and answers true if it does------------------- *)
        let     (
                spk_n:spkey,
                v:vote,
                vote_v:bitstring,r:rand
                )
                = dec(message,audit_channel) in
        if      aenc(tc_vote(v),pk_e,spk_n,r,r) = vote_v
        then    (
                out     (public,enc((v,true),audit_channel))
                )
        else    (
                0
                )
        .