Cryptographic protocol analysis for real-world protocols.
ProVerif-ATP - Combining ProVerif and Automated Theorem Provers for Security Protocol Verification
Online engine for reasoning about the Noise Protocol Framework.
Lingua Universale -- a verification language for AI agent protocols. Like mypy for multi-agent communication. 3696 tests, zero deps.
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
Formalisation of Ethereum consensus in Isabelle/HOL
Artifact for "The Secrets Must Not Flow: Scaling Security Verification to Large Codebases" (S&P '26)
This repository contains my personal notes, models, and exercises for formal verification using the Tamarin Prover. This is a personal/academic project.
This repository provides the formal model and proofs for SOAP, a SOcial Authentication Protocol.
CESA: A Chebyshev Polynomials based Efficient and Secure Access Authentication Scheme for both UE and mMTC Devices over 5G Networks
AI-powered tool that converts protocol diagrams (PNG, PDF) into formal Tamarin verification models. Task 1 submission for IIT Roorkee Formal Verification course.
Circuit-level modelling and verification of I2S protocol with gate-level SIPO receiver using eSim 2.5 and Ngspice. Published on FOSSEE IIT Bombay.
Reproducibility artifact for 'Sheaf Cohomology for Settlement Protocol Verification' (Rooschuz & Mujic, AGIRAILS, 2026). Computes H1 over the ACTP 8-state lifecycle and validates topological completeness on the published 2-complex.
Verifier-backed abstraction invention for small formal protocol and concurrency systems with contradiction-driven ontology revision
Proof-Carrying Payloads (PCP) is an end-to-end authorization overlay for Pub/Sub Messaging
Browser-based symbolic protocol analysis demo — Dolev-Yao 1983, Lowe 1995. Model the attacker as someone who owns the network but can't break crypto, then let a real search enumerate the attacks you didn't think of. It finds Lowe's Needham-Schroeder trace on its own. Audit every deduction. No backends. No simulated math.
The research plan for my PhD in the Information Security group, ETH Zurich.
Reusable SystemVerilog Assertions and self-checking simulation examples for APB4 protocol verification.
Add a description, image, and links to the protocol-verification topic page so that developers can more easily learn about it.
To associate your repository with the protocol-verification topic, visit your repo's landing page and select "manage topics."