Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method

DOI10.1007/978-3-031-12441-9_3MaRDI QIDQ6487294zbMATH OpenFDO

Authors Raúl López-Rueda, Santiago Escobar

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-12441-9_3

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• S-narrowing for constructor systems
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA

Cites work

• Asymmetric unification: a new unification paradigm for cryptographic protocol analysis
• Automated verification of equivalence properties of cryptographic protocols
• Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method
• Completion of a Set of Rules Modulo a Set of Equations
• Conditional rewriting logic as a unified model of concurrency
• Folding variant narrowing and optimal variant termination
• Generalized rewrite theories, coherence completion, and symbolic methods
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 1394315 (Why is no real title available?)
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Protocol analysis with time
• State space reduction in the Maude-NRL protocol analyzer
• Strict coherence of conditional rewriting modulo axioms
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Term Rewriting and Applications

Cited in

(4)

• Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
• Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA

This page was built for publication: Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6487294)