A Study on Computational Formal Verification for Practical Cryptographic Protocol: The Case of Synchronous RFID Authentication

Abstract

Formal verification of cryptographic protocols has a long his- tory with a great number of successful verification tools created. Recent progress in formal verification theory has brought more powerful tools capable of handling computational assumption, which leads to more re- liable verification results for information systems. In this paper, we introduce an effective scheme and studies on apply- ing computational formal verification toward a practical cryptographic protocol. As a target protocol, we reconsider a security model for RFID authentication with a man-in-the-middle adversary and communication fault. We define three model and security proofs via a game-based approach that, in a computational sense, makes our security models compatible with formal security analysis tools. Then we show the combination of using a computational formal verification tool and handwritten verification to overcome the computational tool’s limitations. We show that the target RFID authentication protocol is robust against the above- mentioned attacks, and then provide game-based (handwritten) proofs and their verification via CryptoVerif.