一句话：提出核心演算 IPDL，支持密码协议观察等价的等式证明并机器化到 Coq。
交互式密码协议的安全性常通过证明其与理想规范观察等价来建立，但现有机器化支持有限：diff-equivalence 要求控制结构相同，或需显式给出 bisimulation 见证。本文提出核心演算 IPDL，用于密码协议观察等价的等式证明，并统一处理概率行为、分布式消息传递以及资源受限的敌手与模拟器。作者在分布式抛硬币、不经意传输和 GMW 多方计算等案例上展示 IPDL，并通过将其嵌入 Coq 证明助手完成所有证明的机器化。
Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool support for observational equivalence of cryptographic protocols is still a nascent area of research. Current mechanization efforts tend to either focus on diff-equivalence, which establishes observational equivalence between protocols with identical control structures, or require an explicit witness for the observational equivalence in the form of a bisimulation relation. Our goal is to simplify proofs for cryptographic protocols by introducing a core calculus, IPDL, for cryptographic observational equivalences. Via IPDL, we aim to address a number of theoretical issues for cryptographic proofs in a simple manner, including probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate IPDL on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of case studies are mechanized via an embedding of IPDL into the Coq proof assistant.
@article{paperbot2098,
title = {A Core Calculus for Equational Proofs of Cryptographic Protocols},
author = {Joshua Gancher and Kristina Sojakova and Xiong Fan and Elaine Shi and Greg Morrisett},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571223}
}