Paper 2006/486

Inductive Trace Properties for Computational Security

Arnab Roy, Anupam Datta, Ante Derek, and John C. Mitchell


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 \textit{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 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 ciphertext integrity. We also prove a similar theorem for computational secrecy assuming Decisional Diffie-Hellman and a chosen plaintext secure encryption scheme.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Manuscript
Contact author(s)
arnab @ stanford edu
2006-12-29: received
Short URL
Creative Commons Attribution


      author = {Arnab Roy and Anupam Datta and Ante Derek and John C.  Mitchell},
      title = {Inductive Trace Properties for Computational Security},
      howpublished = {Cryptology ePrint Archive, Paper 2006/486},
      year = {2006},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.