一句话：将符号密码学推理嵌入 Iris 分离逻辑，提出认证协议新规约，使协议验证结果可复用于更大系统。
该论文提出 Cryptis，它是 Iris 分离逻辑的一个扩展，用于符号模型下的密码学推理。分离逻辑擅长并发与资源推理，但难以处理密码学假设；而密码学协议验证的结果通常无法复用到依赖该协议的更大系统。Cryptis 将二者结合，使协议正确性证明可被后续系统验证复用。为支持这一整合，作者为认证协议提出了新的规约，让网络中的代理能够就系统资源的使用达成一致。作者在 Rocq 中形式化验证了多种认证协议，以及一个使用这些认证协议与客户端建立连接的键值存储服务器，验证结果全部机器化检查。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2502-21156,
title = {Cryptis: Cryptographic Reasoning in Separation Logic},
author = {Arthur Azevedo de Amorim and Amal Ahmed and Marco Gaboardi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776730}
}