Calculus of Cryptographic Communication
Calculus of Cryptographic Communication
复制标题
密码通信演算
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
U. Nestmann
中科院分区：
文献类型：
--
作者：
J. Borgström;S. Kramer;U. Nestmann
我们定义C3，一个基于模型的形式主义，是一个框架的建模，规范和验证的密码协议的一半。C3由分布式进程的设计语言和并发执行的相关概念（SOS）组成。我们框架的另一半是基于属性的形式主义，即，C3和CPL的协同设计的两个主要特征是C3过程的约简约束可以通过CPL满意度进行检查，并且C3的观测等价概念和CPL的命题知识概念具有共同的定义基础，即结构上不可区分的协议历史。此外，这种协同设计允许在同一框架内分离协议和属性描述的关注点。C3的其他重要特性是安全（带外）通信和基于历史的密钥查找的明确概念，它们共同提供了认证和密钥建立协议的具体基础。
We define C3, a model-based formalism that is one half of a framework for the modelling, specification and verification of cryptographic protocols. C3 consists of a design language of distributed processes and an associated (SOS) notion of concurrent execution. The other half of our framework is a property-based formalism, i.e., a logic for the specification and verification of cryptographic protocols, called CPL. The two primary features of the co-design of C3 and CPL are that reduction constraints of C3-processes are checkable via CPL-satisfaction, and that C3’s notion of observational equivalence and CPL’s notion of propositional knowledge have a common definitional basis, namely structurally indistinguishable protocol histories. Moreover, this co-design permits separation of the concerns of protocol and property description, within the same framework. Other important features of C3 are explicit notions of secure (out- of-band) communication and history-based key lookup, which together give a concrete foundation on which to base authentication and key establishment protocols.