The purpose of CryptoForma 2 is to sustain and expand a network of excellence for supporting the development of formal notations, methods and techniques for modelling and analysing modern cryptographic protocols, and to increase its national and international profile.
The network brings together cryptographers, developers of security protocols, and the formal methods community which looks to formalise, analyse, and verify such protocols. This work increases security and confidence in such protocols and their applications, to the benefit of protocol designers, businesses, governments, and application users. The network will thus contribute to the wider research agenda of RCUK Global Uncertainties and in particular Cyber Security, by stimulating research that increases security of information as it is transmitted through networks, and stored in appliances and servers.
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 has 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 important work was done in the UK in stream cipher design, symmetric ciphers (differential and algebraic cryptanalysis), elliptic curve cryptography, identity based cryptography, full homomorphic encryption, and in protocols.
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 different abstractions. Many approaches for dealing with this have appeared since, including: automated proof-checking; compositional techniques; proof structuring; abstractions of computational models; and specialised logics.
The CryptoForma network brought together research groups in the UK from the 6 founding sites, with meetings attended from 8 other UK sites and elsewhere in Europe. This new proposal aims to continue to bring together research groups in the UK, aiming at further growth from its (now) 12 sites, and strong profiling and connections internationally. It will continue 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 broad spectrum of expertise enables both
(a) informing/ strengthening practical developments by 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:
cryptographic primitives, e.g. full homomorphic encryption;
specialised specification notations;
abstract concepts and logics that allow the expression of security properties and reasoning about them;
practical protocols, e.g. for e-voting, cloud security, and access control.
With these issues in mind, the overall aims of CryptoForma 2 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, and with the international research community, in order to tackle both practical and foundational research questions;
- disseminate problems and results to researchers and practitioners in the field and to the wider communities in cryptography and formal methods.
To achieve this a variety of research meetings and workshops are planned which
will foster collaboration and dissemination.
|