Network on Formal Methods and Cryptography: CryptoForma 2.
Lead Research Organisation:
University of Kent
Department Name: Sch of Computing
Abstract
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.
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.
Planned Impact
Formal security analysis of cryptographic protocols provides increased security of, and confidence in many important applications where currently public confidence is low, such as electronic voting and e-commerce.
Security protocols studied by network members include SSL (the standard method for secure connection to web services, probably used by literally billions of people), and protocols for secure cloud computing.
This benefits both providers of these and future applications (i.e., governments, businesses) and their users (i.e., society as a whole).
Security protocols studied by network members include SSL (the standard method for secure connection to web services, probably used by literally billions of people), and protocols for secure cloud computing.
This benefits both providers of these and future applications (i.e., governments, businesses) and their users (i.e., society as a whole).
People |
ORCID iD |
| Eerke Boiten (Principal Investigator) |
Publications
Boiten E
(2014)
Abstract State Machines, Alloy, B, TLA, VDM, and Z
Boiten E
(2014)
Editorial
in Formal Aspects of Computing
| Description | - Economic impact. The network aimed to develop techniques to improve confidence in cryptographic and security protocols. These protocols, and the cryptographic primitives they are based on, are used to establish information security in specific security-sensitive applications such as electronic commerce, but also all internet-based business communications and information storage. In particular, researchers in the network (Paterson et al at RHUL, Fournet's group at Microsoft Research) have found security problems in the SSL protocol, which is part of the standard method for secure encrypted communication with web services, probably used by literally billions of people. Several groups in the network (Ryan et al at Birmingham; Chadwick et al at Kent) work on secure protocols for cloud computing, which has become a standard model for commercial data storage for small and medium sized businesses; full homomorphic encryption as being developed e.g. by Smart et al at Bristol (now in a startup Dyadic) is considered to be a crucial candidate component for ensuring confidentiality of data in the cloud, even against the cloud provider. This kind of impact is achieved in a number of indirect ways. Security errors in established software are reported as a matter of routine to the writers and distributors of such software, as well as on internet forums where the practical security community collects reports of known bugs and vulnerabilities. Tools developed for finding security errors tend to be made publicly available through open source projects, or through spin-off companies. The more general techniques underlying such tools are published academically, in textbooks, and included in postgraduate and undergraduate university courses. Design principles which avoid particular types of security problems are shared in similar ways. Also, several network members are in industrial research laboratories (HP, Microsoft), have started spin off companies (Smart in Dyadic) or have close collaborations with industrial partners outside this network which allow the exploitation of novel security protocols, for example in the mobile phone industry. - Societal impact The protocols considered in the network include protocols for secure communication with web services (as described above), which have great societal value as well as economic value. Protocols for data integrity and to support confidentiality or even availability of networked resources are a crucial component of cyber security. A particular topic of interest in the network is electronic voting (groups at Surrey and Birmingham) which is of a potentially large value for governments anywhere. Several experiments in this area have been cut short due to a lack of confidence in the schemes used to establish security properties in this; this research network is aimed at increasing such confidence through mathematics and logic based methods. Again this kind of impact is achieved in indirect ways. Project partners are involved in multidisciplinary collaborations to study and introduce electronic voting. Other methods for achieving impact are as above for economic impact. Network partners have also been vocal in public debate on encryption and security backdoors, starting from an open letter to GCHQ after the Snowden revelations and including contributions in the press and parliamentary evidence by Ryan concerning "bulk equipment interference" in the Investigatory Powers Bill in 2015. |
| First Year Of Impact | 2012 |
| Sector | Digital/Communication/Information Technologies (including Software) |
| Impact Types | Societal,Economic,Policy & public services |
| Description | Engagement with the press on public interest aspects of security, cryptography, and privacy |
| Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Media (as a channel to the public) |
| Results and Impact | Quotes in international, national (Guardian, Independent,...), and online press (Wired, TheRegister, ...) Media comment pieces, e.g. many in The Conversation LinkedIn columns Twitter engagement and online blogs Regional and national radio TV |
| Year(s) Of Engagement Activity | 2013,2014,2015,2016,2017,2018 |
| Description | FOSAD summer schools |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | CryptoForma became a partner in the international FOSAD summer school. Selection of speakers, sponsoring of speakers, and sponsoring of UK attendants. |
| Year(s) Of Engagement Activity | 2012,2013,2014,2015,2016 |
| Description | Open Letter to GCHQ regarding cryptographic backdoors |
| Form Of Engagement Activity | A press release, press conference or response to a media enquiry/interview |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Media (as a channel to the public) |
| Results and Impact | Members of the CryptoForma network drew up an open letter to GCHQ regarding the insecurity of cryptographic backdoors. This was reported on in The Guardian. |
| Year(s) Of Engagement Activity | 2013 |
| URL | http://www.theguardian.com/technology/2013/sep/16/nsa-gchq-undermine-internet-security |