You are here:

Dr James Heather

Senior Lecturer

Qualifications: BA (Oxon) MSc (Oxon) PhD (Lond)

Email:
Phone: Work: 01483 68 9636
Room no: 07 BB 02

Office hours

Thursdays, 2pm to 4pm

Further information

Research Interests

My main focus is on the application of formal methods to computer security problems.

For the first part of my career, this largely involved analysing security protocols using the process algebra CSP, and either finding attacks or proving that no attacks existed.

More recently I have spent most of my time working on secure electronic voting. I am leading the EPSRC-funded Trustworthy Voting Systems research project at Surrey, which aims to design, develop and verify a secure voting system that is strong enough and usable enough for real-world elections. The project is joint work with Birmingham, and run in close collaboration with Luxembourg.

Publications

Highlights

  • Heather JA, Llewellyn MH, Teague VJ, Wen R. (2012) 'On the Side-Effects of Introducing E-voting'. Springer Lecture Notes in Computer Science: E-Voting and Identity, Tallinn, Estonia: VoteID 2011: Third International Conference 7187, pp. 242-256.
    doi: 10.1007/978-3-642-32747-6_15
  • Schneider SA, Srinivasan S, Culnane C, Heather JA, Xia Z. (2012) 'Prêt à Voter with Write-Ins'. Springer Lecture Notes in Computer Science: E-Voting and Identity, Tallinn, Estonia: VoteID 2011: Third International Conference 7187, pp. 174-189.
    doi: 10.1007/978-3-642-32747-6_11
  • Heather J, Ryan PYA, Teague V. (2010) 'Pretty good democracy for more expressive voting schemes'. Springer Lecture Notes in Computer Science: Computer Security – ESORICS 2010, Athens, Greece: 15th European Symposium on Research in Computer Security 6345, pp. 405-423.
    doi: 10.1007/978-3-642-15497-3_25
    Full text is available at: http://epubs.surrey.ac.uk/107388/

    Abstract

    In this paper we revisit Pretty Good Democracy, a scheme for verifiable Internet voting from untrusted client machines. The original scheme was designed for first-past-the-post elections. Here, we show how Pretty Good Democracy can be extended to voting schemes in which the voter lists the candidates in their order of preference. Our scheme applies to elections using STV, IRV, Borda, or any other tallying scheme in which a vote is a list of candidates in preference order. We also describe an extension to cover Approval or Range voting.

  • Ryan PYA, Bismark D, Heather JA, Schneider SA, Xia Z. (2009) 'The Prêt à Voter Verifiable Election System'. IEEE IEEE Transactions on Information Forensics and Security, 4 (4), pp. 662-673.
    doi: 10.1109/TIFS.2009.2033233
    Full text is available at: http://epubs.surrey.ac.uk/7244/

    Abstract

    The Prˆet `a Voter election system has undergone several revisions and enhancements since its inception in 2004, resulting in a family of election systems designed to provide end-to-end verifiability and a high degree of transparency while ensuring secrecy of the ballot. Assurance for these systems arises from the auditability of the election itself, rather than the need to place trust in the system components. This paper brings together the variations of Prˆet `a Voter, presents their design, describes the voter experience, and considers the security properties that they provide.

  • Heather JA, Lundin D. (2008) 'The Append-only Web Bulletin Board'. Malaga, Spain : Springer-Verlag Lecture Notes in Computer Science: Formal Aspects in Security and Trust, Malaga, Spain: FAST 2008 5491, pp. 242-256.
    doi: 10.1007/978-3-642-01465-9_16

Journal articles

  • Heather JA. (2010) 'Turnitoff: identifying and fixing a hole in current plagiarism detection software'. Routledge Journal of Assessment and Evaluation in Higher Education, 35 (6), pp. 647-660.
    doi: 10.1080/02602938.2010.486471
    Full text is available at: http://epubs.surrey.ac.uk/107387/

    Abstract

    In recent times, plagiarism detection software has become popular in universities and colleges, in an attempt to stem the tide of plagiarised student coursework. Such software attempts to detect any copied material and identify its source. The most popular such software is Turnitin, a commercial system used by thousands of institutions in more than 100 countries. Here, we show how to fix a loophole in Turnitin's current plagiarism detection process. We demonstrate that, in its current incarnation, one can easily create a document that passes the plagiarism check regardless of how much copied material it contains; we then show how to improve the system to avoid such attacks.

  • Ryan PYA, Bismark D, Heather JA, Schneider SA, Xia Z. (2009) 'The Prêt à Voter Verifiable Election System'. IEEE IEEE Transactions on Information Forensics and Security, 4 (4), pp. 662-673.
    doi: 10.1109/TIFS.2009.2033233
    Full text is available at: http://epubs.surrey.ac.uk/7244/

    Abstract

    The Prˆet `a Voter election system has undergone several revisions and enhancements since its inception in 2004, resulting in a family of election systems designed to provide end-to-end verifiability and a high degree of transparency while ensuring secrecy of the ballot. Assurance for these systems arises from the auditability of the election itself, rather than the need to place trust in the system components. This paper brings together the variations of Prˆet `a Voter, presents their design, describes the voter experience, and considers the security properties that they provide.

  • Heather J, Wei K. (2009) 'Where next for formal methods?'. Springer Lecture Notes in Computer Science, 5087, pp. 52-58.
    doi: 10.1007/978-3-642-04904-0_10
    Full text is available at: http://epubs.surrey.ac.uk/107397/
  • Heather J. (2007) 'Implementing STV securely in Prêt à Voter'. Proceedings - IEEE Computer Security Foundations Symposium, , pp. 157-169.
    doi: 10.1109/CSF.2007.22
  • Wei K, Heather J. (2006) 'Towards verification of timed non-repudiation protocols'. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3866 LNCS, pp. 244-257.
    doi: 10.1007/11679219_18
  • Wei K, Heather J. (2005) 'Embedding the stable failures model of CSP in PVS'. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3771 LNCS, pp. 246-265.
    doi: 10.1007/11589976_15
  • Heather J, Schneider S. (2005) 'A decision procedure for the existence of a rank function'. IOS Press Journal of Computer Security, 13 (2), pp. 317-344.
    Full text is available at: http://epubs.surrey.ac.uk/107394/

    Abstract

    Schneider’s work on rank functions [17] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only with a protocol running on a small network; and no help is given with the somewhat hit-and-miss process of finding the rank function that underpins the central theorem. In this paper, we develop the theory to allow for an arbitrarily large network, and give a clearly defined decision procedure by which one may either construct a rank function, proving correctness of the protocol, or show that no rank function exists. We briefly discuss the implications of the absence of a rank function, and the open question of completeness of the rank function theorem.

  • Antonopoulos N, Heather J, Peel R. (2005) 'Programmable agents for generic distributed authorisation'. Proceedings of the 2005 International Conference on Internet Computing, ICOMP'05, , pp. 174-180.
  • Heather J, Lowe G, Schneider S. (2003) 'How to prevent type flaw attacks on security protocols'. IOS Press Journal of Computer Security, 11 (2), pp. 217-244.
    doi: 10.1109/CSFW.2000.856942
    Full text is available at: http://epubs.surrey.ac.uk/107395/

    Abstract

    A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number of type flaw attacks have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevented using a simple technique of tagging each field with some information indicating its intended type.

Conference papers

  • Burton C, Culnane C, Heather JA, Peacock T, Ryan PYA, Schneider SA, Srinivasan S, Teague V, Wen R, Xia Z. (2012) 'Using Pret a Voter in Victorian State elections'. 2012 Electronic Voting Technology/Workshop on Electronic Voting
    Full text is available at: http://epubs.surrey.ac.uk/726039/

    Abstract

    The Pret a Voter cryptographic voting system was designed to be flexible and to off er voters a familiar and easy voting experience. In this paper we present a case study of our e fforts to adapt Pret a Voter to the idiosyncrasies of elections in the Australian state of Victoria. The general background and desired user experience have previously been described; here we concentrate on the cryptographic protocols for dealing with some unusual aspects of Victorian voting. 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 verifi able voting protocols to real elections

  • Burton C, Culnane C, Heather J, Peacock T, Ryan P, Schneider S, Srinivasan S, Teague V, Wen R, Xia Z. (2012) 'A Supervised Verifiable Voting Protocol for the Victorian Electoral Commission'. Lecture Notes in Informatics, Lochau/Bregenz, Austria: EVOTE 2012 205, pp. 82-95.
    Full text is available at: http://epubs.surrey.ac.uk/723026/

    Abstract

    This paper describes the design of a supervised verifiable voting protocol suitable for use for elections in the state of Victoria, Australia. We provide a brief overview of the style and nature of the elections held in Victoria and associated challenges. Our protocol, based on Prêt à Voter, presents a new ballot overprinting front-end design, which assists the voter in completing the potentially complex ballot. We also present and analyse a series of modifications to the back-end that will enable it to handle the large number of candidates, , with ranking single transferable vote (STV), which some Victorian elections require. We conclude with a threat analysis of the scheme and a discussion on the impact of the modifications on the integrity and privacy assumptions of Prêt à Voter.

  • Heather JA, Llewellyn MH, Teague VJ, Wen R. (2012) 'On the Side-Effects of Introducing E-voting'. Springer Lecture Notes in Computer Science: E-Voting and Identity, Tallinn, Estonia: VoteID 2011: Third International Conference 7187, pp. 242-256.
    doi: 10.1007/978-3-642-32747-6_15
  • Schneider SA, Heather JA. (2012) 'A Formal Framework for Modelling Coercion Resistance and Receipt Freeness'. Springer Lecture Notes in Computer Science, FM 2012: 18th International Symposium on Formal Methods 7436, pp. 217-231.
    Full text is available at: http://epubs.surrey.ac.uk/726040/

    Abstract

    Coercion resistance and receipt freeness are critical properties for any voting system. However, many di fferent de finitions of these properties have been proposed, some formal and some informal; and there has been little attempt to tie these definitions together or identify relations between them. We give here a general framework for specifying di fferent coercion resistance and receipt freeness properties using the process algebra CSP. The framework is general enough to accommodate a wide range of defi nitions, and strong enough to cover both randomization attacks and forced abstention attacks. We provide models of some simple voting systems, and show how the framework can be used to analyze these models under di fferent de finitions of coercion resistance and receipt freeness. Our formalisation highlights the variation between the defi nitions, and the importance of understanding the relations between them.

  • Schneider SA, Srinivasan S, Culnane C, Heather JA, Xia Z. (2012) 'Prêt à Voter with Write-Ins'. Springer Lecture Notes in Computer Science: E-Voting and Identity, Tallinn, Estonia: VoteID 2011: Third International Conference 7187, pp. 174-189.
    doi: 10.1007/978-3-642-32747-6_11
  • Culnane C, Bismark D, Heather JA, Schneider SA, Srinivasan S, Xia Z. (2011) 'Authentication Codes'. Electronic Voting Technology Workshop on Trustworthy Elections, San Francisco, USA: EVT/WOTE 2011
    Full text is available at: http://epubs.surrey.ac.uk/107386/

    Abstract

    The Prêt à Voter end-to-end verifiable voting system makes use of receipts, retained by voters, to provide individual verifiability that their vote has been recorded as cast. The paper discusses issues around the production and acceptance of receipts, and presents an alternative approach to individual verifiability based on Authentication Codes. These codes are constructed, in the encrypted domain, by the peered Web Bulletin Board when the vote is cast, and provide the voter with an assurance that their vote has been properly received. The approach is designed to work in a uniform way with ranked elections and single preference elections.

  • Heather JA, Schneider SA, Teague VJ. (2011) 'Cryptographic Protocols with Everyday Objects'. Limerick: CryptoForma 2011
  • Moran M, Heather JA, Schneider SA. (2011) 'Anonymity and CSP for Voting Systems'. Limerick: CryptoForma 2011
    Full text is available at: http://epubs.surrey.ac.uk/721384/
  • Schneider S, Llewellyn M, Culnane C, Heather J, Srinivasan S, Xia Z. (2011) 'Focus group views on Prêt à Voter 1.0'. Proc. of 2011 Int. Workshop on Requirements Engineering for Electronic Voting Systems, REVOTE 2011 - In Conjunction with the 19th IEEE International Requirements Engineering Conference 2011, RE 2011, , pp. 56-65.
    doi: 10.1109/REVOTE.2011.6045916
    Full text is available at: http://epubs.surrey.ac.uk/107391/

    Abstract

    This paper discusses the findings of a series of four focus group sessions carried out on a variant of the original Prêt à Voter prototype implementation [2]. The aim of these sessions was to investigate users' ability to use the system, to discover any inadequacies of the system, and to gauge the participants' understanding of its security mechanisms. The groups also discussed general issues around security in election systems.

  • Heather J, Ryan PYA, Teague V. (2010) 'Pretty good democracy for more expressive voting schemes'. Springer Lecture Notes in Computer Science: Computer Security – ESORICS 2010, Athens, Greece: 15th European Symposium on Research in Computer Security 6345, pp. 405-423.
    doi: 10.1007/978-3-642-15497-3_25
    Full text is available at: http://epubs.surrey.ac.uk/107388/

    Abstract

    In this paper we revisit Pretty Good Democracy, a scheme for verifiable Internet voting from untrusted client machines. The original scheme was designed for first-past-the-post elections. Here, we show how Pretty Good Democracy can be extended to voting schemes in which the voter lists the candidates in their order of preference. Our scheme applies to elections using STV, IRV, Borda, or any other tallying scheme in which a vote is a list of candidates in preference order. We also describe an extension to cover Approval or Range voting.

  • Xia Z, Culnane C, Heather JA, Jonker H, Ryan PYA, Schneider SA, Srinivasan S. (2010) 'Versatile Pret a Voter: Handling Multiple Election Methods with a Unified Interface'. Springer-Verlag Lecture Notes in Computer Science, Hyderabad, India: Indocrypt 6498, pp. 98-114.
    doi: 10.1007/978-3-642-17401-8_8010
    Full text is available at: http://epubs.surrey.ac.uk/7233/

    Abstract

    A number of end-to-end veri¯able voting schemes have been introduced recently. These schemes aim to allow voters to verify that their votes have contributed in the way they intended to the tally and in addition allow anyone to verify that the tally has been generated correctly. These goals must be achieved while maintaining voter privacy and providing receipt-freeness. However, most of these end-to-end voting schemes are only designed to handle a single election method and the voter interface varies greatly between different schemes. In this paper, we introduce a scheme which handles many of the popular election methods that are currently used around the world. Our scheme not only ensures privacy, receipt-freeness and end-to-end veri¯ability, but also keeps the voter interface simple and consistent between various election methods.

  • Bismark D, Heather J, Peel RMA, Schneider S, Xia Z, Ryan PYA. (2009) 'Experiences gained from the first Prêt à Voter implementation'. 2009 1st International Workshop on Requirements Engineering for e-Voting Systems, RE-VOTE 2009, , pp. 19-28.
    doi: 10.1109/RE-VOTE.2009.5
    Full text is available at: http://epubs.surrey.ac.uk/7211/

    Abstract

    Implementing an electronic voting system for the first time can be difficult, since requirements are sometimes hard to specify and keep changing, resources are scarce in an academic setting, the gap between theory and practice is wider than anticipated, adhering to a formal development lifecycle is inconvenient and delivery on time is very hard. This paper describes all of the work done by the Prêt à Voter team in the run-up to VoComp in 2007 and enumerates a number of lessons learned.

  • Heather J. (2009) 'Where next for formal methods? (Transcript of Discussion)'. Springer Lecture Notes in Computer Science: Security Protocols, Cambridge, UK: 14th International Workshop 5087, pp. 59-61.
    doi: 10.1007/978-3-642-04904-0
  • Heather JA, Lundin D. (2008) 'The Append-only Web Bulletin Board'. Malaga, Spain : Springer-Verlag Lecture Notes in Computer Science: Formal Aspects in Security and Trust, Malaga, Spain: FAST 2008 5491, pp. 242-256.
    doi: 10.1007/978-3-642-01465-9_16
  • Xia Z, Schneider SA, Heather J, Traoré J. (2008) 'Analysis, Improvement, and Simplification of Prêt à Voter with Paillier Encryption.'. Berkeley, CA : USENIX Association EVT'08 Proceedings of the Conference on Electronic Voting Technology, San Jose, USA: USENIX/ACCURATE Electronic Voting Workshop
    Full text is available at: http://epubs.surrey.ac.uk/7188/

    Abstract

    In this paper, we analyse information leakage in Ryan’s Prˆet `a Voter with Paillier encryption scheme (PAVPaillier). Our analysis shows that although PAV-Paillier seems to achieve a high level of voter privacy at first glance, it might still leak voter’s choice information in some circumstances. Some threats are trivial and have appeared in the literature, but others are more complicated because colluding adversaries may apply combined attacks. Several strategies have been suggested to mitigate these threats, but we have not resolved all the threats. We leave those unsolved threats as open questions. In order to describe our analysis in a logical manner, we will introduce an information leakage model to aid our analysis. We suggest that this model can be applied to analyse information leakage in other complex mixnet based e-voting schemes as well. Furthermore, we introduce a simplification of PAVPaillier. In our proposal, without degrading security properties such as voter privacy, verifiability and reliability, we no longer need to apply the homomorphic property to absorb the voter’s choice index into the onion, thus we step back to employ the ElGamal encryption. This results in a simpler and more straightforward threshold cryptosystem. Some other attractive properties of our proposal scheme are: unlike traditional Prˆet `a Voter schemes, the candidate list in our scheme can be in alphabetical order. Our scheme not only handles approval elections, but also it handles ranked elections (e.g. Single Transferable Voting). Furthermore, our scheme mitigates the randomisation attack.

  • Xia Z, Schneider SA, Heather JA, Ryan PYA, Lundin D, Peel RMA, Howard PJ. (2007) 'Prêt à Voter: All-in-one'. Ottawa, Canada : Ottawa, Canada: IAVoSS Workshop On Trustworthy Elections (WOTE 2007)
    Full text is available at: http://epubs.surrey.ac.uk/107398/

    Abstract

    A number of voter-verifiable electronic voting schemes have been introduced in the recent decades. These schemes not only provide each voter with a receipt without the threat of coercion and ballot selling, but also the ballot tallying phase can be publicly verified. Furthermore, these schemes are robust because the power of authorities can be threshold distributed. Generally speaking, the homomorphic encryption schemes are efficient but they are unable to handle some preferential elections, such as STV elections and Condorcet elections. The mix network schemes are versatile, but they are not as efficient as the homomorphic encryption schemes in approval elections. In this paper, we will present a new electronic voting schemes which is secure, versatile and efficient. We call our proposal scheme the Prˆet `a Voter: All-In-One because it is based on the re-encryption version of the Prˆet `a Voter scheme and inherits most of its security properties. Our scheme not only handles both approval elections and preferential elections, but also the ballot tallying phase will always be the most efficient because according to different elections, different tally strategies can be applied.

  • Wei K, Heather J. (2007) 'A theorem-proving approach to verification of fair non-repudiation protocols'. Springer Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Hamilton, Canada: 4th International Workshop on Formal Aspects in Security and Trust 4691 LNCS, pp. 202-219.
    Full text is available at: http://epubs.surrey.ac.uk/738611/

    Abstract

    We use a PVS embedding of the stable failures model of CSP to verify non-repudiation protocols, allowing us to prove the correctness of properties that are difficult to analyze in full generality with a model checker. The PVS formalization comprises a semantic embedding of CSP and a collection of theorems and proof rules for reasoning about non-repudiation properties. The well-known Zhou-Gollmann protocol is analyzed within this framework. © Springer-Verlag Berlin Heidelberg 2007.

  • Lundin D, Treharne HE, Ryan PYA, Schneider SA, Heather JA, Xia Z. (2006) 'Tear and Destroy: Chain voting and destruction problems shared by Prêt à Voter and Punchscan and a solution using Visual Encryption'. Hamburg, Germany: IAVoSS Workshop on Frontiers in Electronic Elections (FEE 2006)
    Full text is available at: http://epubs.surrey.ac.uk/107399/

    Abstract

    Prˆet `a Voter and Punchscan are two electronic voting schemes that both use paper based ballot forms, part of which is detached and destroyed, to provide receipt-free voter verifiability. However, both schemes share the chain voting problem and the part destruction problem. The first is where anyone who can see the ballot form before it is used can coerce a voter who uses it and the latter where a voter who can leave with the complete form can prove to a coercer the contents of the vote. In this paper we provide a comparison of the schemes from a systems perspective. We also introduce a visual encryption solution to both the above problems.

  • Lundin D, Treharne HE, Ryan PYA, Schneider SA, Heather JA. (2006) 'Distributed Creation of the Ballot Form in Prêt à Voter using an element of Visual Encryption'. Cambridge, UK : IAVoSS Workshop On Trustworthy Elections (WOTE 2006), IAVoSS Workshop On Trustworthy Elections (WOTE 2006)
    Full text is available at: http://epubs.surrey.ac.uk/107400/
  • Heather J, Schneider S. (2006) 'To infinity and beyond or, avoiding the infinite in security protocol analysis'. Proceedings of the ACM Symposium on Applied Computing, 1, pp. 346-353.
  • Lundin D, Treharne HE, Ryan PYA, Schneider SA, Heather JA, Xia Z. (2006) 'Tear and Destroy: Chain voting and destruction problems shared by Prêt à Voter and Punchscan and a solution using Visual Encryption'. EATCS Fundamenta Informaticae (Journal of Fundamental Informatics), , pp. 1001-1019.