Cyber security and privacy are issues that concern everyone living in this technologically dependent world. The work within our Security and Privacy Research Group is underpinned by considering critical issues for industry, government and society. For a list of academic papers by researcher or research area, see publications.
Cryptography is the study of mathematical techniques that secure and protect information in a digital format. It is used in securely sending and receiving messages. The security aspects include confidentiality, integrity, authentication and nonrepudiation. The protocols that apply cryptographic methods are called cryptographic or security protocols. Applications of cryptography include electronic voting, e-passports and RFIDs etc.
Security protocols are notoriously difficult to design and extremely error-prone. Therefore, formal verification is crucial to assess their security. This involves analysing systems with respect to a formal specification using mathematics. This helps to identify flaws within electronic systems and develop solutions for those problems.
Technologies today are increasingly operating wirelessly, enabling communication to occur further, faster and more flexibly. Our research covers a broad range of wireless devices, protocols and systems, from mobile phone networks to embedded devices communicating with one another or even vast systems of clouds, servers, products and users. With applications in conjunction with our other areas of expertise, this research topic focuses on ensuring wireless communication can occur securely while maintaining the functionality necessary for individuals and organisations to operate effectively.
From immobilisers and key fobs to sat-nav and self-driving cars, automotive vehicles are becoming increasingly wireless. This trend, that is only increasing in pace and extent, brings ubiquitous computing to our roads. To ensure security, privacy and safety, our researchers are testing the digital systems embedded in modern cars, in order to identify weaknesses and suggest solutions for manufacturers and users.
Electronic voting has boomed in the past decade, and more than a dozen countries have already used it for political binding elections, including Switzerland, Estonia, USA and Australia. Electronic voting has also become a choice more and more usual for elections in professional colleges or boards. The potential benefits of its use are the ease of voting for citizens living abroad, shortening the duration of the counting procedure, providing a more exact count of the votes or decreasing the number errors with respect to paper voting. The disadvantages are also important, including the risks of computer attacks, the possibility of coercion related to the fact that the act of voting will not be conducted in a public place, or the lack of voters' confidence in the system because of its complexity. Usually it is distinguished between remote voting, meaning that the voting device can potentially be any smart device with an Internet connection; and polling-site voting, meaning that the voters are authenticated in a polling station, but they use an electronic voting machine to cast their votes.
Cloud computing means entrusting data to information systems that are managed by external parties on remote servers, collectively known as the cloud. Cloud security raises privacy and confidentiality concerns, because the service provider has access to all the data and could accidentally or deliberately disclose it.
All aspects of our research are underpinned by a commitment to tackling challenging issues that are important to society. Amidst our theoretical and technical outputs with impact across a range of sectors in industry and governments we maintain an awareness of the variety of stakeholders and perspectives concerning social issues the consequences of which we cannot yet fully predict. Working between the need for security and individuals' right to privacy, our research consistently displays a sensitivity to its social impact, particularly when dealing with the often controversial issues in cyber security for current and future society.
The Security and Privacy group maintains a firm commitment to high quality research and education in cyber security. This includes not only pursuing each strand of intellectual endeavour separately, but ensuring that teaching is informed by up-to-date research and that research responds to the needs to raise the profile of security issues in computer science education. To achieve this, our researchers undertake work investigating the direct application of cyber security and privacy issues in teaching environments. For more information about our range of specific programmes, see education.
Electronic voting protocols should achieve two antagonistic security goals: privacy and veri ability. Additionally, they must be practical, from a usability, operational, and effciency point of view. Privacy can be expressed via several, increasingly demanding security properties:
Building on the Helios scheme, and its variant Belenios, we propose a new voting scheme, BeleniosRF, that offers both receipt-freeness and end-to-end veri ability. It is receipt-free in a strong sense, meaning that even dishonest voters cannot prove how they voted. We provide a game-based deffnition of receipt-freeness for voting protocols with non-interactive ballot casting, which we name strong receipt-freeness (sRF). To our knowledge, sRF is the first game-based definition of receipt-freeness in the literature, and it has the merit of being particularly concise and simple. Built upon the Helios protocol, BeleniosRF inherits its simplicity and does not require any anti-coercion strategy from the voters. We implement BeleniosRF and show its feasibility on a number of platforms, including desktop computers and smartphones.
This research was presented at ACM CCS 2016.
Generally speaking, a cryptographic protocol is an algorithmic procedure that enables to perform a certain task under certain requirements, while assuring that malicious attempts to abuse the performance of this task are unsuccessful. For instance, an encryption scheme allows two parties to communicate over a public channel while attaining privacy; a digital signature scheme provides authenticity, integrity and non-repudiation for digital documents.
To devise a way to prove formally that a given cryptographic protocol is secure has required (and it is still requiring) a lot of effort from researchers. A fundamental set of techniques developed to solve this question have led to the so-called provable security or reductionistic security paradigm. This paradigm can be explained as follows: take some cryptographic goal, like achieving privacy via encryption. The first step is to make a formal adversarial model and define what it means for a scheme to be secure, i.e. which are the functionalities that the scheme should provide when it is fairly used, and on the other hand, which are the functionalities that illegitimate users should not be able to perform. Then, a particular scheme, is shown to be sound via a reduction. Such a reduction implies that the only way to defeat the protocol in that model is to break an underlying atomic and more simple primitive. The latter problem should be known or be generally regarded as infeasible to break.
Modern automotive vehicles have several wireless interfaces, and are interconnected with various devices and with the internet. This connectivity adds great functionality but it also introduces a number of security and privacy threats. This project focuses on improving the security of the next generation electronic vehicles. Working in conjunction with Jaguar Land Rover, the research is developing optimized implementations of cryptographic primitives and protocols for time critical automotive applications.
From the point of view of computer security, there are several criteria that any electronic voting protocol should ideally meet. With regards to the integrity of the ballot casting process, we have individual verifiability, which allows voters to check whether his vote has been cast as intended and contributes to the announced results; and universal verifiability, which ensures that the outcome of the election was correctly calculated from the individual votes, and that this is verifiable by any observer.
Another desirable property is that of vote confidentiality, i.e. that it should be impossible in practice to learn how a particular voter voted, unless this is revealed by the result (e.g. if the vote is unanimous).
An advanced anonymity property is called receipt-freeness, and guarantees that a voter cannot prove how she voted even if she reveals her secret materials to an adversary, including randomness and credentials. These properties shall help achieving the goal of coercion-resistance, whereby powerful attackers are prevented from controlling and deciding how voters under coercion vote.
Electronic voting - especially remote voting over the internet - is very challenging to secure. Yet there is a growing call for internet voting to enable and encourage broader participation. However, such systems must ensure both privacy and verifiability to ensure that elections are legitimate and protected from corruption.
Du-Vote is a step towards tackling the problem of internet voting on user machines that are likely to have malware. Du-Vote is a new remote electronic voting protocol that eliminates the often-required assumption that voters trust general-purpose computers. This will enable secure internet voting on untrusted or even compromised hardware.
PRINCESS is part of a DARPA funded project, working in conjunction with the US R&D company Charles River Analytics. The research is developing techniques for adaptive software operating in uncertain environments, such as UUV control software. With the complex and constantly evolving technical ecosystems of contemporary software, adaptations need to verifiably correct in the context of repairing security, logical and performance-related vulnerabilities. These methods involve inferring the impact of evolution on application behaviour and performance, automatically triggering transformations that beneficially exploit these changes, and validating such transformations. The project aims to realise foundational advances in the design and implementation of complex software systems with increased robustness, agility and longevity.
Confidentiality from the Cloud Provider is an ongoing research project aimed at developing ways in which SME cloud service users can obtain the benefits of cloud computing without having to divulge their data to the cloud provider. So far the project has produced two systems:
ProVerif is a tool for automatically verifying cryptographic protocols to prove secrecy, authentication and equivalences. However, ProVerif over-approximates the adversary's power to enable verification of processes under replication. Unfortunately, this results in ProVerif reporting false attacks. This problem is particularly common in protocols whereby a participant commits to a particular value and later reveals their value. By using a compiler that inserts phase statements into a process, researchers in the Security and Privacy group introduced a method to avoid false attacks when analysing secrecy.
The paper and examples can be found here.
The monitoring of peer to peer file sharing: This work was the first to analyse the direct monitoring of illegal file sharing. Our findings include:
The full report, which includes an ethical consideration of the research, can be found here.
Since 1999, the University of Birmingham has been leading the development of the PRISM probabilisitic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilisitic behaviour. This tool can be used to analyse security protocols, as well as communication/multimedia protocols, randomised distributed algorithms, biological systems and others.
This collection of projects explores the Security and Privacy group's interest in how mutual infomration can be estimated and how information leakage can be measured in real systems. This includes:
Tools and software to support these projects can be found here.
We are surrounded by computerised systems, upon whose secure and reliable operation we are increasingly dependent. Yet flaws in these systems are common, from power plants to travel cards, and these come at high costs for individuals, companies and governments alike. So, rigorous, mathematically-sound techniques to check the security of computerised systems are essential. Security, though, is not absolute: we may only be able to guarantee that an attack on a system is possible with low probability, rather than impossible. Furthermore, system designs often need to trade off the degree of security or privacy offered against other practical concerns such as response time or power consumption. So, effective methods for the analysis of security also need to take these quantitative aspects into account.
This project developed fully-automated techniques to formally verify the correctness of security systems, to identify flaws in their operation, and to fix or optimise aspects of their design. This was achieved by bringing together techniques from several different areas:
Building upon recent advances in these fields, and upon existing efforts to create efficient and scalable verification methods, this project developed novel techniques to verify security systems, implement them in freely-available software tools and apply them to a variety of security applications, from electronic voting schemes to anonymous communication networks.
By learning about penetrating security systems, students can gain a practical knowledge of how they work as well as insights into attacks from an attacker's perspective. Our researchers have developed a virtual machine (VM) framework for cyber security education, which is used for courses offered at the University of Birmingham. This VM includes several capture the flag (CTF) style exercises that students can complete to support their learning:
More information - including the virtual machine, exercises and documentation - can be found here.