Maliciousand AccidentalFault Tolerance for Internet Applications IST Research Project IST199911583 1 January 2000  28 February 2003 


Conceptual Model and Architecture WP1 concentrated on the Conceptual Model and Architecture of attack tolerance. Deliverables... Dependable Middleware WP2 developed a modular and scalable cryptographic grouporiented middleware suite Deliverables... 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 intrusiontolerant Deliverables... Trusted Third Parties WP4 designed a generic architecture for dependable Trusted Third Party (TTP) services based on results from WP2. Deliverables... Distributed Authorisation In WP5, we defined a framework for access control and authorisation Deliverables... Verification and Assessment WP6 worked towards formalisation of the MAFTIA conceptual model Deliverables... 

Verification and AssessmentThere 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.
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.
We used the wellknown and in this context highly effective CSP/modelchecking 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 modelchecker 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.
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. 

