Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories

DOI10.1007/978-3-319-25527-9_16zbMath1437.94060OpenAlexW2296667264MaRDI QIDQ3460872

José Meseguer, Sonia Santiago, Santiago Escobar, Catherine A. 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

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

Related Items (4)

Protocol analysis with time ⋮ Protocol analysis with time and space ⋮ Strand spaces with choice via a process algebra semantics ⋮ Generalized rewrite theories, coherence completion, and symbolic methods

Uses Software

• Maude-NPA

Cites Work

• Unnamed Item
• Unnamed Item
• Combination techniques and decision problems for disunification
• 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
• Equational problems and disunification
• Conditional rewriting logic as a unified model of concurrency
• Folding variant narrowing and optimal variant termination
• Automated verification of selected equivalences for security protocols
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• Term Rewriting and Applications

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