Formal analysis of the Belenios VS protocol – Verifiability – 08_MAIN

(* MAIN PROCESS-------------------------------------------------------------- *)
process (
                (
                out     (public,(sk_e,pk_e))
                )
        |
        !       (
                new     n:name;
                $PASSWORD
                )
        |
        !       (
                in      (public, n:name);
                new     voting_sheet_channel:key;
                new     voting_device_channel:key;
                new     server_channel:key;
                new     public_channel:key;
                $AUDITING_CHANNEL
                        (
                        $REGISTRAR
                        |
                        $VOTER_A
                        $VOTING_SHEET_AUDIT_PIPE
                        $VOTING_SHEET_AUDIT
                        |
                        $VOTING_DEVICE
                        |
                        $VOTING_SERVER
                        )
                )
        |
        !       (
                in      (public, n:name);
                new     voting_sheet_channel:key;
                new     voting_device_channel:key;
                new     server_channel:key;
                new     public_channel:key;
                $AUDITING_CHANNEL
                        (
                        $REGISTRAR
                        |
                        $VOTER_B
                        $VOTING_SHEET_AUDIT_PIPE
                        $VOTING_SHEET_AUDIT
                        |
                        $VOTING_DEVICE
                        |
                        $VOTING_SERVER
                        )
                )
        |
        !       (
                in      (public,server_channel:key);
                in      (public,public_channel:key);
                $VOTING_SERVER
                )
        |
        !       (
                in      (public,n:name);
                new     voting_sheet_channel:key;
                        (
                        $REGISTRAR
                        |
                        Rogue_Voter(voter_registration(n),voting_sheet_channel)
                        )
                )
        )