A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols