Home   >   Demonstrators   >   MAUDE-NPA

Maude-NPA

Demonstrator|vrain

Description
Maude-NPA is the state-of-the-art for the analysis of cryptographic protocols
Member
Address
Camino de Vera S/N
Province
Valencia

DEMONSTRATOR INFORMATION

DESCRIPTION

Maude-NPA is an analysis tool for cryptographic protocols that takes into account many of the algebraic properties of crypto systems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), exponentiation, and homomorphic encryption. Maude-NPA uses an approach similar to the original NRL Protocol Analyzer; it is based on unification, and performs backwards search from a final state to determine whether or not it is reachable. Unlike the original NPA, it has a theoretical basis in rewriting logic and narrowing, and offers support for a wider basis of equational theories that includes commutative (C), associative-commutative (AC), and associative-commutative-identity (ACU) theories.

POSSIBILITIES

Protocols are introduced in a process algebra or strand space notation. The tools is able to prove or disprove secrecy, authentication and indistinguishability security properties. If a property is disproved, a concrete attack sequence is returned. If a property is proved, a complete analysis must be performed, which may require enough time and memory to be accomplished.

TECHNOLOGICAL ENABLER

Artificial Intelligence and Computing
Data security and privacy technologies

Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models