Proving Secrecy is Easy Enough
V. Cortier, J. Millen, H. Ruess
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.