Skip to main content Skip to main navigation


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.


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