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.

翻译：自动核查已成为加密协议安全评估的一个基本部分。 在这方面,隐私类型特性通常以不可分性声明为模型,在过程微积分中以行为等同形式表示。在本文件中,我们既促进这一核查问题的理论和实践。我们为静态等同、痕量等同和标签为两样性确定了新的复杂结果,并为受约束的协议会议规定了这些等同性的决定程序。我们的程序是第一个决定追踪等同和标注两样性的程序,它完全针对大量各种加密原始生物 -- -- 可以用子术语集合的销毁者重写系统来代表。我们还在一个新的工具 " 深层安全 " 中实施了该程序。我们通过广泛的实验表明,它比其他类似工具效率高得多,同时提高了可以分析的协议的范围。