Batch Tamarin (`batch-tamarin`) : Tamarin Python Wrapper

A Python wrapper for Tamarin Prover that enables batch execution of protocol verification tasks with JSON configuration files, comprehensive reporting, and validation tools.

Features

Batch Execution: Run multiple Tamarin models across different Tamarin binary versions
JSON Configuration: Define execution recipes using simple JSON configuration files
Interactive Configuration: Generate JSON configurations from spthy files with guided prompts
Resource Management: Intelligent CPU and memory allocation for parallel task execution
Progress Tracking: Real-time progress updates with Rich-formatted output
Output Processing: Reformat the different Tamarin output to give a detailed summary of execution
CLI Interface: Easy-to-use command-line interface with run, check, init, and report commands
Configuration Validation: Validate JSON recipes and preview tasks before execution
Wellformedness Checking: Check theory files for syntax errors and warnings
Comprehensive Reporting: Generate detailed reports in multiple formats (Markdown, HTML, LaTeX, Typst)
Result Caching: Intelligent caching system to avoid re-executing identical tasks
Trace Visualization: Automatic generation of attack trace visualizations in SVG format

Installation

Prerequisites

Python 3.10+
Tamarin Prover binaries (installed separately)

From PyPI

pip install batch-tamarin

# Or using uv (faster)
uv pip install batch-tamarin

From local package

Get the latest release from this github repo.

pip install ./batch_tamarin-0.1.1-py3-none-any.whl

# Or using uv (faster)
uv pip install ./batch_tamarin-0.1.1-py3-none-any.whl

Usage

Basic Commands

# Show version
batch-tamarin --version

# Show help
batch-tamarin --help

# Run tasks with configuration file
batch-tamarin run recipe.json

# Run with debug output
batch-tamarin run recipe.json --debug

# Check configuration and preview tasks
batch-tamarin check recipe.json

# Check with detailed wellformedness report
batch-tamarin check recipe.json --report

# Check with debug output
batch-tamarin check recipe.json --debug

# Generate configuration interactively from spthy files
batch-tamarin init protocol.spthy

# Generate configuration with multiple files and custom output
batch-tamarin init protocol1.spthy protocol2.spthy --output my_recipe.json

# Generate comprehensive reports from execution results
batch-tamarin report ./results --output report.md --format md

# Generate HTML report with interactive visualizations
batch-tamarin report ./results --output report.html --format html

# Generate LaTeX report for academic publications
batch-tamarin report ./results --output report.tex --format tex

# Clear cached results
batch-tamarin --rm-cache

Configuration Example

Create a JSON configuration file based on the WPA2 example:

{
	"config": {
		"global_max_cores": 10,
		"global_max_memory": "max",
		"default_timeout": 7200,
		"output_directory": "./results"
	},
	"tamarin_versions": {
		"stable": {
			"path": "tamarin-binaries/tamarin-prover-1.10/1.10.0/bin/tamarin-prover"
		},
		"legacy": {
			"path": "tamarin-binaries/tamarin-prover-1.8/1.8.0/bin/tamarin-prover"
		}
	},
	"tasks": {
		"wpa2": {
			"theory_file": "protocols/wpa2_four_way_handshake_unpatched.spthy",
			"tamarin_versions": ["stable", "legacy"],
			"output_file": "wpa2.txt",
			"preprocess_flags": ["yes"],
			"tamarin_options": ["-v"],
			"resources": {
				"max_cores": 2,
				"max_memory": 8,
				"timeout": 3600
			},
			"lemmas": [
				{
					"name": "nonce_reuse_key_type",
					"resources": {
						"max_cores": 1
					}
				},
				{
					"name": "authenticator_rcv_m2_must_be_preceded_by_snd_m1",
					"tamarin_versions": ["stable"],
					"resources": {
						"max_cores": 4,
						"max_memory": 16,
						"timeout": 30
					}
				}
			]
		}
	}
}

Read the configuration guide to understand how to write a JSON recipe : JSON Guide

Output

The wrapper will output the results of all analysis in the output_file specified in the recipe. It will follow this pattern :

output_directory/
├── failed/
│   ├── output_prefix[\_lemma]\_tamarin_alias.json
│   └── ...
├── proofs/
│   ├── output_prefix[\_lemma]\_tamarin_alias.spthy
│   └── ...
├── success/
│   ├── output_prefix[\_lemma]\_tamarin_alias.json
│   └── ...
└── traces/
    ├── output_prefix[\_lemma]\_tamarin_alias.json
    ├── output_prefix[\_lemma]\_tamarin_alias.dot
    ├── output_prefix[\_lemma]\_tamarin_alias.svg
    └── ...

As the name of each directory and file describe, you will find:

success/: JSON results for successful task executions with detailed timing and lemma verification information
failed/: JSON results for failed tasks with error descriptions and diagnostics
proofs/: Generated .spthy model files from successful Tamarin runs (not generated for failed tasks)
traces/: Attack trace visualizations in JSON, DOT, and SVG formats when available

Here is an example for each result json : success/

{
	"task_id": "wpa2_authenticator_installed_is_unique_for_anonce_dev",
	"warnings": ["1 wellformedness check failed!"],
	"tamarin_timing": 12.27,
	"wrapper_measures": {
		"time": 12.385284208023222,
		"avg_memory": 200.17067307692307,
		"peak_memory": 358.34375
	},
	"output_spthy": "results/models/wpa2_authenticator_installed_is_unique_for_anonce_dev.spthy",
	"verified_lemma": {
		"authenticator_installed_is_unique_for_anonce": {
			"steps": 102,
			"analysis_type": "all-traces"
		}
	},
	"falsified_lemma": {},
	"unterminated_lemma": ["nonce_reuse_key_type", "...", "krack_attack_ptk"]
}

failed/

{
	"task_id": "wpa2_authenticator_rcv_m2_must_be_preceded_by_snd_m1_dev",
	"error_description": "The task exceeded its memory limit. Review the memory limit setting for this task.",
	"wrapper_measures": {
		"time": 30.274985666008433,
		"avg_memory": 566.9329637096774,
		"peak_memory": 1059.609375
	},
	"return_code": -2,
	"last_stderr_lines": ["Process exceeded memory limit"]
}

Report Generation

After running batch execution, you can generate comprehensive reports using the report command:

# Generate a Markdown report with statistics and charts
batch-tamarin report ./results --output execution_report.md --format md

# Generate an interactive HTML report
batch-tamarin report ./results --output execution_report.html --format html

# Generate a LaTeX report for academic publications
batch-tamarin report ./results --output execution_report.tex --format tex

# Generate a modern Typst report
batch-tamarin report ./results --output execution_report.typ --format typ

Report Features:

Execution Statistics: Success/failure rates, timing analysis, resource utilization
Visual Charts: Pie charts for error types, bar charts for execution times, Gantt charts for timelines
Trace Visualization: Embedded attack trace diagrams when available
Multiple Formats: Choose the format that best fits your needs (presentations, publications, web)

The report command automatically validates the results directory structure and generates comprehensive analytics from your batch execution results.

Development

A macOS or Linux environment is highly recommended, as tamarin-prover is only running on these OS. You can use WSL2 on Windows hosts.

Contributing

Fork the repository and create a feature branch:
```
git checkout -b feature/my-awesome-feature
```
Set up development environment (see options below)
Install pre-commit hooks (uses ruff for formatting/linting):
```
uv run pre-commit install
```
Make your changes and commit them
Push to your branch and open a pull request

Dependencies, Configuration

Using Nix (the easy way)

# Enter development environment with all dependencies
nix develop

# Install the package in editable mode (required once per environment)
pip install -e .

# The batch-tamarin command is now available
batch-tamarin --version

Using Python Virtual Environment (still pretty easy)

# Install uv if not already installed
curl -LsSf https://astral.sh/uv/install.sh | sh

# Create virtual environment and install all dependencies (including dev)
uv sync --extra dev

# The package is installed in editable mode automatically
batch-tamarin --version

Using uv directly (without venv)

# Install uv if not already installed
curl -LsSf https://astral.sh/uv/install.sh | sh

# Run commands without creating a venv
uv run --extra dev batch-tamarin --version
uv run --extra dev pytest

Testing During Development

Running Tests

The project uses pytest for testing. To run the test suite:

# Run all tests (uses uv to run in the project environment)
uv run pytest

# Run with verbose output
uv run pytest -v

# Run specific test file
uv run pytest tests/test_config_manager.py

Code Quality

The project uses ruff for linting and formatting:

# Check code for issues
ruff check src/

# Automatically fix issues
ruff check src/ --fix

# Format code
ruff format src/

# Check formatting without applying
ruff format --check src/

Testing the Package Installation

Since the package uses proper Python packaging structure, you cannot run python src/batch_tamarin/main.py directly. Use one of these methods:

# Method 1 (Recommended): Use the CLI command (after uv sync --extra dev)
batch-tamarin --help

# Method 2: Test built package (Useful before publishing)
uv build
uv pip install dist/batch_tamarin-*.whl

Packaging/Publishing

Building the Package

# Clean previous builds
rm -rf dist/ build/ **/*.egg-info/ # Be careful, it's still a rm -rf command
# Might fail because of *.egg-info pattern, you might want to remove it

# Build wheel and source distribution
uv build

Publishing

Test Upload (TestPyPI)

python -m twine upload --repository testpypi dist/*

Production Upload (PyPI)

python -m twine upload dist/*

For detailed packaging instructions, see PACKAGING.md.

License

This project is licensed under the GNU General Public License v3.0 or later (GPL-3.0-or-later).

See the LICENSE file for the full license text.

License Summary

✅ Use: Commercial and private use allowed
✅ Modify: Modifications and derivatives allowed
✅ Distribute: Distribution allowed
❗ Share Alike: Derivatives must be licensed under GPL-3.0+
❗ Disclose Source: Source code must be made available
❗ Include License: License and copyright notice must be included

Implementation Details

For detailed architecture, module overview, and workflow documentation, see ARCHITECTURE.md.

Acknowledgments

This project has been done during an internship at CISPA. It was made with the help of the Cas Cremers research group, a particular thanks should go to :

Cas Cremers, as the supervisor of this internship but also for all his support and guidance.
Maïwenn Racouchot and Aleksi Peltonen for their close collaboration, feedback, and, most importantly, the logo.
Esra Günsay, Erik Pallas, Niklas Medinger, Aurora Naska and Alexander Dax for their valuable support and development ideas.

Final Note

As this package need to directly use tamarin-prover commands, you can visit the Tamarin Prover website for installation instructions.

Name		Name	Last commit message	Last commit date
Latest commit History 244 Commits
.github		.github
assets		assets
examples		examples
scripts		scripts
src/batch_tamarin		src/batch_tamarin
tests		tests
.gitignore		.gitignore
.pre-commit-config.yaml		.pre-commit-config.yaml
ARCHITECTURE.md		ARCHITECTURE.md
LICENSE		LICENSE
MANIFEST.in		MANIFEST.in
PACKAGING.md		PACKAGING.md
README.md		README.md
RECIPE_GUIDE.md		RECIPE_GUIDE.md
flake.lock		flake.lock
flake.nix		flake.nix
pyproject.toml		pyproject.toml
setup-hooks.sh		setup-hooks.sh
tamarin-config-schema.json		tamarin-config-schema.json
uv.lock		uv.lock

Folders and files

Latest commit

History

Repository files navigation

Batch Tamarin (batch-tamarin) : Tamarin Python Wrapper

Features

Table of Contents

Installation

Prerequisites

From PyPI

From local package

Usage

Basic Commands

Configuration Example

Output

Report Generation

Development

Contributing

Dependencies, Configuration

Using Nix (the easy way)

Using Python Virtual Environment (still pretty easy)

Using uv directly (without venv)

Testing During Development

Running Tests

Code Quality

Testing the Package Installation

Packaging/Publishing

Building the Package

Publishing

Test Upload (TestPyPI)

Production Upload (PyPI)

License

License Summary

Implementation Details

Acknowledgments

Final Note

About

Topics

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases 11

Contributors

Uh oh!

Languages

Batch Tamarin (`batch-tamarin`) : Tamarin Python Wrapper