Protocol-Independent Secrecy

Published in the proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, May, 2000.

---

Authors

Jon Millen and Harald Rueß

Abstract

Inductive proofs of secrecy invariants for cryptographic protocols can be facilitated by separating the protocol-dependent part from the protocol-independent part. Our Secrecy theorem encapsulates the use of induction so that the discharge of protocol-specific proof obligations is reduced to first-order reasoning. Secrecy proofs for Otway-Rees and the corrected Needham-Schroeder protocol are given.

gzipped postscript or postscript

BibTeX Entry

@InProceedings{MillenRuess:Oakland2000,
  author =       {Jon Millen and Harald Rue{\ss}},
  title =        {Protocol-independent secrecy},
  booktitle =    {2000 IEEE Symposium on Security and Privacy},
  month = {May},
  year =         2000,
  organization = {IEEE Computer Society}
}

---

Harald Ruess: ruess@csl.sri.com