Publication
On the Automated Correction of Security Protocols Susceptible to a Replay Attack
Juan Lopez-Pimentel; Raul Monroy; Dieter Hutter
In: J. Biskup (Hrsg.). Proceedings of the 12th European Symposium On Research In Computer Security. European Symposium on Computer Security (ESORICS-07), September 24 - August 26, Dresden, Germany, Lectures Notes in Computer Science (LNCS), Springer-Verlag, 2007.
Abstract
Although there exist informal design guidelines and formal
specification/verification support, security protocol development is
time-consuming because protocol design is error-prone. In this
paper, we introduce \shrimp, a mechanism that aims to speed up the
development cycle by adding automated aid for protocol diagnosis and
repair. shrimp relies on existing verification tools to validate
an intermediate protocol and to compute attacks if the protocol is
flawed. Then it analyses such attacks to pinpoint the source of the
failure and synthesises appropriate patches, using Abadi and
Needham's principles for protocol design. We have translated some of
these principles into formal requirements on (sets of) protocol
steps. For each requirement, there is a collection of rules that
transform a set of protocol steps violating the requirement into a
set conforming it. We have successfully tested our mechanism on 36
faulty protocols, getting a repair rate of 90%.