Inductive Proofs of Computational Secrecy
Arnab Roy

Citation
Arnab Roy. "Inductive Proofs of Computational Secrecy". Talk or presentation, 11, October, 2007.

Abstract
Secrecy properties of network protocols assert that no probabilistic polynomial-time distinguisher can win a suitable game presented by a challenger. Because such properties are not determined by trace-by-trace behavior of the protocol, we establish a trace-based protocol condition, suitable for inductive proofs, that guarantees a generic reduction from protocol attacks to attacks on underlying primitives. We use this condition to present a compositional inductive proof system for secrecy, and illustrate the system by giving a modular, formal proof of computational authentication and secrecy properties of Kerberos V5.

Electronic downloads

Confidential. This publication has been marked by the author for Trust-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Arnab Roy. <a
  href="http://www.truststc.org/pubs/305.html"
  ><i>Inductive Proofs of Computational
  Secrecy</i></a>, Talk or presentation,  11,
  October, 2007.

• Plain text

  Arnab Roy. "Inductive Proofs of Computational
  Secrecy". Talk or presentation,  11, October, 2007.

• BibTeX

  @presentation{Roy07_InductiveProofsOfComputationalSecrecy,
      author = {Arnab Roy},
      title = {Inductive Proofs of Computational Secrecy},
      day = {11},
      month = {October},
      year = {2007},
      abstract = {Secrecy properties of network protocols assert
                that no probabilistic polynomial-time
                distinguisher can win a suitable game presented by
                a challenger. Because such properties are not
                determined by trace-by-trace behavior of the
                protocol, we establish a trace-based protocol
                condition, suitable for inductive proofs, that
                guarantees a generic reduction from protocol
                attacks to attacks on underlying primitives. We
                use this condition to present a compositional
                inductive proof system for secrecy, and illustrate
                the system by giving a modular, formal proof of
                computational authentication and secrecy
                properties of Kerberos V5.},
      URL = {http://www.truststc.org/pubs/305.html}
  }
  

Posted by Larry Rohrbough on 16 Oct 2007.
For additional information, see the Publications FAQ or contact webmaster at www truststc org..