Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach

DOI10.1007/S10817-010-9188-8MaRDI QIDQ540685zbMATH OpenOpenAlexWikidataFDO

Authors Ralf Küsters, Tomasz Truderung

Publication date 3 June 2011

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9188-8

zbMATH Keywords

automated verificationsecurity protocolsXOR

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• An NP decision procedure for protocol insecurity with XOR
• On the Automatic Analysis of Recursive Security Protocols with XOR
• Limits of the cryptographic realization of Dolev-Yao-style XOR
• Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or
• Automatic Analysis of the Security of XOR-Based Key Management Schemes

Cites work

• scientific article; zbMATH DE number 2043527 (Why is no real title available?)
• scientific article; zbMATH DE number 1882021 (Why is no real title available?)
• An NP decision procedure for protocol insecurity with XOR
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Automated verification of selected equivalences for security protocols
• Automatic Analysis of the Security of XOR-Based Key Management Schemes
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• On the Automatic Analysis of Recursive Security Protocols with XOR
• On the security of PKCS \#11.
• Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
• Security properties: two agents are sufficient
• Session key distribution using smart cards
• Term Rewriting and Applications

Cited in

(9)

• Automated Deduction – CADE-20
• Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
• On the Automatic Analysis of Recursive Security Protocols with XOR
• Limits of the cryptographic realization of Dolev-Yao-style XOR
• An NP decision procedure for protocol insecurity with XOR
• Automatic Analysis of the Security of XOR-Based Key Management Schemes
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif
• Satisfiability of general intruder constraints with and without a set constructor

Describes a project that uses

Uses Software

• ProVerif

This page was built for publication: Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach

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