Abstraction and refinement in protocol derivation

Protocols may be derived from initial components by composition, refinement, and transformation. Adding function variables to a previous protocol logic, we develop an abstraction-instantiation method for reasoning about a class of protocol refinements. The main idea is to view changes in a protocol as a combination of finding a meaningful "protocol template" that contains function variables in messages, and producing the refined protocol as an instance of the template. Using higher-order protocol logic, we can develop a single proof for all instances of a template. A template can also be instantiated to another template, or a single protocol may be an instance of more than one template, allowing separate protocol properties to be proved modularly. These methods are illustrated using some challenge-response and key exchange protocol templates and an exploration of the design space surrounding JFK (just fast keying) and related protocols from the IKE (Internet key exchange) family, which produces some interesting protocols not previously studied in the open literature.