Goals related to verification and assessment

Our first goal is to provide rigorous definitions of the basic concepts developed by MAFTIA. The concise but informal models of intrusion tolerance that will be developed elsewhere in the project will be sufficient for most purposes, but a formal assessment requires a more precise understanding of the concepts.

The second goal is to validate results of the work on dependable middleware using a formal specification language and automatic verification tools (primarily model-checking). Protocols that use cryptographic primitives (in particular for dependable trusted third parties) will also be verified manually as part of their design, using standard cryptographic techniques.

The third specific assessment goal is to connect the fully formal techniques, which greatly idealise cryptographic primitives, with the more realistic complexity-theoretic cryptographic models which are so far not accessible to automatic checking of proofs.