Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties

DOI10.1007/978-3-642-03829-7_1zbMath1252.94061OpenAlexW1536580911MaRDI QIDQ3184784

Santiago Escobar, José Meseguer, Catherine A. Meadows

Publication date: 22 October 2009

Published in: Foundations of Security Analysis and Design V (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03829-7_1

Mathematics Subject Classification ID

Cryptography (94A60)

Related Items (38)

Model Checking Security Protocols ⋮ Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ Secure key management policies in strand spaces ⋮ Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Modular verification of protocol equivalence in the presence of randomness ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ José Meseguer: Scientist and Friend Extraordinaire ⋮ Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude ⋮ Alice and Bob Meet Equational Theories ⋮ Two Decades of Maude ⋮ Twenty years of rewriting logic ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Optimizing Maude programs via program specialization ⋮ Strand spaces with choice via a process algebra semantics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Efficient general AGH-unification ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ Bounded ACh unification ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Intruder deduction problem for locally stable theories with normal forms and inverses ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Efficient General Unification for XOR with Homomorphism ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas ⋮ Terminating non-disjoint combined unification

Uses Software

• YAPA
• AVISPA
• Maude
• OFMC
• SATMC
• NRL
• Maude-NPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An attack on a recursive authentication protocol. A cautionary tale
• Deciding knowledge in security protocols under equational theories
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• On the freedom of decryption
• Conditional rewriting logic as a unified model of concurrency
• Unification modulo ACUI plus distributivity axioms
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Hierarchical combination of intruder theories
• The NRL Protocol Analyzer: An Overview
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Effectively Checking the Finite Variant Property
• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
• YAPA: A Generic Tool for Computing Intruder Knowledge
• On the security of public key protocols
• Variant Narrowing and Equational Unification
• Computing Knowledge in Security Protocols under Convergent Equational Theories
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Information and Communications Security
• Term Rewriting and Applications
• Computer Aided Verification

This page was built for publication: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties