Undecidability of bounded security protocols
Undecidability of bounded security protocols
复制标题
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
A. N.A.DurginP.D.LincolnJ.C.Mitchell;ScedrovComputer
中科院分区：
文献类型：
--
作者：
A. N.A.DurginP.D.LincolnJ.C.Mitchell;ScedrovComputer
使用存在量化的多集重写形式主义，它表明，协议的安全性仍然是不可判定的，即使在相当严格的限制放在协议。特别是，即使数据构造函数、消息深度、消息宽度、不同角色的数量、角色长度和隐藏深度都由常数限制，保密性也是不可判定的属性。如果协议被进一步限制为没有新数据（随机数），那么保密性是dexptime完全的。这两个下界都是通过将不含函数符号的存在Horn理论中的决策问题编码到我们的协议框架中来获得的。在约简中使用加密和对手行为的方式为协议分析提供了一些启示。
Using a multiset rewriting formalism with existen-tial quantiication, it is shown that protocol security remains undecidable even when rather severe restrictions are placed on protocols. In particular, even if data constructors, message depth, message width, number of distinct roles, role length, and depth of encryp-tion are bounded by constants, secrecy is an undecidable property. If protocols are further restricted to have no new data (nonces), then secrecy is dexptime-complete. Both lower bounds are obtained by encoding decision problems from existential Horn theories without function symbols into our protocol framework. The way that encryption and adversary behavior are used in the reduction sheds some light on protocol analysis.