决定密码协议的安全属性。关键周期的应用
Deciding security properties for cryptographic protocols. Application to key cycles
摘要：
有大量的工作致力于安全协议的形式化验证。在本文中，我们重新审视和扩展的NP-完全决策过程有限的会话数。我们使用一个，现在的标准，演绎约束形式主义建模的安全协议。我们的第一个贡献是给出一组简单的约束简化规则，它允许将任何演绎约束系统减少到一组解决的形式，代表所有的解决方案（在会话的范围内）。因此，我们证明，决定存在的关键周期是NP-完全的有限数量的会话。键环的问题已经提出了最近的工作有关的计算和符号模型。所谓的符号模型的可靠性实际上要求没有关键周期（例如，enc（k，k））在协议的执行中发生。否则，需要更强的安全性假设（如KDM安全性）。我们表明，我们的决策过程也可以应用于再次证明的可判定性的认证类属性和可判定性的一个显着的片段的协议与时间戳。
英文摘要：
There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraints formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint system to a set of solved forms, representing all solutions (within the bound on sessions). As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k,k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required. We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
