Scalable mobile payment

For more info about our services contact : help@bestpfe.com

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