batch-tamarin 0.2.1

Python wrapper for Tamarin Prover with JSON configuration

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
• 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 and check commands
• Configuration Validation: Validate JSON recipes and preview tasks before execution
• Wellformedness Checking: Check theory files for syntax errors and warnings

Table of Contents

• Features
• Installation
  • Prerequisites
  • From PyPI
  • From local package
• Usage
  • Basic Commands
  • Configuration Example
  • Output
• Development
  • Contributing
  • Dependencies, Configuration
    • Using Nix (the easy way)
    • Using Python Virtual Environment (still pretty easy)
  • Testing During Development
• Packaging/Publishing
  • Building the Package
  • Publishing
• License
  • License Summary
• Implementation Details
• Acknowledgments
• Final Note

Installation

Prerequisites

• Python 3.9+
• Tamarin Prover binaries (installed separately)

From PyPI

pip install batch-tamarin

From local package

Get the latest release from this github repo.

pip install 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

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

Check Command

The check command allows you to validate your configuration and preview the tasks that would be executed without actually running them:

# Basic configuration check
batch-tamarin check recipe.json

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

What the check command does:

• Validates JSON recipe structure and syntax
• Checks file paths and accessibility
• Tests Tamarin binary integrity
• Previews executable tasks that would be run
• Validates theory files for wellformedness issues
• Generates detailed reports when using --report flag

Output includes:

• Total tasks that would be executed
• Task breakdown by Tamarin version
• Resource allocation summary
• Tamarin version integrity test results
• Any validation errors or warnings found
• Wellformedness check reports (with --report flag)

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
    └── ...

As the name of each directory and file describe, you will find successful task in success and their linked models proofs in proofs Failed tasks don't output proofs (that's a tamarin behavior), you will only find a json in failed

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"]
}

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

1. Fork the repository and create a feature branch:

   git checkout -b feature/my-awesome-feature
   

2. Set up development environment (see options below)

3. Install pre-commit hooks:

   ./setup-hooks.sh
   

4. Make your changes and commit them

5. 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)

# Create and activate virtual environment
python -m venv venv
source venv/bin/activate

# Install development dependencies
pip install -r requirements.txt

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

Testing During Development

Running Tests

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

# Run all tests
pytest

# Run with verbose output
pytest -v

# Run specific test file
pytest tests/test_config_manager.py

# Run with coverage report
pytest --cov=src/batch_tamarin

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 pip install -e .)
batch-tamarin --help

# Method 2: Test built package (Useful before publishing)
python -m build
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
python -m 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.