Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
From MaRDI portal
Publication:5195250
DOI10.6092/issn.1972-5787/3720zbMath1451.68334OpenAlexW1488277732MaRDI QIDQ5195250
Mauricio Ayala-Rincón, Unnamed Author
Publication date: 18 September 2019
Full work available at URL: https://doaj.org/article/767e571c84044efa805d9f4f91c1d389
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Computer security (68M25)
Uses Software
Cites Work
- Unnamed Item
- An attack on the Needham-Schroeder public-key authentication protocol
- Deciding knowledge in security protocols under equational theories
- Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
- Computer security -- ESORICS 2000. 6th European symposium on research in computer security, Toulouse, France, October 4--6, 2000. Proceedings
- Modelling Attacker’s Knowledge for Cascade Cryptographic Protocols
- Models and Proofs of Protocol Security: A Progress Report
- On the security of public key protocols
- Using encryption for authentication in large networks of computers
- Computer-Aided Security Proofs for the Working Cryptographer
- Formal certification of code-based cryptographic proofs
- Computer Aided Verification
This page was built for publication: Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
