Towards a Formal Verification of a Multi-factor Authentication Protocol Using Automated Theorem Provers

We present a proposal for a new multi-factor authentication scheme through the use of biometrics and smart-cards. Targeted to the Brazilian court system, which is being redesigned, the main goals of this protocol are to provide adequate division between authentication and authorisation services, as well as, the existence of different roles for improved security and management. In addition, we formalised the protocol into a first-order logic model and verified it with an automated theorem prover. Our main contributions are the design of the protocol and the usage of a methodology including design, verification, implementation and deployment of a protocol of nation-wide scale.