Verifying Security Protocols: An Application of CSP
Verifying Security Protocols: An Application of CSP
复制标题
验证安全协议：CSP 的应用
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Rob Delicata
中科院分区：
文献类型：
--
作者：
Steve A. Schneider;Rob Delicata
协议分析领域是CSP被证明特别成功的一个领域，并且已经提出了几种使用CSP来推断安全属性（如机密性和身份验证）的技术。在本文中，我们描述了一种这样的方法，基于定理证明，它使用秩函数的思想来建立协议的正确性。这种描述的动机是考虑一个简单但有缺陷的身份验证协议。我们展示了如何使用秩函数分析来定位此缺陷，并证明修改后的协议版本是正确的。
The field of protocol analysis is one area in which CSP has proven particularly successful, and several techniques have been proposed that use CSP to reason about security properties such as confidentiality and authentication. In this paper we describe one such approach, based on theorem-proving, that uses the idea of a rank function to establish the correctness of protocols. This description is motivated by the consideration of a simple, but flawed, authentication protocol. We show how a rank function analysis can be used to locate this flaw and prove that a modified version of the protocol is correct.