Introduction

The Protocol derivation assistant (Pda) is a tool to support the incremental derivation of security protocols, together with proofs of their security properties. Just as proof derivations start from definitions and axioms and apply logical transformations, Pda’s derivations start from basic protocol components, and then support refinements and transformations to reach the desired protocol. The guiding idea of Pda is to utilize incremental methods of protocol design found in practice, and to support these methods in an open, evolving framework. This idea stands in contrast to attempts to reduce security to a predetermined set of formal rules.

Our goal for the Pda environment is an IDE for production of assured protocols, their derivations, and their security properties, with accompanying proofs. We will over time populate the IDE with a library of protocol components, generic refinements and transformations, and a proof lineage. Of note and importance to some is the fact that the IDE could also be used to identify and prove protocol vulnerabilities and derive witnesses of (attacks on) those vulnerabilities.

---