Cryptis: Cryptographic Reasoning in Separation Logic
Abstract
We introduce Cryptis , an extension of the Iris separation logic for the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Rocq.
Fields of Study & Subjects
Advanced Authentication Protocols Security
Cryptography and Data Security
Security and Verification in Computing
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Publisher
- Association for Computing Machinery (ACM)
- Volume
- 10
- Issue
- POPL
- Pages
- 2555–2585
- Publication date
- 8 January 2026
- Language
- EN