Malicious-and Accidental-Fault Tolerance for Internet Applications
IST Research Project IST-
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 ] [ Architecture ] [ Mechanisms and Protocols ] [ Verification and Assessment ]

Verification and Assessment

The verification and assessment work within MAFTIA was largely performed by Saarland and QinetiQ, but involved close collaboration with other partners whose protocols and mechanisms were being verified, notably IBM and Lisbon. The goals of the verification and assessment work were three-fold:

  • to develop a rigorous model of selected malicious- and accidental-fault tolerance concepts
  • to formalize some properties and protocols in the language CSP and verify them with a model checker
  • to investigate how cryptography can be integrated into such formalizations in a faithful way
This work involved bringing together techniques from both the cryptographic community and the formal methods community. Traditional approaches to cryptographic verification rely on precise definitions and proofs - the work is complex, detailed, and error-prone, and there is no tool support. In contrast, the formal methods community uses well-defined protocol languages such as CSP with automated tool support such as model checkers, but there is a need to make simplifying assumptions and abstract away from the underlying cryptographic details, such as error probabilities and partial information leakage. An important step towards bridging the gap between these two models was the development of a system model, the so called "secure reactive system model", which can be used to rigorously specify security requirements, define systems and prove that a system fulfils its requirements. A further important and distinguishing feature of the secure reactive system model is the existence of a composition theorem, which allows for modular design and modular security proofs even of complex systems. The basic approach is illustrated below in Figure 5, which shows how the theorem would be used to verify the security of a certified mail service built on top of a library of cryptographic primitives:

Figure 5 : An application of the composition theorem

The system has been split into two layers. The lower layer is a cryptographic system whose security can be rigorously proven using standard cryptographic arguments. To the upper layer it provides an abstract (and typically deterministic) service that hides all cryptographic details. Relative to this abstract service one can verify the upper layer using existing formal methods. Since the models allow secure composition, one can conclude that the overall system is secure if the formally verified upper layer is put on top of a cryptographically verified lower layer.

In addition to exploring the relationship between the two different approaches to verification and assessment of secure systems, both cryptographic and process algebraic techniques were used to formalise and verify selected components of the MAFTIA middleware. The modelling of the TTCB services provided a good case study for how to model services running over hybrid networks. During the verification of these TTCB protocols, a productive dialogue ensued between the protocol author and verifier to resolve ambiguities, and the verifier was able to suggest minor amendments to one of the services provided by the TTCB that would result in a more fault tolerant service.

[ Conceptual Model ] [ Architecture ] [ Mechanisms and Protocols ] [ Verification and Assessment ]