Verification and Assessment

There were three main objectives to the work on verification and assessment within MAFTIA: formalisation of basic concepts, specification and verification of security properties using CSP, and combining cryptographic and formal analysis techniques.

Formalisation of Basic Concepts

WP1 produced concise but informal models of intrusion tolerance that are sufficient for most purposes. But a formal assessment requires a more precise understanding of the concepts. Therefore we selected the most important concepts and described them within a rigorous model. Here, rigorous is meant in the mathematical sense: the model was precise, allowing proofs of statements as usual when making proofs by hand. But it was not based on a formal language and so was not necessarily amenable to automatic verification.

Specification and verification with CSP

We used the well-known and in this context highly effective CSP/model-checking approach to the analysis of security protocols. In essence the idea is to create a CSP specification of the security properties of interest and a model of the protocol agents along with the hostile agent(s). A model-checker then performs a refinement check of the model against the specification by running through all essentially distinct behaviours. If a behaviour is found that violates the specification this is reported by the tool and represents an attack. The technique is thus highly automated and efficient and is now widely regarded as being at the forefront of the field.

The mechanisms envisaged by MAFTIA depend heavily on various protocols for which this approach is already highly developed. However, the protocols developed by MAFTIA are of a rather different flavour from those more typical in, say, key exchange: they involve more complex cryptographic primitives (such as threshold cryptography) and involve larger numbers of participants in a given run. Thus the existing tools and techniques needed to be enhanced to cater for these considerations.

Combining cryptographic and formal analysis techniques

The first step towards combining cryptographic and formal analysis techniques is to define what it means for a cryptographic protocol to fulfil an arbitrary specification expressed in a formal language like CSP "in the cryptographic sense." The optimum result would be to prove (by hand) once and for all that protocols that were formally verified using the simplified model of cryptographic primitives are also provably secure in the cryptographic sense, when instantiated with real primitives that are provably secure in the cryptographic sense.

Unfortunately, we expect this optimum result to be false, as we already aware of some intuitive counter examples. Nevertheless, we believe in the importance of combining formal methods and real cryptographic meaning because simple specifications and tool support are essential to avoid specification errors, and security should obviously hold for the real system and not only an abstracted one. We therefore attempted to characterise useful conditions under which the abstraction from cryptographic primitives used in a formal methods analysis are faithful.