A formal security analysis of Blockchain voting
summary
Formal Coq development models the Open Vote Network and proves provably functionally correct behavior plus cryptographically secure properties: self‑tallying, maximum ballot secrecy (IND‑CPA style), and dispute‑freedom. The pipeline uses ConCert and SSProve to formalize probabilistic, stateful games and Sigma/OR constructions (including the Fiat‑Shamir transform), then extracted to Rust and Lego for Concordium/Tezos deployments. The smart contract implementation is machine‑generated and verified end‑to‑end; extracted Rust is non‑idiomatic and slower, so embedding via hex provides automatic refinement to imperative code.
AI-written summary · about
chapters (15)
- 0:00Blockchain voting analysis intro
- 1:07Legal and formal verification
- 3:14Blockchain and voting link
- 5:01Open Vote Network overview
- 7:11Security properties needed
- 8:56Concert verification framework
- 10:23Rust extraction
- 12:11Proving Open Vote Network
- 13:35SSProof system
- 15:21Zero-knowledge proofs
- 16:47Ballot secrecy verification
- 17:29Rust in HACL*
- 19:19Verified smart contracts summary
- 20:03ElectionGuard collaboration
- 21:20Q&A: Implementation vs bugs
related talks
42mBeyond Blockchain: Convergent Consensus
43mAll Together Now: An Introduction to Distributed Consensus
24mAutomated game-theoretic security analysis of blockchain protocols
34mProvably Secure Blockchain Protocols and Applications to Secure Computation
01h 02mBlockchain is Cyberpunk
02h 44mBlockchain consensus mechanisms
20mVerifiable Elections—Now Is the Time
41mSecurely Scaling Decentralized Governance