Proving safety of authentication protocols: a minimal approach

摘要

Most work on proving or model checking the safety of authentication protocols is based on trace histories. We suggest that a simpler approach based on sets of messages sent is adequate and prove the correctness of the Needham-Schroeder and Secure Socket Layer protocols as examples. A simpler approach reduces the problem of making hidden or unwarranted assumptions as well as simplifying the proofs.