Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories

DOI10.1007/978-3-319-25527-9_16MaRDI QIDQ3460872zbMATH OpenOpenAlexFDO

Authors Santiago Escobar, José Meseguer, Sonia Santiago, Catherine Meadows

Publication date 8 January 2016

Published in Programming Languages with Applications to Biology and Security (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-25527-9_16

Mathematics Subject Classification ID

Equational classes, universal algebra in model theory (03C05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Cryptography (94A60)

Recommendations

• Symbolic protocol analysis for monoidal equational theories
• Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method
• Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or
• An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
• Canonical narrowing with irreducibility constraints as a symbolic protocol analysis method
• Symbolic execution as DPLL modulo theories
• scientific article; zbMATH DE number 1629965
• scientific article; zbMATH DE number 1759597
• Symbolic Model Checking Commitment Protocols Using Reduction

Cites work

• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Automated verification of selected equivalences for security protocols
• Combination techniques and decision problems for disunification
• Conditional rewriting logic as a unified model of concurrency
• Equational problems and disunification
• Folding variant narrowing and optimal variant termination
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 176756 (Why is no real title available?)
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• On the security of public key protocols
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Term Rewriting and Applications
• Using encryption for authentication in large networks of computers

Cited in

(7)

• Extending H₁-clauses with disequalities
• Protocol analysis with time
• Protocol analysis with time and space
• Generalized rewrite theories, coherence completion, and symbolic methods
• Symbolic protocol analysis for monoidal equational theories
• Strand spaces with choice via a process algebra semantics
• Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method

Describes a project that uses

Uses Software

• Maude-NPA

This page was built for publication: Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories

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