DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice. TheoretiCS, 3, 2024.
doi:10.46298/theoretics.24.4
Download
Abstract
Automated verification has become an essential part in the securityevaluation of cryptographic protocols. In this context privacy-type propertiesare often modelled by indistinguishability statements, expressed as behaviouralequivalences in a process calculus. In this paper we contribute both to thetheory and practice of this verification problem. We establish new complexityresults for static equivalence, trace equivalence and labelled bisimilarity andprovide a decision procedure for these equivalences in the case of a boundednumber of protocol sessions. Our procedure is the first to decide traceequivalence and labelled bisimilarity exactly for a large variety ofcryptographic primitives -- those that can be represented by a subtermconvergent destructor rewrite system. We also implemented the procedure in anew tool, DeepSec. We showed through extensive experiments that it issignificantly more efficient than other similar tools, while at the same timeraises the scope of the protocols that can be analysed.
BibTeX
@Article{CKR-theoretics24,
abstract = {Automated verification has become an essential part in the securityevaluation of cryptographic protocols. In this context privacy-type propertiesare often modelled by indistinguishability statements, expressed as behaviouralequivalences in a process calculus. In this paper we contribute both to thetheory and practice of this verification problem. We establish new complexityresults for static equivalence, trace equivalence and labelled bisimilarity andprovide a decision procedure for these equivalences in the case of a boundednumber of protocol sessions. Our procedure is the first to decide traceequivalence and labelled bisimilarity exactly for a large variety ofcryptographic primitives -- those that can be represented by a subtermconvergent destructor rewrite system. We also implemented the procedure in anew tool, DeepSec. We showed through extensive experiments that it issignificantly more efficient than other similar tools, while at the same timeraises the scope of the protocols that can be analysed.},
author = {Cheval, Vincent and Kremer, Steve and Rakotonirina, Itsaka},
title = {DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice},
journal = {{TheoretiCS}},
volume = {3},
year = 2024,
doi = {10.46298/theoretics.24.4},
url = {https://theoretics.episciences.org/13221},
}