Advanced Symbolic Methods for the Cryptographic Protocol Analyzer Maude-NPA
Abstract
This grant is part of a joint effort between the USAF and USN to advance the DoDs capability to perform protocol analysis. Formal analysis of cryptographic protocols is one of the most successful applications of formal methods in general and to security specifically. Over several years, Maude-NPA has been developed and refined by Catherine Meadows (Naval Research Laboratory, Washington DC, US), Jose Meseguer (University of Illinois at Urbana-Champaign, IL, US) and Santiago Escobar (Universitat Politecnica de Valencia, Spain). Additionally, a PhD student Damian Aparicio was working on the project during its last year. Maude-NPA is a publicly available protocol analyzer that uniquely takes into account many algebraic properties and relies on equational unification for the generation of the analysis search state space. During this grant period, the researchers were able to more fully establish the unification and satisfiability capabilities of the Maude programming language. They were also able to improve the Maude-NPA crypto tool during this period in order to more effectively manage complex protocols such as time-specific properties and distance-bounding protocols. Overall, this grant resulted in 5 published papers which improved the state-of-the-art in the area of formal protocol analysis in terms of both scientific contribution and usable tools.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 03, 2022
- Accession Number
- AD1175122
Entities
People
- Santiago Escobar-romain
Organizations
- Technical University of Valencia