The UK funding agency EPSRC has recently announced a new Network called CryptoForma, which aims to bridge the divide between two different schools of analysing cryptographic protocols. Based at the University of Kent, the Bristol Cryptography Research Group will form a partner in this network along with a number of other leading players, including the Universities of Birmingham, Royal Holloway and Surrey, as well as Microsoft Research and Hewlett-Packard Laboratories.
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.
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.