Proving Secrecy is Easy Enough

---

Authors

Veronique Cortier and Jon Millen and Harald Rueß

Abstract

We develop a systematic proof procedure for establishing secrecy results for cryptographic protocols. Part of the procedure is to reduce messages to simplified constituents, and its core is a search procedure for establishing secrecy results. This procedure is sound but incomplete in that it may fail to establish secrecy for some secure protocols. However, it is amenable to mechanization, and it also has a convenient visual representation. We demonstrate the utility of our procedure with secrecy proofs for standard benchmarks such as the Yahalom protocol.

gzipped postscript or postscript

BibTeX Entry

@unpublished{CMR:CSFW2001,
	TITLE = {Proving Secrecy is Easy Enough},
	AUTHOR = {V{\'e}ronique Cortier and Jon Millen and Harald Rue{\ss}},
	YEAR = 2001,
	NOTE = {To be presented at CSFW'2001}
}

---

Harald Ruess: ruess@csl.sri.com