A Formal Analysis For Capturing Replay Attacks In Cryptographic Protocols

We present a reduction semantics for the LYSA calculus extended with session information, for modelling cryptographic protocols, and a static analysis for it. If a protocol passes the analysis then it is free of replay attacks and thus preserves freshness. The analysis has been implemented and applied to a number of protocols, including both original and corrected version of Needham-Schroeder protocol. The experiment results show that the analysis is able to capture potential replay attacks.