PROTOCOL ANALYSIS USING MAUDE-NPA

Santiago Escobar (Universitat Politècnica de València)

In this course we give an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the symbolic analysis of cryptographic protocols.

It searches backwards from an insecure pattern configuration and it is able to find an attack, given enough resources, or prove the absence of any attack, when the search space is finite, which happens quite often thanks to many optimisation techniques. Several properties can be checked with Maude-NPA: secrecy, authentication, and indistinguishability for an active Dolev-Yao intruder model and an unbounded number of sessions.

Maude-NPA takes into account the algebraic properties of the crypto systems involved (e.g., exclusive-or, Diffie-Hellman, Bilinear Pairings, etc.) in order to give a more complete representation of both the protocol and the attackers capabilities. During the development of the tool we have also defined new theoretical and practical frameworks such as variant-based unification, logical model checking, asymmetric unification, or state-space optimisations that will be presented during the course. Maude-NPA has been recently extended to handle properties checked using SMT solvers: such as time and space constraints.