On the automated correction of security protocols susceptible to a replay attack

Abstract

Although there exist informal design guidelines and formal development support, security protocol development is time-consuming because 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 both to analyse 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%. © Springer-Verlag Berlin Heidelberg 2007.