From 14th IEEE Computer Security Foundations Workshop.
IEEE Computer Society.
2001.

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.

@inproceedings{CMR01,
    AUTHOR = {V\'{e}ronique Cortier and Jonathan Millen and Harald Rue\ss},
    TITLE = {Proving secrecy is easy enough},
    BOOKTITLE = {14th {IEEE} Computer Security Foundations Workshop},
    YEAR = {2001},
    PUBLISHER = {{IEEE} Computer Society},
    URL = {http://www.csl.sri.com/papers/cmr01/}
}

• recipe.ps.gz