  In this paper, we introduce a mechanism that aims to speed up the development
cycle of security protocols, by adding automated aid for diagnosis and repair.
Our mechanism relies on existing verification tools analyzing intermediate
protocols and synthesizing potential attacks if the protocol is flawed. The
analysis of these attacks (including type flaw attacks) pinpoints the source of
the failure and controls the synthesis of appropriate patches to the protocol.
Using strand spaces, we have developed general guidelines for protocol repair,
and captured them 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
implemented our mechanism into a tool, called SHRIMP. We have successfully
tested SHRIMP on numerous faulty protocols, all of which were successfully
repaired, fully automatically.
