Computing knowledge in equational extensions of subterm convergent theories

DOI10.1017/S0960129520000031MaRDI QIDQ5139279zbMATH OpenFDO

Authors Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen

Publication date 8 December 2020

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

Full work available at URL https://doi.org/10.1017/S0960129520000031

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)

Recommendations

• Computing knowledge in security protocols under convergent equational theories
• Computing Knowledge in Security Protocols under Convergent Equational Theories
• Decidability of equational theories for subsignatures of relation algebra
• scientific article; zbMATH DE number 67036
• On computable formal concepts in computable formal contexts
• scientific article; zbMATH DE number 4041328
• Partial completion of equational theories
• Confluent term rewriting for only-knowing logics
• Knowledge representation and reasoning based on computability logic

Cites work

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

Cited in

(4)

• YAPA: A Generic Tool for Computing Intruder Knowledge
• Terminating non-disjoint combined unification
• Graph-embedded rewrite systems: combination and undecidability results
• YAPA: a generic tool for computing intruder knowledge

Describes a project that uses

Uses Software

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

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

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