QinetiQ

QinetiQ comprises the greater part of DERA, the British Government's "Defence Evaluation and Research Agency". Until July 2001, DERA was an agency of the UK Ministry of Defence, incorporating the bulk of the MoD's non-nuclear research, technology and test and evaluation establishments. It then split into two organisations, DSTL and QinetiQ Group plc. DSTL remains part of the MOD and continues to handle the most sensitive areas of research.

The QinetiQ team contributed to work on the formal - i.e. automated - verification and assessment of selected MAFTIA protocols and services, and the formalization of selected MAFTIA fault-tolerant concepts.

The team developed a framework for systematically verifying MAFTIA protocols using the CSP algebra and FDR model checker. The framework provided conventions and original methods for modelling and verifying the diverse MAFTIA protocols. It was applied to a number of protocols including asynchronous and synchronous contract-signing protocols, two TTCB partially synchronous protocols, and Byzantine agreement and broadcast protocols.

The team also looked to bridge the gap between automated verification and formal cryptographic proof, this by attempting to model a formal group key agreement specification in CSP. In all of this work, the QinetiQ team collaborated closely with Saarland University, and with the designers of the protocols including IBM Zurich and Lisbon.

People at QinetiQ

These people worked on MAFTIA. Names in bold are Executive Board members, others are Research Associates.

Sadie Creese
Richard Harrison
Colin O'Halloran
William Simmonds