About

Areas of specialism

applied cryptography; provable security; formal verification; electronic voting

Publications

Panagiotis Gouvas, Roger A Hallman, Shujun Li, Christoforos Dadoyan, Ioana Boureanu, Victor Chang, Angela Sasse, Frank Pallas, Thanassis Giannetsos, Constantin Catalin Dragan, Mark Manulis, Jorg Pohle (2020)Computer Security Security and Cryptology: ESORICS 2020 International Workshops, DETIPS, DeSECSys, MPS, and SPOSE, Guildford, UK, September 17-18, 2020, Revised Selected Papers Springer

This book constitutes the refereed post-conference proceedings of the Interdisciplinary Workshop on Trust, Identity, Privacy, and Security in the Digital Economy, DETIPS 2020; the First International Workshop on Dependability and Safety of Emerging Cloud and Fog Systems, DeSECSys 2020; Third International Workshop on Multimedia Privacy and Security, MPS 2020; and the Second Workshop on Security, Privacy, Organizations, and Systems Engineering, SPOSE 2020; held in Guildford, UK, in September 2020, in conjunction with the 25th European Symposium on Research in Computer Security, ESORICS 2020.A total of 42 papers was submitted. For the DETIPS Workshop 8 regular papers were selected for presentation. Topics of interest address various aspect of the core areas in relation to digital economy.For the DeSECSys Workshop 4 regular papers are included. The workshop had the objective of fostering collaboration and discussion among cyber-security researchers and practitioners to discuss the various facets and trade-o s of cyber security. In particular, applications, opportunities and possible shortcomings of novel security technologies and their integration in emerging application domains.For the MPS Workshop 4 regular papers are presented which cover topics related to the security and privacy of multimedia systems of Internet-based video conferencing systems (e.g., Zoom, Microsoft Teams, Google Meet), online chatrooms (e.g., Slack), as well as other services to support telework capabilities.For the SPOSE Workshop 3 full papers were accepted for publication. They reflect the discussion, exchange, and development of ideas and questions regarding the design and engineering of technical security and privacy mechanisms with particular reference to organizational contexts.

MOHAMMED ALSADI, Matthew Casey, Constantin-Catalin Dragan, François Dupressoir, Luke Riley, Muntadher Sallal, Steven Alfred Schneider, Helen Treharne, Joe Wadsworth, Philip Wright (2023)Towards End-to-End Verifiable Online Voting: Adding Verifiability to Established Voting Systems, In: IEEE transactions on dependable and secure computing IEEE

Online voting for independent elections is generally supported by trusted election providers. Typically these providers do not offer any way in which a voter can verify their vote, and hence the providers are trusted with ballot privacy and in ensuring correctness. Despite the desire to offer online voting for political elections, this lack of transparency and verifiability is often seen as a significant barrier to the large-scale adoption of online elections. Adding verifiability to an online election increases transparency and integrity, as well as allowing voters to verify that the vote they cast has been recorded correctly and included in the tally. However, replacing existing online systems with those that provide verifiable voting requires new algorithms and code to be deployed, and this presents a significant business risk to commercial election providers, as well as the societal risk for official elections selecting for public office. In this paper we present the first step in an incremental approach which minimises the business risk but demonstrates the advantages of verifiability, by developing an implementation of key elements of a Selene-based verifiability layer and adding it to an operational online voting system. Selene is a verifiable voting protocol that publishes votes in plaintext alongside a voter's tracker. These trackers enable voters to confirm that their votes have been captured correctly by the system, such that the election provider does not know which tracker has been allocated to which voter. This results in a system where even a " dishonest but cautious " election authority running the system cannot be sure of changing the result in an undetectable way, and hence gives stronger guarantees on the integrity of the election than were previously present. We explore the challenges presented by adding a verifiability layer to an operational system. The system was used in two initial trials conducted within real contested elections. We conclude by outlining the further steps in the road-map towards the deployment of a fully trustworthy online voting system.

Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y.A. Ryan, Peter Rønne, Morten Rotvold Solberg (2022)Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co, In: The Institute of Electrical and Electronics Engineers, Inc. (IEEE) Conference Proceedings IEEE

Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the state of the art by taking into account that verification in many schemes will happen or must happen after the tally has been published, not before as in previous definitions. As a case study we give a machine-checked proof of privacy for Selene, which is a remote electronic voting scheme which offers an attractive mix of security properties and usability. Prior to our work, the computational privacy of Selene has never been formally verified. Finally, we also prove that MiniVoting and Belenios satisfies our definition.

Ferucio Laurentiu Tiplea, Constantin Catalin Dragan (2021)Asymptotically ideal Chinese remainder theorem -based secret sharing schemes for multilevel and compartmented access structures, In: IET information security15(4)pp. 282-296 Wiley

Multilevel and compartmented access structures are two important classes of access structures where participants are grouped into levels/compartments with different degrees of trust and privileges. The construction of secret sharing schemes for such access structures has been the attention of researchers for a long time. Two main approaches have been taken so far, one of them is based on polynomial interpolation and the other one is based on the Chinese Remainder Theorem (CRT). In this article the first asymptotically ideal CRT-based secret sharing schemes for (disjunctive, conjunctive) multilevel and compartmented access structures are proposed. Our approach is compositional and it is based on a variant of the Asmuth-Bloom secret sharing scheme where some participants may have public shares. Based on this, the proposed secret sharing schemes for multilevel and compartmented access structures are asymptotically ideal if and only if they are based on 1-compact sequences of co-primes. Possible applications for secret image and multi-secret sharing are pointed-out.

Ioana Boureanu, Constantin Catalin Dragan, Francois Dupressoir, David Gerault, Pascal Lafourcade (2021)Mechanised Models and Proofs for Distance-Bounding, In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF)2021-pp. 1-16 IEEE

In relay attacks, a man-in-the-middle adversary impersonates a legitimate party and makes it this party appear to be of an authenticator, when in fact they are not. In order to counteract relay attacks, distance-bounding protocols provide a means for a verifier (e.g., an payment terminal) to estimate his relative distance to a prover (e.g., a bankcard). We propose FlexiDB, a new cryptographic model for distance bounding, parameterised by different types of fine-grained corruptions. FlexiDB allows to consider classical cases but also new, generalised corruption settings. In these settings, we exhibit new attack strategies on existing protocols. Finally, we propose a proof-of-concept mechanisation of FlexiDB in the interactive cryptographic prover EasyCrypt. We use this to exhibit a flavour of man-in-the-middle security on a variant of MasterCard's contactless-payment protocol.

Constantin-Catalin Dragan, Daniel Gardham, Mark Manulis (2018)Hierarchical Attribute-based Signatures. 17th International Conference, CANS 2018, Naples, Italy, September 30 – October 3, 2018, In: J Camenisch, P Papadimitratos (eds.), Cryptology and Network Security. CANS 2018. Lecture Notes in Computer Science11124pp. 212-234 Springer Verlag

Attribute-based Signatures (ABS) are a powerful tool allowing users with attributes issued by authorities to sign messages while also proving that their attributes satisfy some policy. ABS schemes provide a exible and privacy-preserving approach to authentication since the signer's identity and attributes remain hidden within the anonymity set of users sharing policy-conform attributes. Current ABS schemes exhibit some limitations when it comes to the management and issue of attributes. In this paper we address the lack of support for hierarchical attribute management, a property that is prevalent in traditional PKIs where certification authorities are organised into hierarchies and signatures are verified along roots of trust. Hierarchical Attribute-based Signatures (HABS) introduced in this work support delegation of attributes along paths from the top-level authority down to the users while also ensuring that signatures produced by these users do not leak their delegation paths, thus extending the original privacy guarantees of ABS schemes. Our generic HABS construction also ensures unforgeability of signatures in the presence of collusion attacks and contains an extended traceability property allowing a dedicated tracing authority to identify the signer and reveal its attribute delegation paths. We include a public verification procedure for the accountability of the tracing authority. We anticipate that HABS will be useful for privacy-preserving authentication in applications requiring hierarchical delegation of attribute-issuing rights and where knowledge of delegation paths might leak information about signers and their attributes, e.g., in intelligent transport systems where vehicles may require certain attributes to authenticate themselves to the infrastructure but remain untrackable by the latter.

Yifan Yang, Daniel Cooper, John Collomosse, Catalin Dragan, Mark Manulis, Jo Briggs, Jamie Steane, Arthi Manohar, Wendy Moncur, Helen Jones (2020)TAPESTRY: A De-centralized Service for Trusted Interaction Online, In: IEEE Transactions on Services Computingpp. 1-1 Institute of Electrical and Electronics Engineers (IEEE)

We present a novel de-centralised service for proving the provenance of online digital identity, exposed as an assistive tool to help non-expert users make better decisions about whom to trust online. Our service harnesses the digital personhood (DP); the longitudinal and multi-modal signals created through users' lifelong digital interactions, as a basis for evidencing the provenance of identity. We describe how users may exchange trust evidence derived from their DP, in a granular and privacy-preserving manner, with other users in order to demonstrate coherence and longevity in their behaviour online. This is enabled through a novel secure infrastructure combining hybrid on- and off-chain storage combined with deep learning for DP analytics and visualization. We show how our tools enable users to make more effective decisions on whether to trust unknown third parties online, and also to spot behavioural deviations in their own social media footprints indicative of account hijacking.

Catalin Dragan, Mark Manulis (2020)Bootstrapping Online Trust: Timeline Activity Proofs, In: Data Privacy Management, Cryptocurrencies and Blockchain Technology SpringerLink

Establishing initial trust between a new user and an online service, is being generally facilitated by centralized social media platforms, i.e., Facebook, Google, by allowing users to use their social profiles to prove “trustworthiness” to a new service which has some verification policy with regard to the information that it retrieves from the profiles. Typically, only static information, e.g., name, age, contact details, number of friends, are being used to establish the initial trust. However, such information provides only weak trust guarantees, as (malicious) users can trivially create new profiles and populate them with static data fast to convince the new service. We argue that the way the profiles are used over (longer) periods of time should play a more prominent role in the initial trust establishment. Intuitively, verification policies, in addition to static data, could check whether profiles are being used on a regular basis and have a convincing footprint of activities over various periods of time to be perceived as more trustworthy. In this paper, we introduce Timeline Activity Proofs (TAP) as a new trust factor. TAP allows online users to manage their timeline activities in a privacy-preserving way and use them to bootstrap online trust, e.g., as part of registration to a new service. In our model we do not rely on any centralized social media platform. Instead, users are given full control over the activities that they wish to use as part of TAP proofs. A distributed public ledger is used to provide the crucial integrity guarantees, i.e., that activities cannot be tampered with retrospectively. Our TAP construction adopts standard cryptographic techniques to enable authorized access to encrypted activities of a user for the purpose of policy verification and is proven to provide data confidentiality protecting the privacy of user’s activities and authenticated policy compliance protecting verifiers from users who cannot show the required footprint of past activities.

Catalin Dragan, Daniel Gardham, Mark Manulis (2020)Hierarchical Attribute-based Signatures, In: International Conference on Cryptology and Network Security Springer Nature

Attribute-based Signatures (ABS) are a powerful tool allowing users with attributes issued by authorities to sign messages while also proving that their attributes satisfy some policy. ABS schemes provide a exible and privacy-preserving approach to authentication since the signer's identity and attributes remain hidden within the anonymity set of users sharing policy-conform attributes. Current ABS schemes exhibit some limitations when it comes to the management and issue of attributes. In this paper we address the lack of support for hierarchical attribute management, a property that is prevalent in traditional PKIs where certication authorities are organised into hierarchies and signatures are veried along roots of trust. Hierarchical Attribute-based Signatures (HABS) introduced in this work support delegation of attributes along paths from the top-level authority down to the users while also ensuring that signatures produced by these users do not leak their delegation paths, thus extending the original privacy guarantees of ABS schemes. Our generic HABS construction also ensures unforgeability of signatures in the presence of collusion attacks and contains an extended traceability property allowing a dedicated tracing authority to identify the signer and reveal its attribute delegation paths. We include a public verication procedure for the accountability of the tracing authority. We anticipate that HABS will be useful for privacy-preserving authentication in applications requiring hierarchical delegation of attribute-issuing rights and where knowledge of delegation paths might leak information about signers and their attributes, e.g., in intelligent transport systems where vehicles may require certain attributes to authenticate themselves to the infrastructure but remain untrackable by the latter.

Véronique Cortier, Constantin Cătălin Dragan, Francois Dupressoir, Bogdan Warinschi (2018)Machine-checked proofs for electronic voting: privacy and verifiability for Belenios, In: Proceedings of the 31st IEEE Computer Security Foundations Symposium Institute of Electrical and Electronics Engineers (IEEE)

We present a machine-checked security analysis of Belenios – a deployed voting protocol used already in more than 200 elections. Belenios extends Helios with an explicit registration authority to obtain eligibility guarantees. We offer two main results. First, we build upon a recent framework for proving ballot privacy in EasyCrypt. Inspired by our application to Belenios, we adapt and extend the privacy security notions to account for protocols that include a registration phase. Our analysis identifies a trust assumption which is missing in the existing (pen and paper) analysis of Belenios: ballot privacy does not hold if the registrar misbehaves, even if the role of the registrar is seemingly to provide eligibility guarantees. Second, we develop a novel framework for proving strong verifiability in EasyCrypt and apply it to Belenios. In the process, we clarify several aspects of the pen-and-paper proof, such as how to deal with revote policies. Together, our results yield the first machine-checked analysis of both ballot privacy and verifiability properties for a deployed electronic voting protocol. Perhaps more importantly, we identify several issues regarding the applicability of existing definitions of privacy and verifiability to systems other than Helios. While we show how to adapt the definitions to the particular case of Belenios, our findings indicate the need for more general security notions for electronic voting protocols with registration authorities.

MARK MANULIS, DANIEL LEWIS GARDHAM, CONSTANTIN-CATALIN DRAGAN (2020)Biometric-Authenticated Searchable Encryption

We introduce Biometric-Authenticated Keyword Search (BAKS), a novel searchable encryption scheme that relieves clients from managing cryptographic keys and relies purely on client's biometric data for authenticated outsourcing and retrieval of files indexed by encrypted keywords. BAKS utilises distributed trust across two servers and the liveness assumption which models physical presence of the client; in particular, BAKS security is guaranteed even if clients' biometric data, which often has low entropy, becomes public. We formalise two security properties, Authentication and Indistinguisha-bility against Chosen Keyword Attacks, which ensure that only a client with a biometric input sufficiently close to the registered template is considered legitimate and that neither of the two servers involved can learn any information about the encrypted keywords. Our BAKS construction further supports outsourcing and retrieval of files using multiple keywords and flexible search queries (e.g., conjunction, disjunction and subset-type queries). An additional update mechanism allows clients to replace their registered biometrics without requiring re-encryption of outsourced keywords , which enables smooth user migration across devices supporting different types of biometrics.