ILC: a calculus for composable, computational cryptography
ILC: a calculus for composable, computational cryptography
复制标题
DOI：
10.1145/3314221.3314607
复制
发表时间：
2019-06
期刊：
影响因子：
--
通讯作者：
Kevin Liao;Matthew A. Hammer;Andrew K. Miller
中科院分区：
文献类型：
--
作者：
Kevin Liao;Matthew A. Hammer;Andrew K. Miller
通用可组合性（UC）框架是以模块化方式分析密码协议的既定标准，以便在与任意其他协议并发组合的情况下保持安全性。然而，尽管UC被广泛用于纸上证明，但之前系统化它的尝试都失败了，要么使用符号模型（从而排除了计算简化证明），要么限制了它的表达能力。在本文中，我们奠定了基础，建立一个具体的，可执行的实现统一通信框架。我们的主要贡献是一个过程演算，被称为交互式Lambda演算（ILC）。ILC忠实地捕捉了UC交互式图灵机（ITM）的计算模型-通过仿射类型规则将ITM适应π演算的子集。换句话说，良好类型的ILC程序可以表示为ITM。反过来，ILC的强融合属性使推理有关密码安全性的减少。我们使用ILC来开发一个简化的UC实现，称为SaUCy。
The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness. In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC—interactive Turing machines (ITMs)—by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC’s strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.