In the academic area there are numerous approaches to the formal analysis of security protocols. Computer-supported approaches are all based on the Dolev-Yao (DY) model, which assumes a perfect cryptography. On the other side protocol proofs using models that allow for weaker and complexity-theoretic assumptions are available up to now (only) as paper and pencil proofs. One objective of ProtoTo is the formalization of such a model within the VSE tool and the embedding of DY based analysis. Due to the integrated verification technique the gap between the complementary analysis methods gets closed.
At the implementation level new attacks could possibly arise through the refinement of the abstract protocol model. Besides the adequate realization of the cryptographic primitives, these attacks must be considered in addition to the classical (functional) correctness in the implementation of the protocol rules. Thus, another objective of ProtoTo is the development of a refinement concept that deals with the mentioned aspects and that in particular applies established techniques of code verification.
In order to support the application of ProtoTo's verification techniques by trained but not necessarily scientific users, appropriate guidance instructions shall be made available. These will be defined within an integrated procedural method for the development of security protocols that is structured according to the assurance levels of the Common Criteria (CC). The process model contains also guidelines to CC documents and their evaluation. It shall be demonstrated and evaluated using two case studies taken from the areas of trusted computing applications and secure software updates.
Partners
Kobil Systems GmbH, Sirrix AG, Technische Universität Darmstadt
