Flat and one-variable clauses: complexity of verifying cryptographic protocols with single blind copying

DOI10.1145/1380572.1380577MaRDI QIDQ5277817zbMATH OpenOpenAlexFDO

Authors Helmut Seidl, Kumar Neeraj Verma

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1380572.1380577

zbMATH Keywords

cryptographic protocolsfirst-order logicHorn clausesinstantiation-based theorem provingresolution

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Cryptography (94A60)

Recommendations

• Logic for Programming, Artificial Intelligence, and Reasoning
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses
• Automated Deduction – CADE-20
• Protocol Verification Via Rigid/Flexible Resolution

Cited in

(6)

• Extending \({\mathcal H}_1\)-clauses with path disequalities
• Protocol Verification Via Rigid/Flexible Resolution
• Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Automated Deduction – CADE-20
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Flat and one-variable clauses: complexity of verifying cryptographic protocols with single blind copying

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