Cryptis: Cryptographic Reasoning in Separation Logic
summary
Cryptis extends Iris separation logic with a symbolic-cryptography model and gives protocol specs that actually exchange separation-logic resources so proofs compose into larger systems. It proves secrecy and freshness rules, mechanizes NSL and Diffie‑Hellman variants, and uses those proofs to verify a reliable encrypted channel and an end-to-end key‑value store implementation. The development is formalized in Rocq, ships evaluated, reusable artifacts, and builds on a separation-logic escrow pattern to transfer ephemeral session state into application resources.
AI-written summary · about
chapters (13)
- 0:00Cryptis introduction
- 4:05Formal verification challenges
- 8:40Cryptis logic core
- 10:49Needham-Schroeder-Lowe verification
- 15:23Composition with abstractions
- 17:33Key takeaways and future
- 18:56Q&A: Tamarin vs Viper
- 20:21Q&A: Reusability in examples
- 20:42Q&A: Clutch and Cryptis
- 21:46Q&A: Adequacy theorems
- 23:12Q&A: Perfect secrecy assumptions
- 23:53Q&A: Resource monoid
- 24:55Q&A: Key management
related talks
21mSeparation Logics for Probability, Concurrency, and Security
16mCerisier: A Program Logic for Attestation in a Capability Machine
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
20mAsynchronous Probabilistic Couplings in Higher-Order Separation Logic
01h 34mIntro to Cryptol and High Assurance Crypto Engineering
39mKeynote: Towards High-Assurance Cryptographic Software
17mBreaking the Lethal Trifecta: Secure Agentic Computing via...