Modeling and analysis of advanced cryptographic primitives and security protocols in maude-npa
- Autores: Damián Aparicio Sánchez
- Directores de la Tesis: Santiago Escobar Román (dir. tes.)
- Lectura: En la Universitat Politècnica de València ( España ) en 2022
- Idioma: español
- Tribunal Calificador de la Tesis: Salvador Lucas Alba (presid.) , María del Mar Gallardo Melgarejo (secret.) , Alberto Lluch Lafuente (voc.)
- Enlaces
- Tesis en acceso abierto en: RiuNet
- Resumen
The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption.
In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools.
