Paper 2023/1329

Layered Symbolic Security Analysis in DY$^\star$

Karthikeyan Bhargavan, French Institute for Research in Computer Science and Automation
Abhishek Bichhawat, Indian Institute of Technology Gandhinagar
Pedram Hosseyni, University of Stuttgart
Ralf Kuesters, University of Stuttgart
Klaas Pruiksma, University of Stuttgart
Guido Schmitz, Royal Holloway University of London
Clara Waldmann, University of Stuttgart
Tim Würtele, University of Stuttgart

While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY$^\star$ protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F$^\star$ modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY$^\star$ with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest.

Available format(s)
Publication info
Published elsewhere. Minor revision. ESORICS 2023
formal security analysisDY*protocol analysis
Contact author(s)
karthikeyan bhargavan @ inria fr
abhishek b @ iitgn ac in
pedran hosseyni @ sec uni-stuttgart de
ralf kuesters @ sec uni-stuttgart de
klaas pruiksma @ sec uni-stuttgart de
guido schmitz @ rhul ac uk
clara waldmann @ sec uni-stuttgart de
tim wuertele @ sec uni-stuttgart de
2023-09-08: approved
2023-09-06: received
See all versions
Short URL
Creative Commons Attribution


      author = {Karthikeyan Bhargavan and Abhishek Bichhawat and Pedram Hosseyni and Ralf Kuesters and Klaas Pruiksma and Guido Schmitz and Clara Waldmann and Tim Würtele},
      title = {Layered Symbolic Security Analysis in DY$^\star$},
      howpublished = {Cryptology ePrint Archive, Paper 2023/1329},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.