A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols

Abstract. 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.

• Type: Conference
• Year: 2007
• Where: ASIAN
• Authors: Han Gao, Chiara Bodei, Pierpaolo Degano, Hanne Riis Nielson
• Keywords: Algorithms, Analysis, ASIAN 2007, Potential Replay Attacks, Replay Attacks