Sapic+ : protocol verifiers of the world, unite!
Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. Sapic+ : protocol verifiers of the world, unite!. In 31st USENIX Security Symposium (USENIX Security'22), pp. 3935–3952, USENIX Association, Boston, USA, August 2022.
Download
Abstract
Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic+ , we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with automated translations from Sapic+ to ProVerif and DeepSec, as well as powerful, protocol-independent optimizations of the existing translation. We prove each part of these translations sound. A user can thus, with a single Sapic+ file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models. This includes a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic + we demonstrate the effectiveness of our approach. Moreover, we study four new case studies: the LAKE and the Privacy-Pass protocols, both under standardization, the SSH protocol with the agent-forwarding feature, and the recent KEMTLS protocol, a post-quantum version of the main TLS key exchange.
BibTeX
@inproceedings{CJKK-usenix22,
abstract = {Symbolic security protocol verifiers have reached a
high degree of automation and maturity. Today,
experts can model real-world protocols, but this
often requires model-specific encodings and deep
insight into the strengths and weaknesses of each of
those tools. With Sapic+ , we introduce a protocol
verification platform that lifts this burden and
permits choosing the right tool for the job, at any
development stage. We build on the existing compiler
from Sapic to Tamarin, and extend it with automated
translations from Sapic+ to ProVerif and DeepSec, as
well as powerful, protocol-independent optimizations
of the existing translation. We prove each part of
these translations sound. A user can thus, with a
single Sapic+ file, verify reachability and
equivalence properties on the specified protocol,
either using ProVerif, Tamarin or DeepSec. Moreover,
the soundness of the translation allows to directly
assume results proven by another tool which allows
to exploit the respective strengths of each tool. We
demonstrate our approach by analyzing various
existing models. This includes a large case study of
the 5G authentication protocols, previously analyzed
in Tamarin. Encoding this model in Sapic + we
demonstrate the effectiveness of our
approach. Moreover, we study four new case studies:
the LAKE and the Privacy-Pass protocols, both under
standardization, the SSH protocol with the
agent-forwarding feature, and the recent KEMTLS
protocol, a post-quantum version of the main TLS key
exchange.},
address = {Boston, USA},
author = {Cheval, Vincent and Jacomme, Charlie and Kremer,
Steve and K{\"{u}}nnemann, Robert},
booktitle = {31st USENIX Security Symposium ({USENIX}
Security'22)},
month = aug,
pages = {3935--3952},
publisher = {{USENIX} Association},
title = {Sapic+ : protocol verifiers of the world, unite!},
year = 2022,
acronym = {{USENIX} Security'22},
nmonth = 8,
}