Dr Constantin Catalin Dragan


Lecturer in Secure Systems
PhD
+441483683469

About

Areas of specialism

applied cryptography; provable security; electronic voting; formal verification

University roles and responsibilities

  • MSc Senior Personal Tutor (2023 - Current)
  • Personal Tutor (2020 - Current)

    Supervision

    Postgraduate research supervision

    Teaching

    Publications

    Sergiu Bursuc, Constantin-Catalin Dragan, Steve Kremer (2019)Private votes on untrusted platforms: models, attacks and provable scheme, In: 2019 4TH IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY (EUROS&P)8806713pp. 606-620 IEEE

    Modern e-voting systems deploy cryptographic protocols on a complex infrastructure involving different computing platforms and agents. It is crucial to have appropriate specification and evaluation methods to perform rigorous analysis of such systems, taking into account the corruption and computational capabilities of a potential attacker. In particular, the platform used for voting may be corrupted, e.g. infected by malware, and we need to ensure privacy and integrity of votes even in that case. We propose a new definition of vote privacy, formalized as a computational indistinguishability game, that allows to take into account such refined attacker models; we show that the definition captures both known and novel attacks against several voting schemes; and we propose a scheme that is provably secure in this setting. We moreover formalize and machine-check the proof in the EasyCrypt theorem prover.

    Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjosteen, Thomas HAines, Peter Y. A. Ryan, Peter B. Ronne, Morten Rotvold Solberg (2023)Machine-checked proofs of privacy against malicious boards for Selene Co, In: Journal of computer security31(5)pp. 469-499 Ios Press

    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 (2014)A necessary and sufficient condition for the asymptotic idealness of the GRS threshold secret sharing scheme, In: Information processing letters114(6)299pp. 299-303 Elsevier

    The study of the asymptotic idealness of the Goldreich-Ron-Sudan (GRS, for short) threshold secret sharing scheme was the subject of several research papers, where sufficient conditions were provided. In this paper a necessary and sufficient condition is established; namely, it is shown that the GRS threshold secret sharing scheme is asymptotically ideal under the uniform distribution on the secret space if and only if it is based on 1-compact sequences of co-primes. (c) 2014 Elsevier B.V. All rights reserved.

    Ferucio Laurentiu Tiplea, Constantin Catalin Dragan, Anca-Maria Nica (2017)Key-Policy Attribute-Based Encryption from Bilinear Maps, In: P Farshim, E Simion (eds.), INNOVATIVE SECURITY SOLUTIONS FOR INFORMATION TECHNOLOGY AND COMMUNICATION: 10TH INTERNATIONAL CONFERENCE, SECITC 201710543pp. 28-42 Springer Nature

    The aim of this paper is to provide an overview on the newest results regarding the design of key-policy attribute-based encryption (KP-ABE) schemes from secret sharing and bilinear maps.

    Mihai Barzu, Ferucio Laurenţiu Ţiplea, Constantin Cătălin Drăgan (2013)Compact sequences of co-primes and their applications to the security of CRT-based threshold schemes, In: Information sciences240161pp. 161-172 Elsevier Inc

    CRT-based threshold secret sharing schemes use sequences of pairwise co-prime positive integers in their construction. If these sequences are not “compact”, then the CRT-based threshold secret sharing schemes may have a weak security in the sense of a massive loss of entropy or an arbitrarily large information rate. In this paper, compact sequences of co-primes are introduced, and their applications to the security of CRT-based threshold secret sharing schemes is throughout investigated. It is shown that all the results regarding the security of CRT-based threshold secret sharing schemes that use sequences of consecutive primes also hold for threshold secret sharing schemes that use compact sequences of co-primes. Moreover, compact sequences of co-primes may be significantly denser than sequences of consecutive primes of the same length, and their use in the construction of CRT-based threshold secret sharing schemes may lead to better security properties.

    Constantin Catalin Dragan, Ferucio Laurentiu Tiplea (2018)On the asymptotic idealness of the Asmuth-Bloom threshold secret sharing scheme, In: Information sciences463pp. 75-85 Elsevier

    The Chinese remainder theorem (CRT) is a fundamental theorem in number theory, widely used in cryptography to design secret sharing schemes. The CRT-based secret sharing schemes proposed so far make use of sequences of pairwise co-prime integers with special properties. The way these sequences are chosen plays a crucial role in the security achieved by the schemes that rely on them. Moreover, the CRT-based secret sharing schemes could achieve at most asymptotic idealness. In this paper we prove that the Asmuth-Bloom threshold secret sharing scheme is asymptotic ideal if and only if it is based on 1-compact sequences of co-primes. Apart from this, a comprehensive analysis of the known variants of the Asmuth-Bloom threshold secret sharing scheme is provided, clarifying the security properties achieved by each of them. (C) 2018 Elsevier Inc. All rights reserved.

    Ioana Boureanu, Constantin Cătălin Drăgan, Mark Manulis, Thanassis Giannetsos, Christoforos Dadoyan, Panagiotis Gouvas, Roger A Hallman, Shujun Li, Victor Chang, Frank Pallas, Jörg Pohle, Angela Sasse (2020)Computer Security Springer International Publishing

    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.

    Ferucio Laurentiu Tiplea, Constantin Catalin Dragan (2015)Key-Policy Attribute-Based Encryption for Boolean Circuits from Bilinear Maps, In: B Ors, B Preneel (eds.), CRYPTOGRAPHY AND INFORMATION SECURITY IN THE BALKANS9024pp. 175-193 Springer Nature

    We propose a Key-policy Attribute-based Encryption (KPABE) scheme for (monotone) Boolean circuits based on bilinear maps. The construction is based on secret sharing and just one bilinear map, and it is a proper extension of the KP-ABE scheme in [7] in the sense that it is practically efficient for a class of Boolean circuits which strictly includes all Boolean formulas. Selective security of the proposed scheme in the standard model is proved, and comparisons with the scheme in [5] based on leveled multilinear maps, are provided. Thus, for Boolean circuits representing multilevel access structures, our KP-ABE scheme is more efficient than the one in [5].

    Constantin Catalin Dragan, Ferucio Laurentiu Tiplea (2016)Distributive weighted threshold secret sharing schemes, In: Information sciences339pp. 85-97 Elsevier

    The concept of distributive weighted threshold access structure is introduced, which is an weighted threshold access structure where the participants are distributed on levels, the participants on the same level are assigned the same weight, and the threshold of the access structure is 1. The weight of the participants on the ith level is of the form 1/k(i) and, therefore, the ith level induces a standard threshold access structure with threshold k(i). We propose a CRT-based realization of distributive weighted threshold access structures, which is asymptotically perfect and perfect zero-knowledge. We also show that distributive weighted threshold access structures do not generally have ideal realizations. In case of just one level, our scheme can be viewed as an asymptotically perfect and perfect zero-knowledge variation of the Asmuth-Bloom secret sharing scheme. (C) 2016 Elsevier Inc. All rights reserved.

    Constantin Cătălin Drăgan, Ferucio Laurenţiu Ţiplea (2016)Key-Policy Attribute-Based Encryption for General Boolean Circuits from Secret Sharing and Multi-linear Maps, In: Enes Pasalic, Lars R. Knudsen (eds.), Cryptography and Information Security in the Balkanspp. 112-133 Springer International Publishing

    We propose a Key-policy Attribute-based Encryption (KP-ABE) scheme for general Boolean circuits, based on secret sharing and on a very particular and simple form of leveled multi-linear maps, called chained multi-linear maps. The number of decryption key components is substantially reduced in comparison with the scheme in [7], and the size of the multi-linear map (in terms of bilinear map components) is less than the Boolean circuit depth, while it is quadratic in the Boolean circuit depth for the scheme in [7]. Moreover, the multiplication depth of the chained multi-linear map in our scheme can be significantly less than the multiplication depth of the leveled multi-linear map in the scheme in [7]. Selective security of the proposed scheme in the standard model is proved, under the decisional multi-linear Diffie-Hellman assumption.

    Veronique Cortier, Constantin Catalin Dragan, Francois Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi (2017)Machine-Checked Proofs of Privacy for Electronic Voting Protocols, In: 2017 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP)7958621pp. 993-1008 IEEE

    We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.

    Constantin Catalin Dragan, Mark Manulis (2020)KYChain: User-Controlled KYC Data Sharing and Certification, In: PROCEEDINGS OF THE 35TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING (SAC'20)pp. 301-307 Assoc Computing Machinery

    Under Know Your Customer (KYC) regulations, financial institutions are required to verify the identity and assess the trustworthiness of any new client during on-boarding, and maintain up-to-date records for risk management. These processes are time consuming, expensive, typically have sub-par record-keeping steps, and disadvantage clients with nomad lifestyle. In this paper, we introduce KYChain as a privacy-preserving certification mechanism that allows users to share (certified) up-to-date KYC data across multiple financial institutions. We base KYChain on immutable ledgers and show that it offers confidentiality and certification compliance of KYC data.

    Muntadher Sallal, Steve Schneider, Matthew Casey, Francois Dupressoir, Helen Treharne, Catalin Dragan, Luke Riley, Phil Wright (2020)Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger, In: 2020 IEEE 40th International Conference on Distributed Computing Systems (ICDCS)2020-pp. 1167-1168 IEEE

    This paper discusses an approach for incremental change to an online voting system, introducing a verifiability layer based on the Selene protocol to a trusted-third-party-based system, resulting in a fully verifiable and transparent e-voting system. The paper also describes how to use Distributed Ledger Technology as a component of the implementation of Selene to manage the verifiability data in a distributed way for resilience and trust.

    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.

    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.

    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.

    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.

    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.

    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.

    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.

    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.

    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.

    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.