Information Society Technologies (IST) Programme, FET Open Assessment Project: IST-2000-26410
Operative commencement date of contract: May 1st, 2001.
This 1 year assessment project aims at laying the foundations of a new generation of verification tools for automatic error detection for e-commerce and related security protocols. To assess the potential of this technology, we will develop a prototype verification tool incorporating inference engines based on three promising automated deduction techniques: on-the-fly model-checking based on lazy data-types, theorem-proving with constraints, and model-checking based on propositional satisfiability checking. The assessment consists of two phases: a development phase aimed at the design and implementation of a prototype verification tool, and an analysis phase, in which the tool (and the techniques) will be tested and evaluated against a corpus of 50 security protocol verification problems. This will pave the way to turning the prototype into a mature technology, whose application in the industrial setting will be ascertained in a follow-up, full RTD project with industry involvement.