Towards an Automatic Analysis of Security Protocols in First-Order Logic
Towards an Automatic Analysis of Security Protocols in First-Order Logic
复制标题
DOI：
10.1007/3-540-48660-7_29
复制
发表时间：
1999-07
期刊：
影响因子：
--
通讯作者：
Christoph Weidenbach
中科院分区：
文献类型：
--
作者：
Christoph Weidenbach
Neuman-Stubblebine 密钥交换协议以一阶逻辑形式化，并由自动定理证明器 Spass 进行分析。除了分析之外，我们还开发了必要的理论背景，为分析中涉及的单子一阶片段提供新的（不可）可判定性结果。该方法适用于各种安全协议，我们确定了可能的扩展，从而引导未来的研究方向。
The Neuman-Stubblebine key exchange protocol is formalized in first-order logic and analyzed by the automated theorem prover Spass. In addition to the analysis, we develop the necessary theoretical background providing new (un)decidability results for monadic firstorder fragments involved in the analysis. The approach is applicable to a variety of security protocols and we identify possible extensions leading to future directions of research.