Paper 2025/2243 Original: eprint.iacr.org/2025/2243 ↗
On The Dolev-Yao Model of Symmetric Cascade Protocol
Abstract
Security protocols enable authentication, key distribution, and secure information exchange, making them essential for network security, yet flaws in their design can lead to attacks. To prevent this, formal verification methods are vital for analyzing protocol correctness. The Dolev–Yao (DY) \cite{Dy} model introduced formalization for name-stamp and cascade protocols, where users apply public-key operations on messages. Brook and Otto \cite{DY-extension} later distinguished between symmetric and non-symmetric cascade protocols, noting that all DY cases were symmetric and that attacker choices were not fully addressed. They highlighted the incomplete characterization of an attacker’s power as an open problem. In this work, we extend the DY model by systematically analyzing all remaining symmetric two-party cascade protocol cases, aiming to provide a more complete foundation for building formal verification tools.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2025-12-13: last updated
- 2025-12-13: published
- Short URL
- https://ia.cr/2025/2243
- License
- https://creativecommons.org/licenses/by-nc/4.0/
BibTeX
@misc{cryptoeprint:2025/2243,
author = {Varsha Jarali and Shashi Kant Pandey},
title = {On The Dolev-Yao Model of Symmetric Cascade Protocol},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/2243},
year = {2025},
url = {https://eprint.iacr.org/2025/2243}
}