A Symbolic Analysis of Agent Evidence Packages

This article studies an Agent Evidence Package (AEP) profile from the Agent Trust Framework (EATF) and a Model Context Protocol (MCP) attestation profile using symbolic protocol modeling in Tamarin. The starting point is an ordinary engineering question: if a valid signed evidence package is shown to a verifier twice, is the second acceptance only another inspection, or a new action? The model represents agent authorization, gateway forwarding, signer issuance, timestamping, ledger anchoring, and verifier acceptance under explicit Dolev--Yao and trust-anchor assumptions. Several correspondence-style properties verify, including signer and agent authentication, payload integrity, timestamp-event linkage, forward-integrity-style pre-compromise attribution, and resistance to a malicious gateway acting as a signing oracle. The clearest negative result concerns replay semantics: a stateless verifier can accept the same otherwise valid package hash more than once, so freshness and ledger anchoring alone do not imply unique verifier acceptance. A replay-cache variant verifies uniqueness under added verifier state. The contribution is model-bounded and profile-dependent: replay resistance must be stated as a verifier-state or challenge-bound property when a downstream application treats acceptance as a fresh event.