Ayala-Rincón, M. and Santos Rego, Y. 2013. Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model. Journal of Formalized Reasoning. 6, 1 (Jan. 2013), 31–61. DOI:https://doi.org/10.6092/issn.1972-5787/3720.