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