Campus Event Calendar
Event Entry
What and Who
Automated Detection of Protocol Insecurity
Michael Rusinowitch
LORIA Nancy
Talk
AG 1, AG 2, AG 3, AG 4
Expert Audience
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 21 July 2003
15:30
60 Minutes
46.1 - MPII
024
Saarbrücken
Abstract
We present the CASRUL tool for analyzing cryptographic protocols
specifications in a model where the intruder has complete control of
the communications network. CASRUL verifies the executability of
protocols and compile them into transition rules that can be processed
by several back-ends such as model-checkers or theorem-provers. In
our model the existence of an attack can be encoded as a constraint
solving problem for an intruder. We discuss some decidability and
complexity issues concerning the protocol insecurity problem. In
particular the problem is NP-complete for a finite number of sessions
with composed encryption keys and for several extensions of Dolev-Yao
intruder.
specifications in a model where the intruder has complete control of
the communications network. CASRUL verifies the executability of
protocols and compile them into transition rules that can be processed
by several back-ends such as model-checkers or theorem-provers. In
our model the existence of an attack can be encoded as a constraint
solving problem for an intruder. We discuss some decidability and
complexity issues concerning the protocol insecurity problem. In
particular the problem is NP-complete for a finite number of sessions
with composed encryption keys and for several extensions of Dolev-Yao
intruder.
Contact
Ellen Fries
9325-502
--email hidden
passcode not visible
logged in users only