Sciweavers

JCS
2010

Inductive trace properties for computational security

13 years 2 months ago
Inductive trace properties for computational security
Protocol authentication properties are generally trace-based, meaning that authentication holds for the protocol if authentication holds for individual traces (runs of the protocol and adversary). Computational secrecy conditions, on the other hand, often are not trace based: the ability to computationally distinguish a system that transmits a secret from one that does not is measured by overall success on the set of all traces of each system. This presents a challenge for inductive or compositional methods: induction is a natural way of reasoning about traces of a system, but it does not appear directly applicable to non-trace properties. We therefore investigate the semantic connection between trace properties that could be established by induction and non-trace-based security requirements. Specifically, we prove that a certain trace property implies computational secrecy and authentication properties, assuming the encryption scheme provides chosen ciphertext security and ciphertex...
Arnab Roy, Anupam Datta, Ante Derek, John C. Mitch
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JCS
Authors Arnab Roy, Anupam Datta, Ante Derek, John C. Mitchell
Comments (0)