DeepSec：判定安全协议的等价性质——改进的理论与实践
DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
AI总结：
本文针对密码协议隐私验证中的等价判定问题，提出新的复杂性结果和有界会话下的判定过程，并实现为工具DeepSec，实验证明其效率更高且可分析协议范围更广。
摘要：
自动化验证已成为密码协议安全评估中不可或缺的组成部分。在此背景下，隐私类属性通常通过不可区分性语句来建模，并在进程演算中表示为行为等价。本文对这一验证问题的理论和实践均作出了贡献。我们为静态等价、迹等价和带标签互模拟建立了新的复杂性结果，并针对协议会话数量有界的情形给出了这些等价的判定过程。我们的过程是第一个能够对大量密码学原语——即那些可由子项收敛的析构重写系统表示的原语——精确判定迹等价和带标签互模拟的方法。我们还在新工具DeepSec中实现了该过程。通过大量实验，我们表明该工具在效率上显著优于其他同类工具，同时扩大了可分析协议的范围。
英文摘要：
Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
