fstar-protocol-equivalence

⚠️ Work in progress. This is an active, unfinished formalization. Expect things to move and break.

An F* framework for proving protocol indistinguishability under interaction with a symbolic active (Dolev-Yao style) adversary. Protocol indistinguishability under a given adversary (also called test equivalence, or t_equivalence in this development) can be proven by exhibiting an observational bisimulation between the two protocols. When the protocols are a "real" protocol and an ideal specification composed with a simulator protocol, proving this equivalence is the symbolic analogue of a simulation-based proof of cryptographic security.

What's here

The core library defines protocols as labelled transition systems with a few side conditions, an adversary (or tester) that derives new terms from its knowledge, static and testing equivalence, and an observational-bisimulation proof technique that gives sufficient conditions for testing equivalence. Two examples are given:

• Secure Message Delivery (SMD) — examples/secure_message_delivery/. Uses symmetric encryption to realize secure fixed two-party message delivery.
• NSL Mutual Authentication (MA) — examples/nsl_mutual_authentication/. Shows an adaptation of the Needham-Schroeder-Lowe protocol realizes two-party mutual authentication under static corruption.

Each example proves that its implementation realizes its ideal functionality, stated as a testing-equivalence theorem (smd_t_equivalence, ma_t_equivalence) established via the observational-bisimulation framework.

Building

Requires fstar.exe on your PATH (or set FSTAR_HOME).

Verify (type-check and prove) everything:

make -j <num-cores>

To verify a single file:

fstar.exe --cache_dir output --odir output \
  --include helpers \
  --include examples/secure_message_delivery \
  --include examples/nsl_mutual_authentication \
  --include output \
  --already_cached 'Prims' \
  MyFile.fst

Add a .fst.config.json file to configure the F* LSP server for interactive/IDE use.

Repository layout

Core library (root)

File	Purpose
SymbolicTypes	Foundational types: term, world (Impl/Ideal), knowledge, session/channel IDs
SencTerms	Concrete term type for symmetric encryption (used by SMD)
AencTerms	Concrete term type for asymmetric encryption (used by NSL MA)
Adversary	Typeclass for the adversary interface: derivation, derive, monotonicity
AdversarySenc / AdversaryAenc	Symmetric- and asymmetric-encryption adversary instances
StaticEquivalence	indistinguishable and statically_equivalent relations
Protocol	Protocol labelled transition systems: state, label, validity constraints
TestedSystem	Tested system = protocol ∥ adversary; adds adversary knowledge and Input labels
TestEquivalence	Testing equivalence: multi_transitions, t_equivalence
ObservationalBisimulation	Bisimulation framework and the theorem that bisimulation implies testing equivalence

Examples

Both examples/secure_message_delivery/ and examples/nsl_mutual_authentication/ follow the same layout: an implementation world, an ideal world, invariants, a binding of protocols to the adversary (*.TestedProtocols), and a four-module bisimulation proof (Relation → Witnesses → Proof).

Helpers (helpers/)

Multiset (Bag), partition/equivalence-relation typeclasses, and small extensions to F*'s Bijection, PartialMap, and Set libraries.

Metatheory

The metatheory of the framework is not fully mechanized in F* yet. Instead the key ObservationalBisimulation results are mechanized in a companion Lean development and admitted here.