TY - GEN
T1 - Formal verification of a key establishment protocol for EPC Gen2 RFID systems
T2 - 4th Canada-France MITACS Workshop on Foundations and Practice of Security, FPS 2011
AU - Tounsi, Wiem
AU - Cuppens-Boulahia, Nora
AU - Cuppens, Frédéric
AU - Garcia-Alfaro, Joaquin
PY - 2012/1/27
Y1 - 2012/1/27
N2 - 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. We 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. We specify the protocol using the High Level Protocol Specification Language (HLPSL). Then, we verify the secrecy property of the protocol using the AVISPA model checker tool. The results that we report show that the current version of the protocol guarantees sensitive data secrecy under the presence of a passive adversary.
AB - 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. We 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. We specify the protocol using the High Level Protocol Specification Language (HLPSL). Then, we verify the secrecy property of the protocol using the AVISPA model checker tool. The results that we report show that the current version of the protocol guarantees sensitive data secrecy under the presence of a passive adversary.
U2 - 10.1007/978-3-642-27901-0_20
DO - 10.1007/978-3-642-27901-0_20
M3 - Conference contribution
AN - SCOPUS:84856113752
SN - 9783642279003
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 242
EP - 251
BT - Foundations and Practice of Security - 4th Canada-France MITACS Workshop, FPS 2011, Revised Selected Papers
Y2 - 12 May 2011 through 13 May 2011
ER -