Formal analysis of the Belenios VS protocol – Verifiability – 07_SECURITY_PROPERTIES

(* SECURITY PROPERTIES------------------------------------------------------- *)
(* HONEST VOTE CONSISTENCY--------------------------------------------------- *)
query   n:name,v:bitstring,k:rand;
        event(VERIFIED(n,v)) ==> event(VOTE(n,v,k)).

(* CAST AS INTENDED (ID)----------------------------------------------------- *)
query   ID:name,v:bitstring,
        b:bitstring,r:rand,
        spk_n:spkey,spk_1:spkey,spk_2:spkey;
        event(GOING_TO_TALLY(ID,spk_n,b,v))
        ==>
        (
                (
                event(VOTER(ID,spk_1,C))
                )
        ||
                (
                event(VOTER(ID,spk_2,H))
                &&
                event(VOTE(ID,v,r))
                )
        ).

(* TALLIED AS CAST (ID)------------------------------------------------------ *)
query   ID:name,v:bitstring,
        v1:bitstring,v2:bitstring,r1:rand,r2:rand,
        spk_n:spkey,b:bitstring;
        event(VERIFIED(ID,v))
        ==>
        (
        event(GOING_TO_TALLY(ID,spk_n,b,v))
        ||
                (
                event(VOTE(ID,v1,r1))
                &&
                event(VOTE(ID,v2,r2))
                &&
                r1  r2
                )
        ).

(* CAST AS INTENDED (CRED)--------------------------------------------------- *)
query   ID:name,CRED:spkey,v:bitstring,
        b:bitstring,r:rand,
        n1:name,n2:name;
        event(GOING_TO_TALLY(n1,CRED,b,v))
        ==>
        (
                (
                event(VOTER(n2,CRED,C))
                )
        ||
                (
                event(VOTER(ID,CRED,H))
                &&
                event(VOTE(ID,v,r))
                )
        ).

(* TALLIED AS CAST (CRED)---------------------------------------------------- *)
query   ID:name,v:bitstring,
        v1:bitstring,v2:bitstring,r1:rand,r2:rand,
        n:name,CRED:spkey,b:bitstring;
        event(VERIFIED(ID,v))
        ==>
        (
                (
                event(VOTER(ID,CRED,H))
                &&
                event(GOING_TO_TALLY(n,CRED,b,v))
                )
        ||
                (
                event(VOTE(ID,v1,r1))
                &&
                event(VOTE(ID,v2,r2))
                &&
                r1  r2
                )
        ).