Inicio   >   Demostradores   >   MAUDE-NPA

Maude-NPA

Demostrador|vrain

Descripción
Maude-NPA is the state-of-the-art for the analysis of cryptographic protocols
Miembro
dirección
Camino de Vera S/N
Provincia
Valencia

INFORMACIÓN DEL DEMOSTRADOR

DESCRIPCIÓN

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.

POSIBILIDADES

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.

HABILITADOR TECNOLOGICO

Inteligencia Artificial y Computación
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