Formal verification of cryptographic protocols

See also Universal Composability: usecases

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

See in Atomic Cross-chain Swap

Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol (short paper)

Gustavo Betarte et al.

Use QuickChick

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