EMV Joeri de Ruiter Digital Security, Radboud University Nijmegen Overview ● ● EMV ● Introduction ● Weaknesses ● Formal verification EMV-CAP ● ● e.dentifier2 Automated analysis Joeri de Ruiter - Digital Security, Radboud University Nijmegen 2 / 64 What is EMV? Standard for payments using smart cards Joeri de Ruiter - Digital Security, Radboud University Nijmegen 3 / 64 What is EMV? Developed and maintained Owned by Joeri de Ruiter - Digital Security, Radboud University Nijmegen 4 / 64 What is EMV? ● Protocol suite ● Initiated in 1993 ● Worldwide over 1,5 billion cards ● Introduced in the UK in 1997 ● Required in Dutch shops since 2012 ● Variants for contactless and internet banking Joeri de Ruiter - Digital Security, Radboud University Nijmegen 5 / 64 Why EMV? ● Prevent fraud ● Skimming ● Stolen cards ● Card-not-present fraud ● Single Euro Payments Area ● Liability shift ● Client if PIN used ● Merchant if magstripe is used Joeri de Ruiter - Digital Security, Radboud University Nijmegen 6 / 64 Skimming in the Netherlands 45 40 35 30 25 20 15 10 5 0 2007 2008 2009 2010 2011 2012 2013 Fraud in million euros Joeri de Ruiter - Digital Security, Radboud University Nijmegen 7 / 64 Skimming abroad ● Magstripe still present and used abroad ● EMV introduced in UK in 2006 2005 2006 2007 2008 Domestic 79 46 31 36 Foreign 18 53 113 134 Joeri de Ruiter - Digital Security, Radboud University Nijmegen 8 / 64 EMV specifications Joeri de Ruiter - Digital Security, Radboud University Nijmegen 9 / 64 EMV specifications ● Specification over 700 pages (4 books) ● ● ● Additional proprietary specifications Many options ● 3 card authentication methods ● 5 cardholder authentication methods ● 2 types of transactions Everything can be parameterised using Data Object Lists (DOLs) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 10 / 64 Key set-up ● Card and issuer: symmetric key ● ● Issuer: private/public keypair ● ● Authenticate cards Cards (optional): private/public keypair ● ● Authenticate transactions to bank Authenticate cards/transactions to terminal Terminal: public key payment scheme Joeri de Ruiter - Digital Security, Radboud University Nijmegen 11 / 64 EMV session ● Initialisation ● Select application ● Read data ● Card authentication ● Cardholder verification ● Transaction Joeri de Ruiter - Digital Security, Radboud University Nijmegen 12 / 64 Card authentication ● Static Data Authentication (SDA) ● Static data signed by issuer READ RECORD Sig((acc.nr., card nr., …), skBank) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 13 / 64 Card authentication ● Dynamic Data Authentication (DDA) ● Public key cryptography used ● Challenge/response mechanism READ RECORD Sig((acc.nr., …,pkCard), skBank) INTERNAL AUTH, nonceT Sig((nonceT, nonceK), skCard) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 14 / 64 Card authentication ● Combined Data Authentication (CDA) ● Transaction data signed ● Used in MasterCard PayPass cards READ RECORD Sig((acc.nr., …,pkCard), skBank) GENERATE AC, amount, nonceT, ... Sig((amount, nonceT, …, AC), skCard) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 15 / 64 Cardholder verification ● Based on transaction type ● None ● Signature ● PIN code ● Offline – ● With or without encryption Online Joeri de Ruiter - Digital Security, Radboud University Nijmegen 16 / 64 Cardholder verification ● Plaintext PIN verification VERIFY '1234' OK (9000) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 17 / 64 Transaction ● Application Cryptograms ● Transaction Certificate (TC) ● Application Authentication Cryptogram (AAC) ● Authorisation Request Cryptogram (ARQC) ● MAC over transaction data and Application Transaction Counter ● Online ● ● Authentication bank ● First ARQC, then TC Offline ● No contact bank Joeri de Ruiter - Digital Security, Radboud University Nijmegen 18 / 64 Attacking smart cards ● Direct access to memory not possible ● Passive ● ● ● Eavesdrop on communication Active ● Relay attacks ● Man-in-the-middle attack ● Modification of communication Side channels ● Timing ● Power consumption Joeri de Ruiter - Digital Security, Radboud University Nijmegen 19 / 64 Attacking smart cards Joeri de Ruiter - Digital Security, Radboud University Nijmegen 20 / 64 SmartLogic ● By Gerhard de Koning Gans Joeri de Ruiter - Digital Security, Radboud University Nijmegen 21 / 64 Known weaknesses ● Skimming ● Data on magnetic stripe also on chip ● Fake e.dentifiers ABN AMRO replaced in branches – – – 2008, 2009 1,5 milion euro damages Download-card Joeri de Ruiter - Digital Security, Radboud University Nijmegen 22 / 64 Known weaknesses ● Cloning SDA cards ● Possible for offline transactions ● Only static data authenticated ● No support for asymmetric crypto in card ● Yes-card – ● All PIN codes accepted SDA no longer allowed for offline capable cards Joeri de Ruiter - Digital Security, Radboud University Nijmegen 23 / 64 Known weaknesses ● DDA man-in-the-middle attack ● ● ● Possible for offline transactions Terminal cannot determine authenticity of a transaction Transaction not connected to card authentication INTERNAL AUTH, nonceT Sig((nonceT, nonceK), skKaart) GENERATE AC AC MitM Joeri de Ruiter - Digital Security, Radboud University Nijmegen 24 / 64 Known weaknesses ● “Chip & PIN is broken” [Murdoch et al. 2010] ● Possible for both offline and online transactions – – If card is not blocked If transaction without PIN are accepted ● Man-in-the-middle attack ● All PIN codes accepted ● Not possible in the Netherlands Joeri de Ruiter - Digital Security, Radboud University Nijmegen 25 / 64 Known weaknesses Source: https://www.cl.cam.ac.uk/research/security/banking/nopin/ Joeri de Ruiter - Digital Security, Radboud University Nijmegen 26 / 64 Known weaknesses ● “Chip & PIN is definitely broken” [Barisani et al. 2011] ● Rollback to plaintext PIN ● Terminals in the Netherlands patched ● Attack was still possible – Detected in backend Joeri de Ruiter - Digital Security, Radboud University Nijmegen 27 / 64 Complexity ● ● Over 700 pages in 4 books Little discussion of security goals or design choices Joeri de Ruiter - Digital Security, Radboud University Nijmegen 28 / 64 Complexity ● Many options and parameterisations ● 3 card authentication methods – ● 5 cardholder verification methods – ● PIN / Handwritten signature / None 2 types of transactions – ● SDA / DDA / CDA Online / offline Parameterisation using Data Object Lists Joeri de Ruiter - Digital Security, Radboud University Nijmegen 29 / 64 Formal verification - ProVerif ● Automated cryptographic protocol verifier ● Active / passive attacker ● Cryptography considered to be perfect ● Unbounded number of sessions ● Due to some approximations ● False attacks possible ● Claimed properties always hold Joeri de Ruiter - Digital Security, Radboud University Nijmegen 30 / 64 Formal verification - ProVerif ● Input in applied pi-calculus ● Queries ● Secrecy query attacker: M. ● Authenticity query ev:End ==> ev:Begin. query evinj:End ==> evinj:Begin. ● Attack reconstruction Joeri de Ruiter - Digital Security, Radboud University Nijmegen 31 / 64 F# ● Formalisation in F# ● Functional programming language ● Developed by Microsoft Research ● Executable code ● Translated to applied pi-calculus using FS2PV – – Subset of F# language More flexibility (sequential if-statements, functions) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 32 / 64 Formalisation ● Card and terminal formalised ● Options can be either unspecified or fixed ● DOLs fixed for Dutch banking cards ● 370 lines of F# code ● Over 2500 lines of applied pi-calculus Joeri de Ruiter - Digital Security, Radboud University Nijmegen 33 / 64 Formalisation Joeri de Ruiter - Digital Security, Radboud University Nijmegen 34 / 64 DDA // Perform DDA Authentication if requested, otherwise do nothing let card_dda (c, atc, (sIC,pIC), nonceC) dda_enabled = let data = Net.recv c in if Data.INTERNAL_AUTHENTICATE = APDU.get_command data then if dda_enabled then begin let nonceT = APDU.parse_internal_authenticate data in let signature = rsa_sign sIC (nonceC, nonceT) in Net.send c (APDU.internal_authenticate_response nonceC signature); Net.recv c end else failwith "DDA not supported by card" else data Joeri de Ruiter - Digital Security, Radboud University Nijmegen 35 / 64 Security properties ● Sanity checks ● Secrecy of private keys ● Highest supported authentication method used ● Transaction authentication Joeri de Ruiter - Digital Security, Radboud University Nijmegen 36 / 64 Security properties ● Card and terminal agree whether PIN is entered correctly evinj:TerminalVerifyPIN(True) ==> evinj:CardVerifyPIN(True) ● Transaction are authentic evinj:TerminalTransactionFinish(sda,dda,cda,pan,atc,True) ==> evinj:CardTransactionFinish(sda,dda,cda,pan,atc,True) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 37 / 64 EMV-CAP Joeri de Ruiter - Digital Security, Radboud University Nijmegen 38 / 64 EMV-CAP ● Used for online banking ● Based on EMV ● Not public ● Reverse engineered ● Handheld readers ● ● Rabobank (Random Reader) ● ABN AMRO (e.dentifier) Challenge-response Joeri de Ruiter - Digital Security, Radboud University Nijmegen 39 / 64 EMV-CAP PIN PIN OK challenge GENERATE AC (challenge,...) AC bitfilter(AC) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 40 / 64 EMV-CAP issues ● Overloading semantics [Drimer et al. 2009] ● ● Login same as 0 euro transfer No security against man-in-the-browser attack ● Challenges seem meaningless ● Data not always signed directly (Mode 2 + TDS) ● Easy verification of PIN code Joeri de Ruiter - Digital Security, Radboud University Nijmegen 41 / 64 EMV-CAP (Mode 2 +TDS) PIN PIN OK challenge GENERATE AC (0000,...) AC bitfilter(3DES(AC,challenge)) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 42 / 64 e.dentifier2 ● ● ● Developed by Todos (now Gemalto) Can be used with or without USB With USB: ● ● ● See-What-You-Sign “the most secure signwhat-you-see end user device ever seen” Good idea! Joeri de Ruiter - Digital Security, Radboud University Nijmegen 43 / 64 e.dentifier2 ● Text goes in plaintext over USB line ● PC can instruct device to show ● Predefined messages ● Any message to be signed Joeri de Ruiter - Digital Security, Radboud University Nijmegen 44 / 64 Protocol Joeri de Ruiter - Digital Security, Radboud University Nijmegen 45 / 64 Protocol Joeri de Ruiter - Digital Security, Radboud University Nijmegen 46 / 64 Protocol Joeri de Ruiter - Digital Security, Radboud University Nijmegen 47 / 64 Protocol Joeri de Ruiter - Digital Security, Radboud University Nijmegen 48 / 64 Automated analysis Joeri de Ruiter - Digital Security, Radboud University Nijmegen 49 / 64 From specification to implementation ● Specification analysed using formal methods ● How do we know this is actually implemented? ● Model based testing ● Automated learning Joeri de Ruiter - Digital Security, Radboud University Nijmegen 50 / 64 Automated learning ● ● ● LearnLib used Deterministic Mealy machine Equivalence queries approximated ● Random traces Joeri de Ruiter - Digital Security, Radboud University Nijmegen 51 / 64 Automated learning ● Custom test harness for EMV smartcards ● In total 15 different commands ● Input symbols: commands ● Output symbols: status words (optionally with cryptogram type) Joeri de Ruiter - Digital Security, Radboud University Nijmegen 52 / 64 Results Joeri de Ruiter - Digital Security, Radboud University Nijmegen 53 / 64 Results Joeri de Ruiter - Digital Security, Radboud University Nijmegen 54 / 64 Results Joeri de Ruiter - Digital Security, Radboud University Nijmegen 55 / 64 Maestro cards Rabobank Maestro Volksbank Maestro Joeri de Ruiter - Digital Security, Radboud University Nijmegen 56 / 64 EMV-CAP Joeri de Ruiter - Digital Security, Radboud University Nijmegen 57 / 64 Using these diagrams ● Reverse engineering ● ● Fuzzing or model-based testing ● ● Manual inspection of correctness and security Use as basis for automated fuzz testing Formal verification ● Use as basis for model checking Joeri de Ruiter - Digital Security, Radboud University Nijmegen 58 / 64 Automated reverse engineering e.dentifier2 ● Using LearnLib ● Two different versions of the device ● Physical interaction needed ● Programmable smart card ● All PIN codes accepted ● Responses fixed Joeri de Ruiter - Digital Security, Radboud University Nijmegen 59 / 64 Robot ● Built using Lego ● Controlled by Raspberry Pi ● 3 motors: OK, Cancel, digit ● Power USB line Joeri de Ruiter - Digital Security, Radboud University Nijmegen 60 / 64 Robot Joeri de Ruiter - Digital Security, Radboud University Nijmegen 61 / 64 Robot Joeri de Ruiter - Digital Security, Radboud University Nijmegen 62 / 64 Results Joeri de Ruiter - Digital Security, Radboud University Nijmegen 63 / 64 Conclusions ● ● ● EMV specifications too complex ● Too many options ● No explicit security goals ● Design one secure protocol Formal verification is still possible Automated learning is useful when reverse engineering or analysing systems Joeri de Ruiter - Digital Security, Radboud University Nijmegen 64 / 64
© Copyright 2024 ExpyDoc
