Erik Pallas
, Helmholtz Center for Information Security
Aleksi Peltonen, Helmholtz Center for Information Security
Although automated symbolic protocol verification has proven valuable and effective, current approaches begin to reach their limits: While small protocols can be analyzed automatically, the most complex case studies often require substantial expert time and resources. There have been many attempts to solve this problem by compositional verification, but they rely on unrealistic protocol assumptions and do not support real-world security properties like Forward Secrecy. In this work, we enable compositional symbolic analysis for real-world security protocols with respect to modern security properties. We develop a composition result in the Applied π-Calculus that holds even in the presence of attackers capable of dynamic corruption if the protocols satisfy a disjointness requirement. We demonstrate the applicability and effectiveness of our result on the composition of a data exchange protocol with a Diffie-Hellman key exchange and a compositional analysis of Forward Secrecy in TLS 1.3 within the scope of RFC 8446 and the ECH extension. While monolithic analyses of TLS 1.3 with ECH fail to deliver a result in 10% of cases, all compositional analyses succeed. Additionally, runtime decreases by 71% and memory usage by 86% on average.
BibTeX
@misc{cryptoeprint:2026/900,
author = {Cas Cremers and Erik Pallas and Aleksi Peltonen},
title = {Secure Protocol Composition under Dynamic Corruption: Scaling Up Symbolic Analysis for Real-World Security Properties},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/900},
year = {2026},
url = {https://eprint.iacr.org/2026/900}
}
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。