A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols

14 years 5 months ago

Download www.di.unipi.it

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.

Han Gao, Chiara Bodei, Pierpaolo Degano, Hanne Rii

Real-time Traffic

Algorithms | Analysis | ASIAN 2007 | Potential Replay Attacks | Replay Attacks |

claim paper

» Cryptographic Protocol Analysis of ANON

» Formal Analysis of TimeDependent Cryptographic Protocols in RealTime Maude

» Using Admissible Interference to Detect Denial of Service Vulnerabilities

» Security Analysis of VoiceoverIP Protocols

» Trusted Multiplexing of Cryptographic Protocols

» A Formal Analysis of Complex Type Flaw Attacks on Security Protocols

» What is the best way to prove a cryptographic protocol correct

» A rewritingbased inference system for the NRL protocol analyzer grammar generation

Post Info
More Details (n/a)

Added	07 Jun 2010
Updated	07 Jun 2010
Type	Conference
Year	2007
Where	ASIAN
Authors	Han Gao, Chiara Bodei, Pierpaolo Degano, Hanne Riis Nielson

Comments (0)

Sciweavers

A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols

Algorithms | Analysis | ASIAN 2007 | Potential Replay Attacks | Replay Attacks |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers