Tamarin models for state continuity of SGX enclave programs

Data driven Public Key Ecosystem Backed by Blockchain & Fault Tolerance. Keywords: Trustless PKI, Blockchain, Consensus, Merkle tree, Merkle proof, Practical Byzantine Fault Tolerance (PBFT), Proof of Work (PoW), X.509 alternative

Tamarin models for Bluetooth secure pairing protocols: Passkey Entry (PE) and Numeric comparison (NC)

Tamarin files associated with my thesis "Formal Analysis and Applications of Direct Anonymous Attestation"

A Python package that enables batch execution of tamarin-prover tasks with JSON configuration files and comprehensive reporting.

Tamarin codes for checking verifiability properties of Helios, Belenios and the Estonian e-voting protocol.

Esperimenti e progetti realizzati durante il corso di Computer Security 2021/2021

High-level frontend language to Tamarin prover

Theoretical and practical introduction to the Tamarin Prover through a real-world case study on the Needham Schroeder protocol

A Docker image for the Tamarin prover

An vscode extension for highlighting tamarin-prover.

This repository provides the formal model and proofs for SOAP, a SOcial Authentication Protocol.

Tamarin proofs for the OTR and PAKE security protocols

A (work-in-progress) implementation of IPsec in Tamarin-Prover for automated security analysis

Beginner-friendly seminar about the work of Basin D. et Al. on formalizing social engineering attacks in the symbolic model

The formal proof of the security of the Mutual Authentication and Key Exchange (MAKE) protocol of LDACS using the symbolic model checker Tamarin.

Tree-sitter grammar and syntax highlight for the Tamarin Prover theory files

Formal Verification of Security Protocols

Dockerfile for Tamarin prover

confluin does confluence checks for Tamarin input files