Cryptographic Protocol Synthesis and Verification for Multiparty Sessions
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions
复制标题
多方会话的密码协议综合和验证
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
J. Leifer
中科院分区：
文献类型：
--
作者：
K. Bhargavan;R. Corin;Pierre;C. Fournet;J. Leifer
我们提出了一个编译器的设计和实现，该编译器根据高级多方会话描述生成自定义加密协议。我们的会话指定了分布式参与者之间消息交换和数据访问的预先安排模式。它们为每个参与者的所有消息提供强大的安全保证。我们的编译器生成用于发送和接收这些消息的代码，以及加密操作和检查，以强制执行这些保证，防止任何可能控制网络和某些会话参与者的对手。我们通过依赖于最新的加密类型系统来验证生成的代码是安全的。大多数证明是由机械化的类型检查完成的，并不依赖于编译器的正确性。我们在捕获协议代码的可执行细节的模型中获得了迄今为止最强的会话安全保证。我们用一系列受web服务启发的协议来说明和评估我们的方法。
We present the design and implementation of a compiler that, given high-level multiparty session descriptions, generates custom cryptographic protocols. Our sessions specify pre-arranged patterns of message exchanges and data accesses between distributed participants. They provide each participant with strong security guarantees for all their messages. Our compiler generates code for sending and receiving these messages, with cryptographic operations and checks, in order to enforce these guarantees against any adversary that may control both the network and some session participants. We verify that the generated code is secure by relying on a recent type system for cryptography. Most of the proof is performed by mechanized type checking and does not rely on the correctness of our compiler.We obtain the strongest session security guarantees to date in a model that captures the executable details of protocol code. We illustrate and evaluate our approach on a series of protocols inspired by web services.