Decision and Complexity of Dolev-Yao Hyperproperties
summary
Provides the first decision procedure for Dolev–Yao hyperproperties under a bounded number of sessions and subterm-convergent equational theories, proving validity when message quantifiers are guarded and attacker quantification is limited to knowledge derivation. Handles common primitives like encryption, signatures and zero-knowledge, rejects associative/commutative primitives and some indistinguishability fragments. Shows undecidability when sessions are unbounded or restrictions are dropped, and establishes tight complexity bounds — the full fragment is exponential-hierarchy-complete, with practical cases much cheaper.
AI-written summary · about
chapters (7)
- 0:00Dolev-Yao hyperproperties intro
- 2:50Functional vs security hyperproperties
- 6:21Modeling adversarial envs
- 10:17Decidability conditions
- 12:44Complexity analysis
- 14:46Conclusion & future work
- 15:27Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
21mHyper Separation Logic
31mContention in Cryptography: Obfuscation, Leakage, UCE and the AI-DHI Assumptions
22mAutomata and Fixpoints for Asynchronous Hyperproperties
01h 06mObfuscation: Past, Present, and Possible Futures
54mVerification Dilemmas, Law, and the Promise of Zero-Knowledge Proofs
01h 06mCompiled Nonlocal Games: From CHSH to BQP Verification
22mComputational-Bounded Robust Compilation and Universally Composable Security