The Pda Protocol Derivation Language
In this section, we will define the language of protocol derivations used in the Pda tool. The general idea of the derivational approach is that derivations of protocols go hand in hand with that of proofs of security properties of the protocols. The benefit of this approach is that complex protocols can be derived incrementally from much simpler ones. At the same time the security property proofs are also incrementally developed, so that already proven properties of abstract protocols can be used as theorems in more specific ones. This gives the derivational approach a huge gain compared to other approaches, which try to prove security properties on the final protocols. Because in the latter case the protocol is treated as a monolithic piece of code and/or spec, the complexity of security property proofs can become huge so that it can become infeasible to try proving them with state-of-the-art proving techniques.
Technically, Pda separates the language of protocol derivations from the language to express security properties and proofs. While the latter one is exchangable in the tool, the language of protocol derivations is pre-defined in order to provide a general framework to define protocols and derivations. In its distributed version, Pda comes with a module for expressing specs and proofs in Specware, Kestrel’s state-of-the-art specification language. (Specware itself is not included in the release, but is the framework to communicate to a Specware server process running in the background.) In the following, we will present the Pda protocol derivation language in detail.