The thesis presents verification of biometric authentication protocols. ProVerif is used as the verification tool for verifying and analysing the protocols. The protocol are analysed in ProVerif model. Various attacks to the protocols are generated in order to verify whether the protocols hold their intended properties. We have selected three biometric authentication protocols and proposed a remote biometric authentication protocol for on-line banking. Each of which has different intended purposes and properties. The first protocol is generic authentication using biometric data. This protocol provides three properties of the protocol: effectiveness, correctness, and privacy of biometric data. In addition, the protocol is clarified in order to verify the property of effectiveness. Details in chapter 3 show that without this clarification, the property of effectiveness would not hold. The second protocol is a biometric authentication protocol for a signature creation application. This is a specific purpose protocol that requires successfully biometric authentication in order to proceed the user's request, signing a document. The two properties of the protocol are verified: privacy of biometric data and intensional authentication. This protocol is used for signing a document using a user's private key. Hence, extension of the protocol is required so that the intensional authentication property can be verified. This property demonstrates that the legitimate user signs only the document that he intends to sign. A detailed description of this work can be found in chapter 4. The thesis further considers a remote biometric authentication protocol. Chapter 5 presents the protocol and verification of its desirable properties. This chapter shows analysis of the two properties of the protocol: privacy of biometric data and authenticity. Next, the thesis proposes a remote biometric authentication protocol for on-line banking in chapter 6. The protocol promises three intended properties: privacy of the biometric data, liveness of biometric data and intensional authentication. The protocol is illustrated in detail and desirable properties of the protocol are verified. Finally, chapter 7 concludes this study by briefly comparing properties that each protocol hold. Furthermore, we have identified the limitations of this thesis and possible areas for further research.
展开▼
