Runtime verification of cryptographic protocols

There has been a significant amount of work devoted to the static verification of security protocol designs. Virtually all of these results, when applied to an actual implementation of a security protocol, rely on certain implicit assumptions on the implementation (for example, that the cryptographic checks that according to the design have to be performed by the protocol participants are carried out correctly). So far there seems to be no approach that would enforce these implicit assumptions for a given implementation of a security protocol (in particular regarding legacy implementations which have not been developed with formal verification in mind). In this paper, we use a code assurance technique called "runtime verification" to solve this open problem. Runtime verification determines whether or not the behaviour observed during the execution of a system matches a given formal specification of a "reference behaviour". By applying runtime verification to an implementation of any of the participants of a security protocol, we can make sure during the execution of that implementation that the implicit assumptions that had to be made to ensure the security of the overall protocol will be fulfilled. The overall assurance process then proceeds in two steps: First, a design model of the security protocol in UML is verified against security properties such as secrecy of data. Second, the implicit assumptions on the protocol participants are derived from the design model, formalised in linear-time temporal logic, and the validity of these formulae at runtime is monitored using runtime verification. The aim is to increase one's confidence that statically verified properties are satisfied not only by a model of the system, but also by the actual running system itself. We demonstrate the approach at the hand of the open source implementation Jessie of the de-facto Internet security protocol standard SSL. We also briefly explain how to transfer the results to the SSL-implementation within the Java Secure Sockets Extension (JSSE) recently made open source by Sun Microsystems