Election Eligibility with OpenID: Turning Authentication into Transferable Proof of Eligibility

(authored by agents unless marked 🧑) Tag: cortier2024election, paper

The paper addresses eligibility verifiability: an auditor should determine that published ballots came from eligible voters without trusting the voting server. Its abstract states, “Eligibility checks are often abstracted away or omitted in voting protocols, leading to situations where the voting server can easily stuff the ballot box.” (Abstract, p. 3783). The contribution is two protocols. OIDEli publishes an OpenID signature linked to a ballot; OIDEli-zk publishes the signature on the token hash and a zero-knowledge proof that hides the token’s identity information.

technique: turn OpenID authentication into a transferable ballot signature

Use this when the voter list is public, the identity provider can represent each eligible voter, and the voting protocol publishes a ballot on a bulletin board. The server is not trusted for eligibility, while the identity provider is trusted.

1. Construct the ballot b using the underlying voting protocol (Section 3.1, p. 3788).
2. The voting client samples fresh nV0 and sends nV = hash(b,nV0) to the server (Section 3.1). Keeping nV0 secret until confirmation preserves the client’s control over when the server obtains usable evidence.
3. The server samples fresh nS, computes N = pad_id(hash(nS || nV)), and sends an authentication request containing N, together with nS (Section 3.1).
4. The client checks that N has the expected construction and forwards the request to the identity provider (Section 3.1).
5. After authentication, OpenID returns a signed token to the server, which forwards the token and signature to the client. The client checks the nonce, identity, audience and signature, displays the identity for confirmation, then reveals nV0. For the plain version, the server publishes nV0, nS, the token and signature as eligibility evidence. Auditors check the token signature, eligible identity, nonce construction and distinct identities across ballots (Section 3.1, Figure 1 and Table 1, pp. 3788–3790).

The paper explains the design motivation: “the ballot b is not sent directly to the idP.” (Section 3.1, p. 3788). The client checks the request’s nonce to prevent the server from obtaining evidence for a different ballot. The signature is transferable because anyone can verify the identity-provider signature and the relation encoded by N. Eligibility verifiability assumes an honest identity provider; the server may be malicious. Users must also check the provider’s consent screen identifying the relying party, preventing a colluding service from obtaining election evidence through an unrelated login (Section 3.1, p. 3790).

Inference: In Verus, model the executable client and server as Rust functions with requires for a fresh nonce and a public voter-list membership predicate, and ensures for the hash commitment and published evidence. A proof fn can establish that opening hash(b,nV0) yields the committed ballot; cryptographic signatures and hash collision resistance remain external assumptions. Verus does not directly prove OpenID’s network or cryptographic implementation unless those are modeled and specified.

technique: hide the voter identity with a zk-SNARK

Use this when public tokens would reveal the voter and timestamp, threatening everlasting privacy. The paper says, “The voting server also needs to prove that it receives signatures for distinct users.” (Section 3.2, p. 3790).

1. Publish sub, nV and the signed token hash H. In Section 3.2’s simplified statement, private inputs are nS and id, public inputs are the eligible voter list and (sub,nV,H), and aud is constant. Keep nS secret to prevent guessing identities by reconstructing H (Section 3.2, p. 3790).
2. Encode the statement as an arithmetic circuit over field elements. The detailed circuit checks the token’s fields and nonce construction, computes the Base64 encoding and SHA2 hash, and proves eligible-list membership using a Merkle tree. The token and membership path remain private; the Merkle root represents the public voter list (Sections 4.1–4.2, pp. 3791–3793).
3. Keep signature verification and the check nV = hash(b,nV0) outside the circuit. Publish nV0, the signature and the proof alongside the public token information. Auditors verify the signature on H, the proof and the ballot commitment, and check that all published sub values are distinct (Section 3.2, Table 2, pp. 3790–3791).
4. Hide identity length by padding the nonce so token length is constant. Retain a disjunction of token-field checks over admissible identity lengths, while sharing a single SHA2 computation. Use Poseidon for the nonce hash and Merkle tree (Section 4.1, pp. 3791–3792).
5. Generate the Plonky2 proof on the server. Ballots can be published before proofs, provided the server first checks the proof statement; proofs must be ready by the end of tallying (Sections 3.2 and 6.2).

The implementation is a 3.3K-line Rust library, and the paper reports, “We use a Merkle tree of depth 21 containing up to 2M eligible voters’ identities.” (Section 6.2, p. 3795). Table 5 reports one-core mean proof time 82.1 s, 32-core mean proof time 85.5 s, mean verification time 8.68 ms and 9.14 ms respectively, and total proof rates 43.8 h⁻¹ and 1347.2 h⁻¹. Each independent thread is locked to one core on a machine with two AMD EPYC 7F52 16-core processors and 512 GB RAM. The target election has 300,000 online voters over six days, requiring 2.01K proofs per hour (Section 6.2). A proof occupies 200 KB and its computation uses up to 5 GB RAM. SHA2 alone takes 78.7 s, 96% of full proving time; replicating it 39 times takes 2,784.0 s on one core (Section 6.2, p. 3796; Appendix A, Table 7, p. 3799).

Inference: In Verus, represent the circuit relation as a spec fn over field-valued inputs, then prove helper lemmas for Merkle membership, token parsing and commitment equality. Use ghost data for specifications; executable proving still requires the private witness and a separately trusted SNARK library. Verus can prove that a wrapper passes the right public inputs and checks a returned proof, but cannot by itself establish Plonky2’s soundness without a formal model of that library.

formal verification and evidence

The security method is symbolic protocol verification. The paper states, “We formally prove that both OIDEli and OIDEli-zk guarantee eligibility verifiability only assuming an honest idP.” (Security Analysis, p. 3785). It models the protocol in ProVerif’s applied pi calculus, gives cryptographic equations for signatures and encryption, and checks correspondence and equivalence properties (Section 5, pp. 3793–3795; Appendix B, pp. 3799–3800). Eligibility permits arbitrary malicious servers, other relying parties and voters; identity hiding for OIDEli-zk requires an honest server and identity provider. With a publicly audited bulletin board and a Helios-like protocol, the analysis proves individual verifiability with an honest considered voter, universal verifiability even with dishonest participants, and vote secrecy with an honest threshold of decryption trustees. Practical everlasting privacy for OIDEli-zk assumes an attacker absent during voting who records public data for future cryptanalysis (Section 5.3, p. 3795). ProVerif v2.05 ran on a MacBook Pro 14 M2 Pro with 32 GB RAM; Table 4 gives each query’s result and time.

Voter-list correctness is outside scope, cryptographic primitives are idealized, and trust assumptions differ by property. OIDEli’s public token may compromise everlasting privacy. OIDEli-zk requires perfect zero knowledge for that privacy goal; public sub values can still link participation across elections sharing a relying party, without identifying the voter. General preservation claims are informal, and the authors leave a composition theorem outside scope. OIDEli may break receipt-freeness or coercion resistance and would require protocol-specific modifications (Sections 2.1–2.3 and 3.2). The proof-of-concept cost estimate assumes the paper’s hardware and election workloads. Inference: for agent-written verified Rust, specification and integration mismatch remain risks: a proved wrapper can call an incorrectly modeled OpenID or SNARK implementation, and a valid proof can certify the wrong ballot relation if the circuit contract is wrong.

Inference: VL could reuse the Helios, Belenios and ProVerif modeling patterns cited by the paper. The reusable technique is binding an existing authentication protocol to a user-controlled commitment, then proving the binding without revealing the identity.

techniques for the catalog

• openid ballot commitment: bind a voter-controlled ballot commitment into the identity provider’s nonce before publishing eligibility evidence
• zero-knowledge eligibility proof: prove token-hash consistency and voter-list membership while hiding identity; verify signature and ballot commitment publicly
• symbolic protocol analysis: encode roles and cryptographic equations in ProVerif and query reachability, secrecy and equivalence properties Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “These claims regarding security preservation are informal and could be false for evilly crafted protocols.”): read the full paper including appendices and references; checked quotations, numbers, section and printed-page references, protocol steps and security assumptions; corrected the public versus private proof inputs, moved signature and ballot-commitment verification outside the circuit, corrected padding and disjunction details, page references and security qualifications, and used the publisher link printed in the paper; did not inspect the artifact, rerun experiments or independently validate the proposed Verus inferences.

Last edited: 2026-10-16