Deriving, Attacking and Defending the GDOI Protocol
Deriving, Attacking and Defending the GDOI Protocol
复制标题
DOI：
10.1007/978-3-540-30108-0_4
复制
发表时间：
2004-09
期刊：
影响因子：
--
通讯作者：
C. Meadows;Dusko Pavlovic
中科院分区：
文献类型：
--
作者：
C. Meadows;Dusko Pavlovic
作为对安全增量推理逻辑框架持续努力的一部分，我们尝试对 GDOI 进行派生重建，GDOI 是 IETF RFC 3547 中提出的协议，用于 IPsec 组通信中经过身份验证的密钥协议。在推导其身份验证属性之一时遇到的困难导致我们推导了一种在之前对该协议的广泛分析中未曾出现过的攻击。事实证明，派生技术不仅有助于构建、分析和修改协议，而且有助于攻击协议。我们认为，所提出的结果证明了派生方法的要点，该方法通过精炼和组合基本协议组件来跟踪和形式化协议的非正式设计方式。在简要概述了简单的身份验证逻辑之后，我们概述了 GDOI 的派生，它显示了其有效的安全属性，以及对其进行的两次攻击的派生，显示了其不需要的属性。我们还讨论了一些消除这些漏洞的修改。它们的推导表明了所需身份验证的证据。在撰写本文时，我们正在与 Msec 工作组合作开发此问题的解决方案。
As a part of a continued effort towards a logical framework for incremental reasoning about security, we attempted a derivational reconstruction of GDOI, the protocol proposed in IETF RFC 3547 for authenticated key agreement in group communication over IPsec. The difficulties encountered in deriving one of its authentication properties led us to derive an attack that had not surfaced in the previous extensive analyses of this protocol. The derivational techniques turned out to be helpful not only for constructing, analyzing and modifying protocols, but also attacks on them. We believe that the presented results demonstrate the point the derivational approach, which tracks and formalizes the way protocols are designed informally: by refining and composing basic protocol components.After a brief overview of the simple authentication logic, we outline a derivation of GDOI, which displays its valid security properties, and the derivations of two attacks on it, which display its undesired properties. We also discuss some modifications that eliminate these vulnerabilities. Their derivations suggest proofs of the desired authentication. At the time of writing, we are working together with the Msec Working Group to develop a solution to this problem.