swMATH12159MaRDI QIDQ24090FDOQ24090
Author name not available (Why is that?)
Official website: http://maude.cs.uiuc.edu/tools/Maude-NPA/
Cited In (63)
- 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?)
- FAST
- Maude
- ProVerif
- Timbuk
- 2OBJ
- PMaude
- PAGODA
- OFMC
- SATMC
- scyther
- HI-maude
- K-Maude
- MFE
- ITP
- MTT
- CARIBOO
- Anima
- InvA
- NRL
- vlogsl
- FreshML
- A reduced semantics for deciding trace equivalence
- Automated verification of equivalence properties of cryptographic protocols
- Akiss
- Apte
- Programming and symbolic computation in Maude
- SymPLFIED
- TAMARIN
- Order-sorted equational unification revisited
- margrave
- Z3str2
- ABETS
- ACUOS2
- KOOL
- CPSA
- Optimization of rewrite theories by equational partial evaluation
- GLINTS
- 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
