Biometry to enhance smart card security (MOC using TOC protocol) Giampaolo Bella – Stefano Bistarelli – Fabio Martinelli Università degli Studi “G. d’Annunzio” Dipartimento di Scienze - Pescara C - Pisa Consiglio Nazionale delle Ricerche Overview • Biometry and smart cards – TOC, MOC, SOC • Procotols between application/hardware – A MOC protocol – A MOC via TOC protocol • Towards a formal specification/analysis • Discussion… C - Pisa Consiglio Nazionale delle Ricerche Biometry • Acquisition of bio-features that almost uniquely identify entities • From bio to digital world – Fingerprint: • image acquisition from a scanner • template acquisition from the imagine – The template stores the useful information obtained from the image • match algorithms receive as inputs two templates and returns true iff the two templates are compatible – Bio-information is usually public in the sense that it can be ``easily’’ acquired. C - Pisa Consiglio Nazionale delle Ricerche Smart cards • Smart devices with computational and storage resources • Criptoki (PKCS#11) is the interface smart-cards/applications • Access to smart card functions through a PIN – We consider protocols that use also biometric authentication C - Pisa Consiglio Nazionale delle Ricerche Biometry and smart cards • Applying biometric authentication to log on the smart card: – Template On Card (TOC): Only the template is stored on board • Requires very cheap cards – Match On Card (MOC): The template is on the smart card, the match is performed on board, the live template acquisition is external • Requires smart-cards with ``strong’’ computational power – System On Card (SOC): Each phase is internally performed • Requires currently expensive technology C - Pisa Consiglio Nazionale delle Ricerche Template on Card (TOC) • Template on Card Smart Card Biometric Template Biometric Template Biometric Input User Grant C - Pisa Consiglio Nazionale delle Ricerche Match on Card (MOC) • Match on Card Smart Card Biometric Template Biometric Input CPU User Grant C - Pisa Consiglio Nazionale delle Ricerche System on Card • System on Card Smart Card Biometric Input Biometric Template User Grant CPU C - Pisa Consiglio Nazionale delle Ricerche A MOC protocol • • • • C - Pisa Goal: MOC + key establishment Correctness doesn’t depend on biometry but on cryptography The live template is a fresh scanner acquisition The live template is kept secret for privacy reasons Consiglio Nazionale delle Ricerche A MOC using TOC protocol • CM is the criptoki match module • CM signs a hash of the pair of templates only if they match C - Pisa Consiglio Nazionale delle Ricerche Verification challenges? • Biometry adds no problems • ``Incremental’’ protocols – the two are equivalent from the application viewpoint – Functional – Security C - Pisa Consiglio Nazionale delle Ricerche Formal specification • Process algebra for functional and security aspects – Basic sending/receiving operations • Basic operators as sequencing (.); parallel composiiton (|) • We have 4 different players – Two specifications for the smart cards • SMOC and SMT – The criptoki C and the match module M • MOC protocol: SMOC | C • MOC using TOC : SMT | M | C C - Pisa – The criptoki and the match module may be distinct processes (they share no knowledge) Consiglio Nazionale delle Ricerche Towards formal security analysis • MOC is ``secure’’ – Correspondence analysis: • Control actions to express user’ beliefs – Smart cards issues Start(S,C,Tstored) – Criptoki issues End(C,S,Tlive) – For every enemy X, • SMOC | C | X when restricted to control actions is trace equivalent to Start(S,C,Tstored).End(C,S,Tlive) and Tstored and Tlive match • MOC using TOC is ``as secure as’’ MOC – For every enemy X, • SMT |C | M | X =control actions SMOC | C | X C - Pisa Consiglio Nazionale delle Ricerche Questions? C - Pisa Consiglio Nazionale delle Ricerche