Formal Methods and Cryptography: The Next Generation of Abstractions (CryptoForma)

The purpose of CryptoForma is to build an expanding network in computer science and mathematics to support the development of formal notations, methods and techniques for modelling and analysing modern cryptographic protocols. This work increases security and confidence in such protocols and their applications (e.g. in e-commerce and voting), to the benefit of protocol designers, businesses, governments, and application users.The United Kingdom has traditionally been a world leader in research into, and applications of, formal methods. Work in the UK on the foundations of languages and notations such as CSP, pi-calculus, and Z have led to their widespread use in critical systems development in industry.The UK is also well known to contain leading experts in cryptography. In the last two decades we have done important work in stream cipher design, symmetric ciphers (differential and algebraic cryptanalysis), elliptic curve cryptography, identity based cryptography and in protocols (e.g. in the mobile phone industry).In the 1990s in the UK, formal methods were successfully applied to the modelling and verification of security protocols at a high level of abstraction. However, modern cryptographic protocols contain probabilistic and complexity theoretic aspects which require a different set of abstractions. Several approaches for dealing with this have appeared since, including: automated proof-checking; compositional techniques; higher level proof structures; abstractions of computational models; and specialised logics.The network aims to bring together research groups working in the UK in these areas, starting with 7 sites and expanding rapidly from that.It will allow a systematic and effective cross-fertilisation between the differing strands of work. The consortium contains mathematicians and computer scientists, experts on cryptography, on formal methods, and on their interconnection, and developers of practical cryptographic protocols both from academia and from industry. A group with such a very broad spectrum of expertise will enable both(a) informing/strengthening practical developments by solid mathematical analysis, and (b) motivating foundational analysis by practice-based needs and requirements.To do so the network will organise meetings around both fundamental and more directly applicable issues, such as:- adequate abstractions of cryptographic primitives;- specialised specification notations with notions of probability, timing, and complexity;- abstract concepts and logics that allow the expression of security properties and reasoning about them;- practical protocols, e.g. e-voting, trust management, and those involving zero-knowledge proofs and commitments which formal methods cannot currently deal with.With these interests and questions in mind, the overall aims of CryptoForma are to:- bring together academics and industrialists interested in the application of formal methods to the specification, development and verification of cryptographic protocols;- stimulate collaboration between individuals and groups in order to tackle the questions highlighted above;- disseminate problems and results to researchers and practitioners in the field and to the wider communities in cryptography and formal methods.To achieve this research meetings and workshops are planned which will foster collaboration and disseminate key results.This proposal is timely and important because- society has recently experienced a reduced confidence in protection of electronic data, and in applications such ase-commerce and e-voting;- a critical mass of researchers in this area exists in the UK but this is not being exploited;- the subject is high on the agenda of research institutions, industries and academics world-wide. This is evidenced by the letters of support and the enthusiasm for the preliminary meeting of the network in January 2009 where all partners and 10 others will meet.