Maude-NPA

swMATH12159MaRDI QIDQ24090FDOQ24090

Author name not available (Why is that?)

Described by source

• State space reduction in the Maude-NRL protocol analyzer

Cited In (31)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Twenty years of rewriting logic
• Intruder deduction problem for locally stable theories with normal forms and inverses
• Symbolic computation in Maude: some tapas
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Tree automata for detecting attacks on protocols with algebraic cryptographic primitives
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Terminating non-disjoint combined unification
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
• Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
• Efficient general AGH-unification
• Title not available (Why is that?)
• Title not available (Why is that?)
• A reduced semantics for deciding trace equivalence
• Automated verification of equivalence properties of cryptographic protocols
• Programming and symbolic computation in Maude
• Order-sorted equational unification revisited
• Optimization of rewrite theories by equational partial evaluation
• Model Checking Security Protocols
• Computing knowledge in equational extensions of subterm convergent theories
• Efficient general unification for XOR with homomorphism
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• Variant narrowing and equational unification
• José Meseguer: scientist and friend extraordinaire
• Combining proverif and automated theorem provers for security protocol verification
• Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
• Two Decades of Maude
• Built-in variant generation and unification, and their applications in Maude 2.7
• Bounded ACh unification
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

This page was built for software: Maude-NPA