Exemption Without Exposure: Formally Verified Conditional Privacy-Preserving Authentication with Secure-Ranging Binding for Authorised Armed Carriers in AI Weapon Surveillance

Abstract Automated weapon detectors treat every visible firearm as a threat, yet plain-clothes soldiers, police officers and licensed guards lawfully carry weapons on the roads where kidnappers operate. Exempting them keeps false alarms manageable, but an exemption is also an attack surface: a stolen, relayed or wrongly attributed credential can silence an alert about a genuine threat. This paper presents conditional privacy-preserving authentication (CPPA) for authorised armed carriers in artificial intelligence surveillance. Carriers present short-lived pseudonymous role credentials through a challenge-response exchange, so the verifier learns a role but not an identity, while an oversight authority can resolve a pseudonym only under lawful order. Ultra-wideband secure ranging binds the credential to the vehicle the camera flagged, and a three-outcome policy ensures that no weapon detection is silently discarded. The protocol is verified in the Tamarin prover: unforgeability, injective agreement, identity secrecy and unlinkability hold, and weakening any of four design elements yields an attack. A reference implementation verifies a 225-byte presentation in a median of 253\,{\unboldmath$\upmu$}s on one 2.1~GHz virtual processor. Monte Carlo simulation shows a binding error of {\unboldmath$6.7\times10^{-4}$} for side-by-side vehicles with 0.1~m ranging and 0.5~m camera localisation, against 0.08 with 1~m ranging and localisation. In a representative scenario, binding lowers the probability that a threat is silently exempted from 0.21 to the credential compromise rate of 0.01. A closed-form analysis of multi-agent threat verification shows that half of its accuracy gain is lost once agent errors correlate at about 0.4.