Analysing Security and Privacy Properties
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
Security systems break because design practices focus too much on mechanisms, at the expense of clearly-defined properties. The vision of this research is to bring about a shift of emphasis to highlight the properties that security systems are expected to provide. This will be done by developing methods for verification of security systems. I will focus on a selection of interconnected real-world problems that are of great importance to society, but that are currently in need of greater industry/academe cooperation. The combination of fundamental research with close collaboration with industry, government and users is expected to achieve significant results and impact. I will develop and apply new methods and techniques to create and analyse solutions in three areas:* Trusted computing is an industry-led technology that aims to root security in hardware. Since its launch, academics including me have discovered significant issues that threaten to undermine its potential at providing a range of security benefits. This has arisen because industry does not have the expertise to analyse the protocols.* Electronic voting is an application currently attracting significant interest from government and industry, but numerous security issues have resulted in failure of confidence among politicians, commentators and public alike.* Privacy for citizens using electronic services is hotly debated by journalists and user groups and politicians, but has been substantially eroded by new technologies and policies.In these three areas, there is currently the risk of significant waste of resources on inappropriate or unaccepted technologies, resulting in user disempowerment and exclusion. The outcomes of this fellowship are intended to address that risk.A distinguishing feature of the proposal is the substantial engagement with industry and user groups that are active in these three areas. As a result of discussions with them, several organisations have committed significant resources, including cash contribution, manager and developer time, and access to users and experts.
Organisations
- University of Birmingham (Lead Research Organisation)
- Microsoft Research (Collaboration)
- L3 TRL Technology (Collaboration)
- Open Rights Group (Collaboration, Project Partner)
- Google (Collaboration)
- Microsoft Corporation (Collaboration)
- Hewlett Packard Ltd (Collaboration)
- Forensic Pathways Ltd (Project Partner)
- 3Form (Project Partner)
- Royal Holloway University of London (Project Partner)
- Hewlett-Packard (United Kingdom) (Project Partner)
- OPT2Vote Ltd (Project Partner)
- Electoral Reform Services (Project Partner)
- Ministry of Justice (Project Partner)
- Google (United Kingdom) (Project Partner)
- Microsoft (United States) (Project Partner)
People |
ORCID iD |
| Mark Ryan (Principal Investigator) |
Publications
Yu J
(2017)
Authenticating Compromisable Storage Systems
Yu J
(2016)
DTKI: A New Formalized PKI with Verifiable Trusted Parties
in The Computer Journal
Yu J
(2014)
An Efficient Generic Framework for Three-Factor Authentication With Provably Secure Instantiation
in IEEE Transactions on Information Forensics and Security
Yu J
(2018)
DECIM: Detecting Endpoint Compromise In Messaging
in IEEE Transactions on Information Forensics and Security
Yu J
(2015)
Security Protocols XXIII
Stalla-Bourdillon Sophie
(2014)
Privacy vs. Security
Smyth B
(2015)
Formal analysis of privacy in Direct Anonymous Attestation schemes
in Science of Computer Programming
Ryan M
(2013)
Cloud computing security: The scientific challenge, and a survey of solutions
in Journal of Systems and Software
Ryan M
(2017)
Security Protocols XXV
Ryan M
(2011)
Cloud computing privacy concerns on our doorstep
in Communications of the ACM
Preneel B
(2015)
Privacy and Security in an Age of Surveillance (Dagstuhl Perspectives Workshop 14401)
in Dagstuhl Manifestos 5(1)
Pike A
(2012)
Digital exclusion or learning exclusion? An ethnographic study of adult male distance learners in English prisons
in Research in Learning Technology
Oxford, M.
(2020)
Quantitative Verification of Certificate Transparency Gossip Protocols
Mark D Ryan
(2012)
Automatic Analysis of Security Properties
in INTRUST
Mark D Ryan
(2014)
FMS @ Petri Nets
in Du-Vote: Remote Electronic Voting with Unstructured Computers
Grewal G
(2015)
Du-Vote: Remote Electronic Voting with Untrusted Computers
Denzel M
(2018)
Malware Tolerant (Mesh-)Networks.
Delaune S
(2010)
Symbolic bisimulation for the applied pi calculus*
in Journal of Computer Security
Delaune S
(2011)
Formal Analysis of Protocols Based on TPM State Registers
| Title | Inaugural lecture |
| Description | Mark Ryan's inaugural lecture. |
| Type Of Art | Film/Video/Animation |
| Year Produced | 2011 |
| Impact | Enquiries from PhD students. |
| URL | http://vimeo.com/25449665 |
| Title | Online voting video |
| Description | Video about online internet voting. |
| Type Of Art | Film/Video/Animation |
| Year Produced | 2013 |
| Impact | None yet. |
| URL | http://www.youtube.com/watch?v=dI7IHtHpwf4 |
| Description | Further development and prototype implementation of StatVerif, a technique and tool for analysing protocols with persistent state. Formal analysis of authorisation protocols of the TPM. Formal analysis of state-based (PCR) protocols of the TPM. Proposal of digital envelope using protocols of the TPM. Formal analysis of direct anonymous attestation protocol. Exposition of applied pi calculus. Use of formal analysis to discover vulnerabilities in mobile phone protocols, and fixes. Development of applied pi calculus with state, and soundness and completeness proofs. Formal analysis of confidentiality-preserving cloud computing architecture. Analysis of trade-off between privacy and security properties. StatVerif verifier tool made publicly available online. |
| Exploitation Route | StatVerif will be used by academics and industry interested in performing automatic analysis of protocols involving persistent state. Research can be used by designers of the TPM to improve their specifications. StatVerif will be used by academics and industry interested in performing automatic analysis of protocols involving persistent state. Research can be used by designers of the TPM to improve their specifications. |
| Sectors | Creative Economy,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Government, Democracy and Justice,Security and Diplomacy,Other |
| URL | http://sec.cs.bham.ac.uk/research/StatVerif/ |
| Description | One of the project's core findings is the way in which security properties and privacy properties are often pulling in opposite directions. We see this in the debate around WhatsApp encryption: it increases a user's privacy, of course, but it can weaken societal security by making serious crimes harder to detect and prosecute. A core idea explored by the project is how to develop technical measures which maximise the security properties (crime detectablility) while simultaneously avoiding negative privacy impact. A mechanism we developed to achieve that is called called "accountable decryption" (documented in some of the academic paper outputs). It has had visible impact on society and industry in the following ways: Ryan has been invited to give several talks about the technology, to various organisations including Privacy International and Open Rights Group. Ryan has consulted with a company that is implementing the methods in several products under the branding of "Privacy-preserving accountable decryption" (PPAD - https://pad.tech). The company has build a product called PAD Places which allows nominated parties to access the location of a user, in such a way that no other party can access it and the user is necessarily notified of accesses that are made. Another impact of the project has been its influence on the ProVerif verification tool, which is focussed on analysing security protocols and has a significant user base in industry. The mechanism of accountable decryption uses a public ledger (or blockchain), and in a collaboration between our group and the ProVerif developers, ProVerif has been extended to handle this kind of protocol. |
| First Year Of Impact | 2021 |
| Sector | Digital/Communication/Information Technologies (including Software),Government, Democracy and Justice,Security and Diplomacy,Other |
| Impact Types | Societal,Economic |
| Description | Advisory council member for WebRoots The Institute for Digital Democracy |
| Geographic Reach | National |
| Policy Influence Type | Participation in a guidance/advisory committee |
| URL | https://webrootsdemocracy.org/advisory-council/ |
| Description | (FutureTPM) - Future Proofing the Connected World: A Quantum-Resistant Trusted Platform Module |
| Amount | € 4,868,890 (EUR) |
| Funding ID | 779391 |
| Organisation | European Commission |
| Sector | Public |
| Country | European Union (EU) |
| Start | 01/2018 |
| End | 12/2020 |
| Description | Microsoft gift |
| Amount | $45,000 (USD) |
| Organisation | Microsoft Corporation |
| Sector | Public |
| Country | United States |
| Start | 04/2010 |
| Description | Research Chair in Cyber Security |
| Amount | £400,000 (GBP) |
| Organisation | Hewlett Packard Ltd |
| Department | Hewlett Packard Laboratories, Bristol |
| Sector | Private |
| Country | United Kingdom |
| Start | 09/2016 |
| End | 08/2021 |
| Description | User-controlled hardware security anchors: evaluation and designs |
| Amount | £486,082 (GBP) |
| Funding ID | EP/R012598/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 02/2018 |
| End | 01/2023 |
| Title | StatVerif |
| Description | A software tool to verify the security properties of protocols. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2014 |
| Provided To Others? | Yes |
| Impact | Take up by other researchers |
| URL | https://sec.cs.bham.ac.uk/research/StatVerif/ |
| Description | |
| Organisation | |
| Country | United States |
| Sector | Private |
| PI Contribution | Collaboration of certificate management |
| Collaborator Contribution | Collaboration of certificate management |
| Impact | Discussion and meetings |
| Start Year | 2010 |
| Description | Google Asylo |
| Organisation | |
| Department | Research at Google |
| Country | United States |
| Sector | Private |
| PI Contribution | Disclosed vulnerabilities. Found instances of the problematic [user_check] attribute that lacked proper pointer validation, leaving critical vulnerabilities in the compiled enclave |
| Collaborator Contribution | - |
| Impact | Improved security of products. |
| Start Year | 2019 |
| Description | Hewlett Packard |
| Organisation | Hewlett Packard Ltd |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Collaboration on TPM specification |
| Collaborator Contribution | Collaboration on TPM specification |
| Impact | Contribution to TPM 2.0 specification and multiple research papers |
| Start Year | 2006 |
| Description | L-3 TRL |
| Organisation | L3 TRL Technology |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Collaboration on Secure Cloud-based Collaboration Platform |
| Collaborator Contribution | Collaboration on Secure Cloud-based Collaboration Platform |
| Impact | Discussion and meetings Ongoing research partnership Solutions for key management and data processing in the cloud |
| Start Year | 2014 |
| Description | Microsoft |
| Organisation | Microsoft Corporation |
| Country | United States |
| Sector | Public |
| PI Contribution | Collaboration on TPM specification and access conrol |
| Collaborator Contribution | Collaboration on TPM specification and access conrol |
| Impact | PhD secondment and planned future collaborations |
| Start Year | 2008 |
| Description | Microsoft Open Enclave |
| Organisation | Microsoft Research |
| Department | Microsoft Research Cambridge |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Disclosed Vulnerabilities. CVE-2019-0876, CVE-2019-1369,and CVE-2019-1370. |
| Collaborator Contribution | - |
| Impact | Improved security of products. |
| Start Year | 2019 |
| Description | Open Rights Group |
| Organisation | Open Rights Group |
| Country | United Kingdom |
| Sector | Charity/Non Profit |
| PI Contribution | Collaboration on privacy |
| Collaborator Contribution | Collaboration on privacy |
| Impact | Contribution to Royal Society Meeting on 9 June 2014 |
| Start Year | 2014 |
| Title | ConfiChair |
| Description | ConfiChair is a cloud-based collaboration tool that guarantees confidentiality from the cloud provider. See confiChair.org |
| Type Of Technology | Webtool/Application |
| Year Produced | 2011 |
| Impact | Follow-up funding |
| URL | https://www.confichair.org/ |
| Title | StatVerif |
| Description | StatVerif is a software tool for analysing the security protocols of stateful protocols. It builds upon another well known tool called ProVerif |
| Type Of Technology | Software |
| Year Produced | 2011 |
| Impact | Papers in journals and conferences |
| Company Name | CloudTomo |
| Description | The company aims to commercialise some security research. |
| Year Established | 2011 |
| Impact | Has won two funding awards: Scottish Enterprise award (60K) and TSB award (80K, not taken up). |
| Description | British Science Festival panel |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | Yes |
| Geographic Reach | National |
| Primary Audience | Public/other audiences |
| Results and Impact | Discussion. Awareness raising. |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://www.britishscienceassociation.org/british-science-festival/privacy-and-security-age-surveilla... |
| Description | Dagstuhl perspectives workshop |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | Yes |
| Geographic Reach | International |
| Primary Audience | Other academic audiences (collaborators, peers etc.) |
| Results and Impact | Wide-ranging presentations. Manifesto document. |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://www.dagstuhl.de/en/programm/kalender/semhp/?semnr=14401 |
| Description | Delivered a Talk at HP Labs |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | Co-I Ryan delivered a tutorial talk at HP Labs 22 October 2020, "Intro to Keystone (an enclave system for RISC-V)" |
| Year(s) Of Engagement Activity | 2020 |
| Description | Delivered a Talk at Huawei Security Advisory Board |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Co-I Ryan delivered a Talk at Huawei Security Advisory Board 27 November 2020, "An overview of hardware security anchors for IoT and embedded applications" |
| Year(s) Of Engagement Activity | 2020 |
| Description | Google visit |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Much discussion. Interaction. |
| Year(s) Of Engagement Activity | 2012 |
| Description | Pint of Science Festival |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Regional |
| Primary Audience | Public/other audiences |
| Results and Impact | Mark Ryan, along with colleagues Tom Chothia and Flavio Garcia, gave talks as part of the Pint of Science Festival. This international series of events offers the general public to engage with experts in scientific fields by attending talks, asking questions and entering discussion, within the informal setting of a bar or pub. The academics presented the findings of research with real-world impact to individual privacy that increased awareness and interest in the subject area. |
| Year(s) Of Engagement Activity | 2015 |
| URL | http://www.birmingham.ac.uk/university/colleges/eps/news/college/2015/04/Pint-of-Science-Festival-20... |
| Description | Royal Society meeting |
| Form Of Engagement Activity | A formal working group, expert panel or dialogue |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Policymakers/politicians |
| Results and Impact | It was a high-profile meeting at the Royal Society entitled Security and Privacy in Society. The event hosts a unique combination of people from both the surveillance community and the privacy community. I am very pleased to have a stellar list of invitees, including Sir David Omand and Sir Francis Richards, both former directors of GCHQ, Rt. Hon. James Arbuthnot MP (Chairman of the Defence Select Committee), Julian Huppert MP, and Helen Goodman MP, and the privacy proponents Caspar Bowden, Charles Raab, and Bart Preneel. Yet others include Jean Jaques Quisquater, the journalists Ewen MacAskill (Guardian) and Gordon Corera (BBC). There will also be some senior current people from GCHQ. Support for further funding applications. |
| Year(s) Of Engagement Activity | 2014 |
| URL | http://www.cs.bham.ac.uk/research/groupings/security_and_privacy/royalsoc2014/ |
| Description | invited talk at the Shonan seminar |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Professional Practitioners |
| Results and Impact | Ryan gave an invited talk called "Hardware technologies for making privacy violations transparent and accountable" at the Shonan seminar (Japan) on the theme of "Biggest failures in privacy" on 28 Sept. |
| Year(s) Of Engagement Activity | 2021 |