Strand-Based Approach to Patch Security Protocols

TL;DR

This paper presents SHRIMP, an automated tool that uses strand spaces and verification analysis to diagnose flaws in security protocols and automatically generate patches, significantly improving protocol repair efficiency.

Contribution

It introduces a novel, automated approach combining formal analysis and repair rules for security protocols, implemented in the SHRIMP tool.

Findings

Successfully repaired numerous faulty protocols automatically

Automated diagnosis and patch generation improves development cycle

Formal guidelines ensure reliable protocol repair

Abstract

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.