Dynamic Tags for Security Protocols
Myrto Arapinis (School of Computer Science, University of Birmingham),, St\'ephanie Delaune (LSV, CNRS & ENS Cachan), Steve Kremer (INRIA Nancy -, Grand-Est)

TL;DR
This paper introduces a transformation technique that allows security protocols secure in a single session to be proven secure for an unbounded number of sessions, simplifying the design and verification process.
Contribution
It presents a method to convert protocols secure in bounded sessions into protocols secure in unbounded sessions, facilitating scalable security verification.
Findings
A transformation maps single-session security to unbounded-session security.
For many classical properties, a single session suffices for security proofs.
The approach provides a practical design strategy for scalable security protocols.
Abstract
The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
