proverif-tamarin-protocol-modeling

Formal protocol verification with ProVerif and Tamarin Prover for multi-agent coordination systems. Use when modeling secrecy properties (escrow opacity, session note confidentiality), replay resistance (token dismissal finality, backup-restore attacks), delegation chain correctness, or append-only log integrity in applied pi calculus. Use when deciding between ProVerif and Tamarin for a given property. Use when extending existing .pv models (e.g., harbor_card_v3_delegation.pv) with new security queries. NOT for general cryptography tutorials, TLS certificate management, key management operations (rotation, storage, HSM integration), or smart contract verification (use Solidity-specific tools).