应用Pi演算：移动值、新名称和安全通信
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
摘要：
我们研究的编程结构的互动“新”，它产生静态范围的名称，通过信道上的消息通信。这种交互在安全协议中至关重要，这是我们工作的主要激励示例，它也出现在其他编程语言上下文中。我们定义了应用π演算，一个简单的，一般的π演算的扩展，其中的值可以形成从名称通过应用程序的内置函数，受方程，并作为消息发送。(In相比之下，纯pi演算缺少内置函数，它的唯一消息是原子名。我们开发的语义和证明技术，这种扩展的语言，并将其应用于推理安全协议。本文基本上包含了2001年介绍应用π演算的会议论文。它填补了空白，结合改进，并进一步解释和研究应用π演算。自2001年以来，应用π演算一直是许多进一步工作的基础，在许多研究出版物中描述，有时体现在有用的软件中，例如ProVerif工具，它依赖于应用π演算来支持安全协议的规范和自动分析。虽然本文的目的不是要成为一个完整的审查的主题，它受益于进一步的工作，并提供了更好的基础，其中一些。特别是，应用π演算已经通过其在ProVerif的实现演变，目前的定义反映了这种演变。
英文摘要：
We study the interaction of the programming construct "new", which generates statically scoped names, with communication via messages on channels. This interaction is crucial in security protocols, which are the main motivating examples for our work, it also appears in other programming-language contexts. We define the applied pi calculus, a simple, general extension of the pi calculus in which values can be formed from names via the application of built-in functions, subject to equations, and be sent as messages. (In contrast, the pure pi calculus lacks built-in functions, its only messages are atomic names.) We develop semantics and proof techniques for this extended language and apply them in reasoning about security protocols. This paper essentially subsumes the conference paper that introduced the applied pi calculus in 2001. It fills gaps, incorporates improvements, and further explains and studies the applied pi calculus. Since 2001, the applied pi calculus has been the basis for much further work, described in many research publications and sometimes embodied in useful software, such as the tool ProVerif, which relies on the applied pi calculus to support the specification and automatic analysis of security protocols. Although this paper does not aim to be a complete review of the subject, it benefits from that further work and provides better foundations for some of it. In particular, the applied pi calculus has evolved through its implementation in ProVerif, and the present definition reflects that evolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
