Variations on the themes of message freshness and replay-or the difficulty in devising formal methods to analyze cryptographic protocols

摘要

A survey is given of the variations on the choice and the usage of freshness identifiers, and the various forms of replay attack. Besides helping to clarify the important concepts of freshness and replay, this exercise demonstrates the potential complexity in devising formal methods to analyze cryptographic protocols.