Detailed Security Proofs for DARLT

This document gives the complete definitions, oracles and security proofs for DARLT, delegatable anonymous rate-limited tokens with batch spending and public accountability for AI agents. It contains the full experiments for accountability, non-frameability, metadata hiding and least-privilege delegation, the proofs for the underlying primitive SPSEQ-FC in the generic group model, and the proofs of all security theorems of DARLT.