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

DOI10.1007/S10817-010-9188-8zbMATH Open1213.94119OpenAlexW2053014980WikidataQ60530316 ScholiaQ60530316MaRDI QIDQ540685FDOQ540685

Tomasz Truderung, Ralf Küsters

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

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

zbMATH Keywords

automated verificationsecurity protocolsXOR

Mathematics Subject Classification ID

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

Cites Work

• Automated Deduction – CADE-20
• Automated verification of selected equivalences for security protocols
• An NP decision procedure for protocol insecurity with XOR
• Title not available (Why is that?)
• On the Security of PKCS #11
• Automatic Analysis of the Security of XOR-Based Key Management Schemes
• Title not available (Why is that?)
• Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach
• Term Rewriting and Applications
• Security properties: two agents are sufficient
• Session Key Distribution Using Smart Cards
• On the Automatic Analysis of Recursive Security Protocols with XOR
• Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case
• Automated Deduction – CADE-20

Cited In (8)

• Automated Deduction – CADE-20
• An NP decision procedure for protocol insecurity with XOR
• Automatic Analysis of the Security of XOR-Based Key Management Schemes
• On the Automatic Analysis of Recursive Security Protocols with XOR
• 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
• Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach

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)