Verifying a chipcard-based biometric identification protocol in VSE

Abstract

In this paper we describe our experiences in specifying and verifying a complex cryptographic protocol actually used in industry that has been developed for the area of chipcard based biometric identification systems. The main emphasis was placed on authenticity, integrity and confidentiality properties. The formal analysis even led to several simplifying modifications of the protocol that facilitate the implementation, yet maintaining the protocol security properties we considered. The formal analysis is based on an inductive approach performed with the help of VSE (Verification Support Environment). The heuristic based proof automation techniques realized in VSE result in an average grade of automation of 80 percent. Thus, VSE provides substantial support for the specification and verification of cryptographic protocols. © Springer-Verlag Berlin Heidelberg 2006.