Tamarin proof for the KEMTLS protocol using the multi-stage AKE model
-
Updated
Apr 19, 2023 - Makefile
Tamarin proof for the KEMTLS protocol using the multi-stage AKE model
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
Artifact for "The Secrets Must Not Flow: Scaling Security Verification to Large Codebases" (S&P '26)
Tamarin files parser and cryptographic protocols models
Claude Skill: extract cryptographic protocol message flow from code, RFCs, ProVerif or Tamarin models into Mermaid + ASCII sequence diagrams
X-Men 2.0 is a formal-analysis tool that mutates security ceremony specifications to model realistic human errors such as forgetting, slipping, and mistyping. It generates meaningful protocol variants for verification in Tamarin, helping researchers expose weaknesses in human-in-the-loop security workflows.
Add a description, image, and links to the tamarin topic page so that developers can more easily learn about it.
To associate your repository with the tamarin topic, visit your repo's landing page and select "manage topics."