Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses

DOI10.1007/978-3-540-71322-7_5MaRDI QIDQ3593070zbMATH OpenOpenAlexFDO

Authors Helmut Seidl, Kumar Neeraj Verma

Publication date 24 September 2007

Published in Program Analysis and Compilation, Theory and Practice (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71322-7_5

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• Flat and one-variable clauses: complexity of verifying cryptographic protocols with single blind copying
• Logic for Programming, Artificial Intelligence, and Reasoning
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Automated Deduction – CADE-20
• Protocol Verification Via Rigid/Flexible Resolution

Cited in

(11)

• Verification of cryptographic protocols: tagging enforces termination
• SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
• LACPV'2001. Logical aspects of cryptographic protocol verification. Proceedings of the 1st workshop (a satellite workshop of CAV'01), Paris, France, July 23, 2001.
• Finite Models in FOL-Based Crypto-Protocol Verification
• Protocol Verification Via Rigid/Flexible Resolution
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Tractable inference systems: an extension with a deducibility predicate
• Flat and one-variable clauses: complexity of verifying cryptographic protocols with single blind copying
• Automated Deduction – CADE-20
• Iterative Specialisation of Horn Clauses
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Cryptographic Protocol Verification Using Tractable Classes of Horn Clauses

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