Formal verification of cryptographic protocols
Process calculus
Michael Backes (Saarland University) et. al.
an abstraction of secure multi-party computations in the applied π-calculus
RChain Casper in pi-calculus (2015)
Draft paper Formally introducing Casper by Vlad and Lucius Meredith Proverif
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
Joseph Y. Halpern (Cornell University), Rafael Pass (Cornell University)
Yoichi Hirai
Gustavo Betarte et al.
Coq based on Toychain and a library for elliptic curve Model checking
Lung-Chen Huang, Naipeng Dong, Guangdong Bai, Siau Cheng Khoo, Jin Song Dong
Examination of double spending in UPPAAL
Description of the Bitcoin Protocol in UPPAAL
BIP Framework, Statistical Model Checking
NuSMV
Game-based
Basics
Giancarlo Bigi, et al.
Andreas Lochbihler, S. Reza Sefidgar, David Basin, Ueli Maurer (ETH Zürich)
Uncategorized
RANDAO
Runtime Verification
Rewriting logic w/ Maude
Probablistic Rewriting
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
Plasma
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