Bisimulation-based Non-deterministic Admissible Interference and its Application to the Analysis of Cryptographic Protocols
Bisimulation-based Non-deterministic Admissible Interference and its Application to the Analysis of Cryptographic Protocols
复制标题
基于双模拟的非确定性容许干扰及其在密码协议分析中的应用
DOI：
10.1016/s1571-0661(04)00311-1
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
J. Mullins
中科院分区：
文献类型：
--
作者：
S. Lafrance;J. Mullins
在本文中，我们首先定义了基于互模拟的非确定性容许干扰（BNAI），推导了其过程理论表征，并提出了一种针对通信过程中主要算子的组合验证方法，以这种方式将[19]中获得的类似的基于迹线的结果概括为基于观察的互模拟的更精细概念[6]。与基于跟踪的版本一样，BNAI 仅通过降级器（例如密码系统）承认保密级别之间的信息流，但被表述为观察等效性的概括 [18]。然后，我们描述了一种用于分析密码协议的可接受的基于干扰的方法，以一种不平凡的方式扩展了[11]中提出的基于非干扰的方法。密码协议的保密性和身份验证是根据 BNAI 定义的，并推导出各自的基于互模拟的证明方法。最后，作为该方法的重要说明，我们考虑简单的案例研究：Wide Mouthed Frog 协议 [1] 和 Woo 和 Lam 单向身份验证协议 [25] 的典型示例。这种方法的最初想法是证明入侵者只能通过在导致无害干扰时被视为允许的选定通道来干扰协议。
In this paper, we first define bisimulation-based non-deterministic admissible interference(BNAI), derive its process-theoretic characterization and present a compositional verification method with respect to the main operators over communicating processes, generalizing in this way the similar trace-based results obtained in [19] into the finer notion of observation-based bisimulation [6]. Like its trace-based version, BNAI admits information flow between secrecy levels only through a downgrader (e.g. a cryptosystem), but is phrased into a generalization of observational equivalence [18]. We then describe an admissible interference-based method for the analysis of cryptographic protocols, extending, in a non-trivial way, the non interference-based approach presented in [11]. Confidentiality and authentication for cryptoprotocols are defined in terms of BNAI and their respective bisimulation-based proof methods are derived. Finally, as a significant illustration of the method, we consider simple case studies: the paradigmatic examples of the Wide Mouthed Frog protocol [1] and the Woo and Lam one-way authentication protocol [25]. The original idea of this methodology is to prove that the intruder may interfere with the protocol only through selected channels considered as admissible when leading to harmless interference.