Project Topics
Get Complete Project Material File(s) Now! »
Mobile payment: a token-based payment protocol for mobile devices
Mobile phones have been extensively used since their launching to perform or confirm transactions. We can use them to secure Internet transactions by providing a two factors authorization process as in 3D-Secure[97, 56] or even directly pay from them on merchants website, whether it is from a browser of with a “payment button” as in Apple Pay. In some countries they are even used to process to peer to peer payment and are reliable in continents where the vast majority of the population do not own a bank account, as in Africa. And last but not least, smartphones are now able to fully emulate payment cards to process to NFC-based payment and the competition is fierce between all new payment applications (Apple Pay, Android Pay, Samsung Pay, Orange Cash, Paylib…).
Scalable mobile payment
As stated before, the competition between payment applications is fierce. Yet, security breaches on those applications are regularly found [88]. Partly due to the fact that there is no standard describing the exact requirements of mobile payment applications – merely frameworks or white papers – and the fact that each major actor in the market keep the specifications of their solutions away from the public eyes.
Nonetheless, one common ground between all of these applications is the fact that to be competitive, they must be as much scalable as possible. In the payment world, this means complying with existing standards for payments, usually card-based. The most widely deployed standard about payment is the EMV Chip and PIN standard, issued by the consortium EMVCo regrouping major card constructors such as Visa or MasterCard. For an application to be scalable without needing a massive update on merchant terminals, It is critical to be compatible with this specification.
Regarding the security management of mobile payment solutions, two main trends can be identified. The first one emulates the payment card inside a tamper-resistant hardware called a Secure Element, as in Apple Pay or Orange Cash. Development and maintenance costs are expensive for such solutions but it inherits the security of Chip and PIN cards. The second trends emulates the payment card directly from the smart device main OS, as in Android Pay. Such solutions are highly flexible and cheaper to maintain and develop but the security is more fragile than in Secure Element-centric solutions.
We proposed a payment protocol along its security proof that was proven secure even if the client device is infected.
Formally proving the security of the mobile payment protocol with the Tamarin prover
EMV standard protocols have been formally studied in [44]. Yet, the analysis the payment data authen-tication protocols as defined by EMV assumes that the device holding the payment data – in this case, the Chip and PIN card – is honest. This is a reasonable assumptions in this scenario since a payment card provided by the issuer in not an active device connected to a public network, something that is no longer the case when considering a mobile payment application. Critical payment data are held in an environment that could be compromised by a malware in the mobile environment. Hence, we needed to prove the security of our mobile payment application in the context of a compromised device.
One of the main difficulties regarding the security proof of our protocol was embodied by the fact that we rely on the use of counters and counter verification in it. This is a feature that is not supported efficiently by ProVerif. Thus, we used the Tamarin prover tool to process our security proof, adding one more use case to the tool application.
Combining verifiability and privacy in voting schemes: from Helios to Belenios RF
The first part of this thesis will focus on specifying an electronic voting protocol that guarantees both verifiability and privacy even if it is performed using compromised devices from the user point of view or if the election administrators are rogue. It allows online internet voting.
The protocol itself is a variant of an existing voting scheme, Belenios Receipt-Free (Belenios RF) [29], which is itself an extension of Belenios [38], which was built upon Helios [3, 4]. This chapter will depict the evolution from Helios to Belenios RF by providing an overview of what these protocols have to offer and what are their limits.
Helios: a web-based open-audit voting scheme
Helios [3, 4] is presented as “the first web-based open-audit voting system” and was launched in 2008. From a voter point of view, it can be run from a modern web browser. The voter computes their vote from their browser and cast it to a voting server after an authentication. The bulletin board is publicly accessible. At the end of the tally process, the election result can be audited by anyone by relying on publicly available data.
Helios was used several times to run real-world elections such as the election of the University of Louvain-la-Neuve president from 2010 to 2012 or the International Association for Cryptographic Research board members since 2011. This protocol has the advantage of its simplicity and was designed to achieve both verifiability and privacy. The following section provides some insights about the way Helios works and its security features.
An overview of the Helios voting scheme
The first version of Helios technically relied on the combination of two cryptographic protocols: the ballot casting approach from Benaloh [18] and the Sako-Killian mixnet [103]. The first one proposes a rather simple way to obtain verifiable elections by following a specific scheme during ballot casting while the second one focuses on the tally part by providing a provable shuffling of the ballot box to ensure privacy and decrypt all ballots one by one.
The current version of Helios – Helios v.4 – does not rely on a mixnet for tally anymore. Instead, it relies on homomorphic encryption: the whole result is obtained from the global decryption of ballots rather than an individual decryption, an operation that is made possible thanks to an inherent property of the El Gamal asymmetric encryption scheme Helios relies on to encrypt the ballots. This kind of tally has the advantage of requiring only one server – instead of several for the good tally execution. Like Helios v.1, the tally is output with a proof of good computation.
We have two main phases during an election: the voting phase during which electors cast their ballots and the tallying phase which computes the election result.
The main entities interacting in the voting scheme are the election administrator who sets the election up, the voter and their web browser, the voting server which administrates the public bulletin board and the tallying authority in charge of tallying the election – this last entity could be a group of several tallying authorities, by sharing the election secret key among several entities using a threshold cryptosystem.
Belenios: strengthening Helios’ verifiability with credentials
Belenios [38] is a voting scheme built upon Helios that was proposed by Véronique Cortier, David Galindo, Stéphane Glondu and Malika Izabachène. It addresses both the problem of potentially display-ing the voter’s identity along their ballot and the fact that there is no efficient control over the voting server by adding another entity to the whole Helios voting ecosystem: a registrar.
The registrar provides each voters with cryptographic signature credentials. It creates one credential per eligible voter and provides them to the voter. Each voter signs their ballot and cast them. The ballot are displayed along the public signing credential on the bulletin board.
We propose an overview of the Belenios voting protocol, explicitly stating the differences with Helios and discuss its security features in the following section.
The main entities participating to the Belenios voting scheme are almost the same as in Helios. The election administrator sets the election up, voters participates to the election through their web browser, the voting server provides each eligible voters authentication credential to cast a ballot and the tallying authority – or authorities, if a threshold cryptosystem is used – is in charge of computing the election result.
A new entity is introduced to this ecosystem: the registrar. In addition to their authentication cre-dentials received from the voting server, voters receive voting credentials from the registrar – provided via a different channel than the one that was used to provide the authentication credentials. The voting credentials are a pair of asymmetric encryption key that are used by the voter through their device to sign their ballot.
[38] proposes a generic construction that transforms any voting scheme that is verifiable under the assumption that both the voting server and the registrar are honest – or, if there is no registrar, that the voting server is honest – into a voting protocol that is verifiable under the assumption that at least one of both entities is honest.
Belenios relies on El Gamal encryption to encrypt the votes [48], like Helios, and on Schnorr signa-tures to sign the ballots [105].
Table of contents :
Introduction
1 Secure design of cryptographic protocols
1.1 An example of protocol: the Helios voting scheme
1.2 An error-prone task
1.3 Protocol security proofs in the symbolic model
2 Scope of this thesis
3 Electronic voting: the Belenios VS voting scheme
3.1 Web-based voting
3.2 Contributions
4 Mobile payment: a token-based payment protocol for mobile devices
4.1 Scalable mobile payment
4.2 Contributions
5 Thesis outline
Chapter 1 Protocol Modeling
1.1 Syntax
1.1.1 Terms
1.1.2 Expression evaluation
1.1.3 Equations and formulas
1.1.4 Processes
1.2 Semantics
1.2.1 Semantic configuration
1.2.2 Reduction
1.2.3 Trace
1.3 Security Properties
1.3.1 Trace properties
1.3.2 Equivalence Properties
Part I Voting Protocol
Chapter 2 Belenios VS
2.1 Combining verifiability and privacy in voting schemes: from Helios to Belenios RF
2.1.1 Helios: a web-based open-audit voting scheme
2.1.2 Belenios: strengthening Helios’ verifiability with credentials
2.1.3 Belenios Receipt-Free: adding ballot randomization to achieve strong receiptfreeness
2.1.4 Motivations to improve Belenios RF
2.2 Presentation of the protocol
2.2.1 Election ecosystem, entities and voting material
2.2.2 The cryptography behind our protocol
2.2.3 An overview of our protocol
2.3 Threat model
2.3.1 Threats
2.3.2 Communication model
2.3.3 Corruption scenarii
2.4 Security claims
2.4.1 Verifiability
2.4.2 Privacy
2.4.3 Our protocol security against several corruption scenarii
Chapter 3 Achieving verifiability with ProVerif provable properties
3.1 Formalizing verifiability
3.1.1 Sets and multisets
3.1.2 Election related functions
3.1.3 Events and events-defined multisets
3.1.4 Security assumptions and hypothesis on a voting protocol
3.1.5 Verifiability
3.2 Verifiability based on correct authentication
3.2.1 Trace properties satisfied in the context of a correct authentication
3.2.2 A theorem for verifiability based on a correct authentication
3.2.3 Proof
3.3 Verifiability assuming a correct use of voting credentials
3.3.1 An additional hypothesis on a honest registrar’s behaviour
3.3.2 ProVerif provable properties
3.3.3 A theorem for verifiability based on the correct use of voting credentials
3.3.4 Proof
Chapter 4 Security analysis of Belenios VS
4.1 Verifiability of our protocol
4.1.1 ProVerif models
4.1.2 Formal properties in the ProVerif calculus
4.1.3 Results
4.2 Privacy of our protocol
4.2.1 Formalizing the vote confidentiality
4.2.2 ProVerif models
4.2.3 Results
Part II Payment Protocol
Chapter 5 A landscape of the mobile payment industry and its main limitations
5.1 Technical Constraints
5.1.1 EMV compliance
5.1.2 Security Management of Mobile Payment Solutions
5.1.3 Tokenisation
5.2 A survey of existing mobile payment solutions
5.2.1 Apple Pay
5.2.2 Google Wallet and Android Pay
5.2.3 Samsung Pay
5.2.4 Orange Cash
5.3 Improvement possibilities regarding mobile payment applications
5.3.1 Devising an open mobile payment protocol specification
5.3.2 Improving the security management
5.3.3 Adding some privacy
Chapter 6 Designing an EMV-compliant Payment Protocol for Mobile Devices
6.1 Presentation of our protocol
6.1.1 Entities
6.1.2 Token provisioning request and process
6.1.3 EMV-compliant token-based payment
6.2 Trust Assumptions
6.2.1 Threat Model
6.2.2 Communication Model
6.3 Security Claims
6.3.1 Mandatory transaction agreement by the user
6.3.2 Merchant payment assurance
6.3.3 Injective Token Provisioning
6.3.4 Injective token-based payment
6.3.5 Token stealing window
6.3.6 Client payment unlinkability
6.4 A Practical Solution
Chapter 7 A Formal Analysis of our Payment Protocol
7.1 Tamarin prover
7.1.1 Message theory
7.1.2 Protocol representation by state transition systems
7.1.3 Security properties specification
7.1.4 Counter representation
7.2 Protocol model and formal properties
7.2.1 Protocol model for trace properties
7.2.2 Formalizing trace properties
7.2.3 The case of payment unlinkability
7.3 Proving the security of our protocol
7.3.1 Using the interactive mode to achieve some proofs
7.3.2 Results
7.3.3 The importance of tagging
7.3.4 Comparing our protocol with existing EMV attacks
Conclusion and perspectives
1 On web-based voting
1.1 Belenios VS: a verifiable and private voting protocol that is secure even if the user’s device is compromised
1.2 Proposing a method to automatize the verifiability proof in the symbolic model153
2 On mobile payment
2.1 Devising an open end-to-end mobile payment protocol
2.2 A framework for tokenised services
Bibliography
