PF-IBAKA and PF-IBAKA-H Reproducibility Artifact: Tamarin Models, Implementations, Tests, and Benchmark Data

This reproducibility artifact accompanies the manuscript “Compromise-Isolated Handover for Pairing-Free Identity-Based Authenticated Key Agreement in Vehicle-to-Infrastructure Networks.” The archive contains the formal specifications and verification material for PF-IBAKA and PF-IBAKA-H, including Tamarin models, proof scripts, raw prover outputs, falsified lemmas, and negative-control variants. It also contains the reference implementations, functional and security-regression tests, wire-format validation, benchmark scripts, and raw performance measurements collected on x86 and Raspberry Pi 4 platforms. PF-IBAKA is a pairing-free identity-based authenticated key-agreement protocol that separates the Diffie–Hellman exponent from the signature nonce. PF-IBAKA-H is a handover protocol in which both endpoints contribute static–ephemeral secrets to isolate the target session from a compromised source roadside unit. The artifact is intended to support independent reproduction of the formal-verification results, functional tests, communication-cost calculations, and experimental evaluation reported in the manuscript. DOI: https://doi.org/10.5281/zenodo.22955833