Malicious-and Accidental-Fault Tolerance for Internet Applications
IST Research Project IST-1999-11583
1 January 2000 - 28 February 2003

Check out a summary of the project, or browse through the original project proposal.

MAFTIA involved experts from 5 countries and 6 organisations. The Industrial Advisory Board provided valuable feedback on the work of the project.

Research was organised into six workpackages.

Find out more about the key scientific results and achievements, and the benefits of this research collaboration.

Conceptual Model and Architecture
WP1 concentrated on the Conceptual Model and Architecture of attack tolerance.

Dependable Middleware
WP2 developed a modular and scalable cryptographic group-oriented middleware suite

Intrusion Detection
WP3 investigated ways of reducing the high rate of false positives and false negatives for existing Intrusion Detection Systems (IDSs), whilst making the IDS itself intrusion-tolerant

Trusted Third Parties
WP4 designed a generic architecture for dependable Trusted Third Party (TTP) services based on results from WP2.

Distributed Authorisation
In WP5, we defined a framework for access control and authorisation

Verification and Assessment
worked towards formalisation of the MAFTIA conceptual model

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.