Steve Schneider

Craig Burton, Chris Culnane, Steve Schneider

The November 2014 Australian State of Victoria election was the first statutory political election worldwide at State level which deployed an end-to-end verifiable electronic voting system in polling places. This was the first time blind voters have been able to cast a fully secret ballot in a verifiable way, and the first time a verifiable voting system has been used to collect remote votes in a political election. The code is open source, and the output from the election is verifiable. The system took 1121 votes from these particular groups, an increase on 2010 and with fewer polling places.

Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen et al.

In today's world, critical infrastructure is often controlled by computing systems. This introduces new risks for cyber attacks, which can compromise the security and disrupt the functionality of these systems. It is therefore necessary to build such systems with strong guarantees of resiliency against cyber attacks. One way to achieve this level of assurance is using formal verification, which provides proofs of system compliance with desired cyber security properties. The use of Formal Methods (FM) in aspects of cyber security and safety-critical systems are reviewed in this article. We split FM into the three main classes: theorem proving, model checking and lightweight FM. To allow the different uses of FM to be compared, we define a common set of terms. We further develop categories based on the type of computing system FM are applied in. Solutions in each class and category are presented, discussed, compared and summarised. We describe historical highlights and developments and present a state-of-the-art review in the area of FM in cyber security. This review is presented from the point of view of FM practitioners and researchers, commenting on the trends in each of the classes and categories. This is achieved by considering all types of FM, several types of security and safety critical systems and by structuring the taxonomy accordingly. The article hence provides a comprehensive overview of FM and techniques available to system designers of security-critical systems, simplifying the process of choosing the right tool for the task. The article concludes by summarising the discussion of the review, focusing on best practices, challenges, general future trends and directions of research within this field.

Mohammed Alsadi, Matthew Casey, Constantin Catalin Dragan et al.

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, so the providers are trusted with ballot privacy and 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, allowing voters to verify that their vote 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. 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 uses trackers to enable voters to confirm that their votes have been captured correctly while protecting voter anonymity. This results in a system where even the election authority running the system cannot change the result in an undetectable way, and 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. We describe the results of two initial trials, which obtained that survey respondents found this form of verifiability easy to use and that they broadly appreciated it. We conclude by outlining the further steps in the road-map towards the deployment of a fully trustworthy online voting system.

Thomas Gittings, Steve Schneider, John Collomosse

We present a novel method for generating robust adversarial image examples building upon the recent `deep image prior' (DIP) that exploits convolutional network architectures to enforce plausible texture in image synthesis. Adversarial images are commonly generated by perturbing images to introduce high frequency noise that induces image misclassification, but that is fragile to subsequent digital manipulation of the image. We show that using DIP to reconstruct an image under adversarial constraint induces perturbations that are more robust to affine deformation, whilst remaining visually imperceptible. Furthermore we show that our DIP approach can also be adapted to produce local adversarial patches (`adversarial stickers'). We demonstrate robust adversarial examples over a broad gamut of images and object classes drawn from the ImageNet dataset.

Jinguang Han, Liqun Chen, Steve Schneider et al.

An anonymous Single Sign-On (ASSO) scheme allows users to access multiple services anonymously using one credential. We propose a new ASSO scheme, where users can access services anonymously through the use of anonymous credentials and unlinkably through the provision of designated verifiers. Notably, verifiers cannot link service requests of a user even if they collude. The novelty is that when a designated verifier is unavailable, a central authority can authorise new verifiers to authenticate the user on behalf of the original verifier. Furthermore, if required, a central verifier is authorised to deanonymise users and trace their service requests. We formalise the scheme along with a security proof and provide an empirical evaluation of its performance. This scheme can be applied to smart ticketing where minimising the collection of personal information of users is increasingly important to transport organisations due to privacy regulations such as General Data Protection Regulations (GDPR).

Jinguang Han, Liqun Chen, Steve Schneider et al.

Anonymous Single-Sign-On authentication schemes have been proposed to allow users to access a service protected by a verifier without revealing their identity which has become more important due to the introduction of strong privacy regulations. In this paper we describe a new approach whereby anonymous authentication to different verifiers is achieved via authorisation tags and pseudonyms. The particular innovation of our scheme is authentication can only occur between a user and its designated verifier for a service, and the verification cannot be performed by any other verifier. The benefit of this authentication approach is that it prevents information leakage of a user's service access information, even if the verifiers for these services collude which each other. Our scheme also supports a trusted third party who is authorised to de-anonymise the user and reveal her whole services access information if required. Furthermore, our scheme is lightweight because it does not rely on attribute or policy-based signature schemes to enable access to multiple services. The scheme's security model is given together with a security proof, an implementation and a performance evaluation.

Jinguang Han, Liqun Chen, Steve Schneider et al.

Electronic tickets (e-tickets) are electronic versions of paper tickets, which enable users to access intended services and improve services' efficiency. However, privacy may be a concern of e-ticket users. In this paper, a privacy-preserving electronic ticket scheme with attribute-based credentials is proposed to protect users' privacy and facilitate ticketing based on a user's attributes. Our proposed scheme makes the following contributions: (1) users can buy different tickets from ticket sellers without releasing their exact attributes; (2) two tickets of the same user cannot be linked; (3) a ticket cannot be transferred to another user; (4) a ticket cannot be double spent; (5) the security of the proposed scheme is formally proven and reduced to well known (q-strong Diffie-Hellman) complexity assumption; (6) the scheme has been implemented and its performance empirically evaluated. To the best of our knowledge, our privacy-preserving attribute-based e-ticket scheme is the first one providing these five features. Application areas of our scheme include event or transport tickets where users must convince ticket sellers that their attributes (e.g. age, profession, location) satisfy the ticket price policies to buy discounted tickets. More generally, our scheme can be used in any system where access to services is only dependent on a user's attributes (or entitlements) but not their identities.

Jorden Whitefield, Liqun Chen, Frank Kargl et al.

Research on vehicular networking (V2X) security has produced a range of security mechanisms and protocols tailored for this domain, addressing both security and privacy. Typically, the security analysis of these proposals has largely been informal. However, formal analysis can be used to expose flaws and ultimately provide a higher level of assurance in the protocols. This paper focusses on the formal analysis of a particular element of security mechanisms for V2X found in many proposals: the revocation of malicious or misbehaving vehicles from the V2X system by invalidating their credentials. This revocation needs to be performed in an unlinkable way for vehicle privacy even in the context of vehicles regularly changing their pseudonyms. The REWIRE scheme by Forster et al. and its subschemes BASIC and RTOKEN aim to solve this challenge by means of cryptographic solutions and trusted hardware. Formal analysis using the TAMARIN prover identifies two flaws with some of the functional correctness and authentication properties in these schemes. We then propose Obscure Token (OTOKEN), an extension of REWIRE to enable revocation in a privacy preserving manner. Our approach addresses the functional and authentication properties by introducing an additional key-pair, which offers a stronger and verifiable guarantee of successful revocation of vehicles without resolving the long-term identity. Moreover OTOKEN is the first V2X revocation protocol to be co-designed with a formal model.

Steve Schneider, Helen Treharne, Heike Wehrheim et al.

Refinement in Event-B supports the development of systems via proof based step-wise refinement of events. This refinement approach ensures safety properties are preserved, but additional reasoning is required in order to establish liveness and fairness properties. In this paper we present results which allow a closer integration of two formal methods, Event-B and linear temporal logic. In particular we show how a class of temporal logic properties can carry through a refinement chain of machines. Refinement steps can include introduction of new events, event renaming and event splitting. We also identify a general liveness property that holds for the events of the initial system of a refinement chain. The approach will aid developers in enabling them to verify linear temporal logic properties at early stages of a development, knowing they will be preserved at later stages. We illustrate the results via a simple case study.

Chris Culnane, Peter Y. A. Ryan, Steve Schneider et al.

The Pret a Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this paper we present a case study of our efforts to adapt Pret a Voter to the idiosyncrasies of elections in the Australian state of Victoria. This technical report includes general background, user experience and details of the cryptographic protocols and human processes. We explain the problems, present solutions, then analyse their security properties and explain how they tie in to other design decisions. We hope this will be an interesting case study on the application of end-to-end verifiable voting protocols to real elections. A preliminary version of this paper appeared as the 10th February 2014 version of "Draft Technical Report for VEC vVote System". The team involved in developing the vVote design described in this report were: Craig Burton, Chris Culnane, James Heather, Rui Joaquim, Peter Y. A. Ryan, Steve Schneider and Vanessa Teague.

Chris Culnane, Steve Schneider

The Web Bulletin Board (WBB) is a key component of verifiable election systems. It is used in the context of election verification to publish evidence of voting and tallying that voters and officials can check, and where challenges can be launched in the event of malfeasance. In practice, the election authority has responsibility for implementing the web bulletin board correctly and reliably, and will wish to ensure that it behaves correctly even in the presence of failures and attacks. To ensure robustness, an implementation will typically use a number of peers to be able to provide a correct service even when some peers go down or behave dishonestly. In this paper we propose a new protocol to implement such a Web Bulletin Board, motivated by the needs of the vVote verifiable voting system. Using a distributed algorithm increases the complexity of the protocol and requires careful reasoning in order to establish correctness. Here we use the Event-B modelling and refinement approach to establish correctness of the peered design against an idealised specification of the bulletin board behaviour. In particular we show that for n peers, a threshold of t > 2n/3 peers behaving correctly is sufficient to ensure correct behaviour of the bulletin board distributed design. The algorithm also behaves correctly even if honest or dishonest peers temporarily drop out of the protocol and then return. The verification approach also establishes that the protocols used within the bulletin board do not interfere with each other. This is the first time a peered web bulletin board suite of protocols has been formally verified.