Biometry to enhance smart card security (MOC using TOC protocol)Università degli Studi “G. d’Annunzio”
Dipartimento di Scienze - Pescara Giampaolo Bella – Stefano Bistarelli – Fabio Martinelli
Biometry to enhance smart card security (MOC using TOC protocol)
Università degli Studi “G. d’Annunzio”
Dipartimento di Scienze - Pescara Giampaolo Bella – Stefano Bistarelli – Fabio Martinelli
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…
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.
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
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
Template on Card (TOC)
User Smart Card Biometric Template Grant Biometric Template Biometric Input Template on Card
Match on Card (MOC)
Smart Card Biometric Template User CPU Grant Biometric Input Match on Card
System on Card
User Biometric Input Smart Card CPU Biometric Template Grant System on Card
A MOC protocol
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
A MOC using TOC protocol
CM is the criptoki match module
CM signs a hash of the pair of templates only if they match
Verification challenges?
Biometry adds no problems
``Incremental’’ protocols – the two are equivalent from the application viewpoint
Functional
Security
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
The criptoki and the match module may be distinct processes (they share no knowledge)
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
Comments