Standard
Layered Symbolic Security Analysis in DY*. / Bhargavan, Karthikeyan; Bichhawat, Abhishek; Hosseyni, Pedram et al.
Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings. ed. / Gene Tsudik; Mauro Conti; Kaitai Liang; Georgios Smaragdakis. 2024. p. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14346 LNCS).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Bhargavan, K, Bichhawat, A, Hosseyni, P, Küsters, R, Pruiksma, K
, Schmitz, G, Waldmann, C & Würtele, T 2024,
Layered Symbolic Security Analysis in DY*. in G Tsudik, M Conti, K Liang & G Smaragdakis (eds),
Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14346 LNCS, pp. 3-21.
https://doi.org/10.1007/978-3-031-51479-1_1APA
Bhargavan, K., Bichhawat, A., Hosseyni, P., Küsters, R., Pruiksma, K.
, Schmitz, G., Waldmann, C., & Würtele, T. (2024).
Layered Symbolic Security Analysis in DY*. In G. Tsudik, M. Conti, K. Liang, & G. Smaragdakis (Eds.),
Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings (pp. 3-21). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14346 LNCS).
https://doi.org/10.1007/978-3-031-51479-1_1Vancouver
Bhargavan K, Bichhawat A, Hosseyni P, Küsters R, Pruiksma K
, Schmitz G et al.
Layered Symbolic Security Analysis in DY*. In Tsudik G, Conti M, Liang K, Smaragdakis G, editors, Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings. 2024. p. 3-21. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-51479-1_1
Author
Bhargavan, Karthikeyan ; Bichhawat, Abhishek ; Hosseyni, Pedram et al. /
Layered Symbolic Security Analysis in DY*. Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings. editor / Gene Tsudik ; Mauro Conti ; Kaitai Liang ; Georgios Smaragdakis. 2024. pp. 3-21 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Bibtex
@inproceedings{bb677218141d486e85df364381e50b0f,
title = "Layered Symbolic Security Analysis in DY*",
abstract = "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 ⋆ protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F ⋆ 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 ⋆ 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.",
author = "Karthikeyan Bhargavan and Abhishek Bichhawat and Pedram Hosseyni and Ralf K{\"u}sters and Klaas Pruiksma and Guido Schmitz and Clara Waldmann and Tim W{\"u}rtele",
year = "2024",
month = jan,
day = "12",
doi = "10.1007/978-3-031-51479-1_1",
language = "English",
isbn = "9783031514784",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "3--21",
editor = "Gene Tsudik and Mauro Conti and Kaitai Liang and Georgios Smaragdakis",
booktitle = "Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings",
}
RIS
TY - GEN
T1 - Layered Symbolic Security Analysis in DY*
AU - Bhargavan, Karthikeyan
AU - Bichhawat, Abhishek
AU - Hosseyni, Pedram
AU - Küsters, Ralf
AU - Pruiksma, Klaas
AU - Schmitz, Guido
AU - Waldmann, Clara
AU - Würtele, Tim
PY - 2024/1/12
Y1 - 2024/1/12
N2 - 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
⋆ protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F
⋆ 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
⋆ 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.
AB - 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
⋆ protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F
⋆ 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
⋆ 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.
U2 - 10.1007/978-3-031-51479-1_1
DO - 10.1007/978-3-031-51479-1_1
M3 - Conference contribution/Paper
SN - 9783031514784
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 21
BT - Computer Security – ESORICS 2023 - 28th European Symposium on Research in Computer Security, 2023, Proceedings
A2 - Tsudik, Gene
A2 - Conti, Mauro
A2 - Liang, Kaitai
A2 - Smaragdakis, Georgios
ER -
