Formal verification of cryptographic protocols
See also Universal Composability: usecases
Process calculus
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 Blog post, GitHub
See in Formal Verification of Consensus Algorithms
RChain Casper in pi-calculus (2015)
Slide
Draft paper Formally introducing Casper by Vlad and Lucius Meredith
Proverif
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*
Mathematical logic
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
Yoichi Hirai
Based on An intuitionistic epistemic logic for asynchronous communication.
See in Atomic Cross-chain Swap
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol (short paper)
Gustavo Betarte et al.
Coq based on Toychain and a library for elliptic curve
Use QuickChick
Model checking
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
NuSMV
Game-based
Basics
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)
AFP
Tutorial
Uncategorized
RANDAO
Runtime Verification
GitHub Repo
Rewriting logic w/ Maude
Probablistic Rewriting
Automated Verification of Electrum Wallet
INRIA
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
Raiden
Isabelle proofs for settlement contract
Plasma
More Viable Plasma
see 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
SimplePlasma.v GitHub
#Formal_Verification