Joeri de Ruiter
Promotor: prof.dr. B.P.F. Jacobs (RU)
Copromotor: dr.ir. E. Poll (RU)
Radboud Universiteit Nijmegen
Date: 27 August 2015, 14:30
Security protocols play an important role in our everyday life. In particular, they are used when paying with bank cards or performing online payments. In this thesis we look at the complex security protocols that are used in these systems: the EMV protocol family, used in bank cards, and the TLS protocol, used to secure network connections. Just the specifications of these protocols can already be hundreds of pages long. We analyse these protocols from different angles. On the one hand we perform a formal analysis of protocol specifications. For this analysis we specify the protocol in F# and make use of the ProVerif tool for the verification. On the other hand we also look at actual implementations of protocols. For this we make use of automated learning techniques to infer state machines from implementations of security protocols.
The first protocol we discuss is EMV, the world’s leading standard for payments with smart cards: at the moment over 1.5 billion EMV cards are in use and worldwide almost all bank cards with a chip on them are EMV compliant. The core specifications are over 700 pages and every payment processor has additional proprietary specifications on top of this. Using ProVerif and FS2PV we analysed the EMV specifications, modelled in F#. Though the model was quite large and resulted in an even larger pi-calculus model, we were still able to perform an automated analysis. This revealed known weaknesses for EMV. To analyse implementations of EMV, we performed an analysis using automated learning techniques on EMV bank cards.
For internet banking, many banks let their clients use a hand-held smart card reader with a small display and keypad. In combination with a smart card and PIN code, this reader then signs challenges provided on the bank’s website, to either log in or confirm bank transfers. Many of these systems use a proprietary standard of MasterCard called the Chip Authentication Program, also known as EMV-CAP. This standard is based on the EMV standard. We analysed a device used for online banking that makes use of this security protocol, the e.dentifier2. Both a manual and a automated analyses were performed of this device that show that it contains a security issue. Based on our observations we present a solution, called the Radboud Reader, to secure online transactions that provides stronger security guarantees than existing solutions.
When using online banking websites, or visiting other websites for which security is important, the TLS protocol is used. Using the same automated learning techniques as we used in the previous analyses, we analyse eight different TLS implementations. This resulted in the discovery of various security flaws and functional bugs in widely used implementations.