Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures

DOI10.1016/J.TCS.2009.10.022MaRDI QIDQ2268100zbMATH OpenOpenAlexFDO

Authors Yannick Chevalier, Michaël Rusinowitch

Publication date 10 March 2010

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2009.10.022

zbMATH Keywords

cryptographic protocolsequational theoriescombination of decision proceduresDolev-Yao intruder

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Recommendations

• Automata, Languages and Programming
• Hierarchical Combination of Intruder Theories
• Hierarchical combination of intruder theories
• Algebraic Intruder Deductions
• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 1948405 (Why is no real title available?)
• scientific article; zbMATH DE number 1754628 (Why is no real title available?)
• Complexity of nilpotent unification and matching problems.
• Computer Aided Verification
• Easy intruder deductions
• Foundations of Software Science and Computation Structures
• Mathematical Foundations of Computer Science 2003
• Mobile values, new names, and secure communication
• On the freedom of decryption
• On the security of public key protocols
• On the symbolic reduction of processes with cryptographic functions.
• Programming Languages and Systems
• Programming Languages and Systems
• STACS 2004
• The NRL Protocol Analyzer: An Overview
• Unification in a combination of arbitrary disjoint equational theories
• Unification in the union of disjoint equational theories: Combining decision procedures

Cited in

(5)

• Deducibility constraints and blind signatures
• Hierarchical combination of intruder theories
• Satisfiability of general intruder constraints with and without a set constructor
• Automata, Languages and Programming
• Hierarchical Combination of Intruder Theories

Describes a project that uses

Uses Software

• NRL
• AVISPA

This page was built for publication: Symbolic protocol analysis in the union of disjoint intruder theories: combining decision procedures

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