A report on a tool still in development \E2\80\94 the architecture we chose, the trade-offs we made, and why we believe this direction has a future.
This article is not a product announcement. It is a report on how we are building a tool still in progress. The architecture is settled, the key decisions are made, the code is being written. But the final form is still ahead \E2\80\94 and that is exactly why now is the right time to talk about where we are going and why.
The project is under active development. What follows describes what we are building toward, not what ships today. But every architectural decision in this article is already implemented or in active development. We are reporting concrete progress, not speculating.
The problem we are solving
ProVerif and Tamarin are excellent tools. They solve vulnerability detection well: accept a protocol description, build an attacker model, check whether security properties hold. When they find an attack, they produce a trace \E2\80\94 a concrete sequence of steps the attacker takes.
And then the engineer is alone with that trace. Writing a patch, verifying it blocks the attack, making sure the protocol still works \E2\80\94 all manual labor, all informal reasoning.
ProVerif and Tamarin do not repair protocols. They do not analyze quantum adversaries or side channels. And on real-world protocols \E2\80\94 TLS 1.3, Signal, WireGuard \E2\80\94 they run for hours. We are building a tool that closes all three gaps.
The vision
A protocol analyzer that accepts a description of a cryptographic protocol and its security properties, finds attacks when they exist, and generates a formally verified fix \E2\80\94 all without manual intervention. The tool should run fast enough to analyze real-world protocols in minutes, not hours. And it should cover attack surfaces that existing tools ignore.
This is not an incremental improvement over ProVerif or Tamarin. It is a different category of tool.
Automatic repair: the core capability
Existing tools stop at "attack found." The analyzer we are building continues: it generates a patch, verifies that the patch blocks the found attack, and checks that the protocol still satisfies its security properties.
The mechanism is Counterexample-Guided Protocol Synthesis (CEGPS), borrowed from program synthesis:
- The analyzer finds an attack trace.
- The repair module proposes modifications that could block this trace.
- The verifier checks each modification: does it block the attack, and does the protocol preserve its security properties.
- If a patch fails \E2\80\94 a counterexample is extracted, and the cycle repeats.
- From the set of verified patches, multi-objective optimization selects the best one.
Every proposed patch is formally verified. No "probably working" suggestions \E2\80\94 only fixes proven to block the attack. The repair module uses eight types of repair rules and multi-objective optimization considering security, performance cost, and protocol complexity.
The target is 10x to 50x speedup over existing tools on classical benchmarks. On real-world protocols \E2\80\94 TLS 1.3 full handshake, Signal X3DH \E2\80\94 the goal is analysis time under ten minutes, compared to hours for current tools.
This follows from seven architectural decisions, grouped into three categories:
Memory management. Arena allocation places each symbolic term in a bump allocator recreated per run \E2\80\94 removing allocator overhead and improving cache locality. Hash consing stores identical subterms in a single instance, making term comparison O(1) instead of O(n). Together, these two decisions account for roughly half of the projected speedup.
Parallelism. Work-stealing pool for parallel state expansion \E2\80\94 each state processed independently. Incremental knowledge closure \E2\80\94 when a new fact is added, only its consequences are computed, not the entire closure. Together: near-linear scaling with core count.
Solver integration. Batch SMT encoding \E2\80\94 all terms in one solver call instead of one per term \E2\80\94 removes the dominant bottleneck in deep property checking. Precomputed hashing on term construction eliminates redundant structure traversal.
Additionally: Rust as the implementation language provides control over memory layout and safe parallelism that OCaml (ProVerif) and Haskell (Tamarin) do not offer for this workload.
Sixteen attacker models
Most tools default to Dolev-Yao and stop there. The analyzer we are building supports sixteen distinct attacker models: passive eavesdropper, insider, quantum, resource-bounded, compromised certificate authority, side-channel equipped, and others.
A protocol can be secure against a passive eavesdropper but vulnerable to an insider with access to key material. Or safe against classical attacks but broken by a quantum adversary that solves ECDH. Analyzing under a single model gives a single answer. Analyzing under sixteen models gives a map of where the protocol breaks and where it holds.
Neural networks: guiding search with GNNs and active learning
The state space of protocol analysis is exponential \E2\80\94 brute-force search wastes time on dead-end regions, and hand-crafted heuristics help but do not generalize.
We use graph neural networks (GNNs) to guide the search. A GNN scores states in the search space \E2\80\94 predicting which regions are more likely to contain attacks. The symbolic engine explores high-scoring regions first.
Why GNNs? We evaluated alternatives: reinforcement learning requires millions of trials to converge \E2\80\94 sample efficiency is too low when each trial is a full protocol analysis. Recurrent networks process sequences, but protocol states are graphs \E2\80\94 flattening them loses structural information. GNNs operate directly on state graphs, preserve structural relationships, and require less training data.
Training uses active learning: the analyzer runs, the results (which states led to attacks, which were dead ends) become training data, and the model improves over repeated analyses. Every analysis run produces useful training data.
The key principle: neural networks guide search order, but all conclusions come from formal symbolic verification. The network is a heuristic accelerator, never an oracle.
Architecture: modularity as a design requirement
The tool is split into several dozen crates \E2\80\94 self-contained Rust libraries, each responsible for a distinct domain. The main groups:
- Analysis core \E2\80\94 Dolev-Yao model, state space search, property checking, SMT encoding, observational equivalence.
- Repair module \E2\80\94 CEGIS loop, repair rules, multi-objective optimization.
- Specialized analyzers \E2\80\94 quantum, side-channel, game-theoretic, MPC, fuzzing, binary, physical.
- Infrastructure \E2\80\94 CLI, web interface, LSP server, CI/CD integration, WASM bindings.
A contributor can work on the quantum module without understanding the fuzzer \E2\80\94 that is why we chose modularity over a monolith. The core analyzer has no dependency on the web server. Each crate has its own tests, documentation, and release cycle. This isolation makes the tool possible to contribute to and reason about at scale.
What we do that no one else does
- Quantum analysis. BB84, E91, DI-QKD, noisy channel analysis, post-quantum migration.
- Side-channel analysis. DPA, CPA, template attacks, mutual information analysis, masking verification.
- Game-theoretic analysis. Nash equilibrium, Bayesian games, correlated equilibrium, MEV analysis.
- MPC verification. BGW, SPDZ, MASCOT, OT extension.
- Coverage-guided fuzzing. Mutation testing with coverage feedback, integrated with symbolic execution.
- Protocol standard library. Ready-made descriptions of real protocols.
What exists now
As of this writing:
- Symbolic analysis core \E2\80\94 stable, passes tests on classical protocols and simplified TLS handshake.
- Repair module \E2\80\94 functional, generates verified patches for found attacks.
- GNN search guide \E2\80\94 working with active learning, shows measurable speedup on test sets.
- Quantum, leakage, MPC modules \E2\80\94 basic implementation, will be deepened.
What is not ready: unbounded session verification through Horn clauses, export to various formats, distributed cluster analysis, WASM version for web playground.
The bottom line
We are building a protocol analyzer that fixes attacks and covers attack surfaces existing tools ignore, and runs fast enough for real-world protocols.
The architecture is settled, the key decisions are made, the code is being written.
This project is under active development. The final form described here is not yet shipped. But every decision in this article is already embodied in code or in active development. We are reporting concrete progress, not speculating.
If you have worked with ProVerif, Tamarin, or other verification tools \E2\80\94 we want to hear your opinion. We welcome feedback on where we are wrong or what we are missing. The formal verification community is small, and that is its strength.
This project is under active development. This article describes the target architecture and planned capabilities of a tool that is still being built. No product is being announced \E2\80\94 only decisions, trade-offs, and the current state of implementation.
