Formal Verification of a Key Establishment Protocol for EPC Gen2 RFID Systems: Work in Progress
The EPC Class-1 Generation-2 (Gen2 for short) is a standard Radio Frequency IDentification (RFID) technology that has gained a prominent place on the retail industry. The Gen2 standard lacks, however, of verifiable security functionalities. Eavesdropping attacks can, for instance, affect the security of monitoring applications based on the Gen2 technology. The authors are working on a key establishment protocol that aims at addressing this problem. The protocol is applied at both the initial identification phase and those remainder operations that may require security, such as password protected operations. They specify the protocol using the High Level Protocol Specification Language (HLPSL).