Computing knowledge in equational extensions of subterm convergent theories

DOI10.1017/S0960129520000031zbMath1495.68113MaRDI QIDQ5139279

Serdar Erbatur, Christophe Ringeissen, Andrew M. Marshall

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

deductiondecision proceduresequational theoriessecurity protocolsstatic equivalence

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Computer security (68M25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Terminating non-disjoint combined unification

Uses Software

• YAPA
• AVISPA
• FAST
• ProVerif
• OFMC
• Maude-NPA
• Akiss

Cites Work

• Computing knowledge in security protocols under convergent equational theories
• Decidability and combination results for two notions of knowledge in security protocols
• An NP decision procedure for protocol insecurity with XOR
• Intruder deduction problem for locally stable theories with normal forms and inverses
• Deciding knowledge in security protocols under equational theories
• Syntacticness, cycle-syntacticness and shallow theories
• Unification in permutative equational theories is undecidable
• Folding variant narrowing and optimal variant termination
• Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday
• Notions of knowledge in combinations of theories sharing constructors
• Hierarchical combination of intruder theories
• YAPA
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
• The CL-Atse Protocol Analyser
• Completion of a Set of Rules Modulo a Set of Equations
• Term Rewriting and All That
• Mobile values, new names, and secure communication
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Automated Verification of Equivalence Properties of Cryptographic Protocols
• Automata, Languages and Programming
• Term Rewriting and Applications
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computing knowledge in equational extensions of subterm convergent theories