Formal verification of cryptographic protocols
Universal Composability: usecases
Computationally Sound Abstraction and Verification of Secure Multi-Party Computations (2010)
Michael Backes (Saarland University) et. al.
an abstraction of secure multi-party computations in the applied π-calculus
Psi/Chi calculus, IOHK
Formal Verification of Consensus Algorithms
RChain Casper in pi-calculus (2015)
Formally introducing Casper by Vlad and Lucius Meredith
Verify-Your-Vote: A Verifiable Blockchain-based Online Voting Protocol
Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers
Nadim Kobeissi (INRIA Paris, Symbolic Software)
Ledger Design Language (LDL) is a modeling language for describing public ledgers.
The LDL compiler produces two outputs.
1. an applied-pi calculus symbolic model representing the public ledger as a protocol.
Using ProVerif, the protocol can be played against an active attacker, whereupon we can query for block integrity, authenticity and other properties.
2. a formally verified read/write API for interacting with the public ledger in the real world, written in the F*
A Knowledge-Based Analysis of the Blockchain Protocol
Joseph Y. Halpern (Cornell University), Rafael Pass (Cornell University)
Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap
An intuitionistic epistemic logic for asynchronous communication.
Atomic Cross-chain Swap
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol (short paper)
Gustavo Betarte et al.
Coq based on
and a library for elliptic curve
Model Checking Blockchain-based System: A Case Study (slide)
Lung-Chen Huang, Naipeng Dong, Guangdong Bai, Siau Cheng Khoo, Jin Song Dong
Modeling and Verification of the Bitcoin Protocol
Examination of double spending in UPPAAL
Description of the Bitcoin Protocol in UPPAAL
Formal verification of smart contracts based on users and blockchain behaviors models
BIP Framework, Statistical Model Checking
Model-Checking of Smart Contracts
Course: Game Theory in Formal Verification
Validation of Decentralised Smart Contracts through Game Theory and Formal Methods
Giancarlo Bigi, et al.
Formalizing Constructive Cryptography using CryptHOL
Andreas Lochbihler, S. Reza Sefidgar, David Basin, Ueli Maurer (ETH Zürich)
Rewriting logic w/ Maude
Automated Verification of Electrum Wallet
a formal modeling in ASLan++ of the twofactor authentication protocol used by the Electrum Bitcoin wallet.
an automatic analysis of the wallet and show that it is secure for standard scenarios in Dolev Yao model
Isabelle proofs for settlement contract
More Viable Plasma
Formal verification of More Viable Plasma
Models transactions and defines "exitable" TXOs
Proves safety and liveness properties about exitable TXOs
An attempt to verify Plasma MVP in Coq by pirapira