La identificación por radiofrecuencia (RFID) es un componente crucial de Internet de las cosas (IoT), y RFID utilizando criptografía de curva elíptica (ECC) es un enfoque de autenticación de criptosistema de clave pública que aborda el problema de la encriptación de datos de etiquetas electrónicas en sistemas RFID. La comercialización y despliegue a gran escala de sistemas RFID han planteado una serie de problemas relacionados con la seguridad que sugieren la necesidad de protocolos de seguridad. La teoría de la lógica de eventos (LoET) es un método formal para la construcción y razonamiento sobre sistemas distribuidos y protocolos que involucran conceptos de seguridad. Este documento propone tres clases de eventos, Calcular, Recuperar y Generar, y axiomas y reglas de inferencia relacionadas para abstraer formalmente la función de generación de clave de sesión ECC e instituir formalmente el proceso de autenticación de ambas partes, y la LoET extendida se utiliza para analizar las propiedades de seguridad de los protocolos de seguridad de RFID basados en ECC. Bajo suposiciones razonables, se muestra que un esquema de autenticación mutua de RFID basado en ECC satisface la característica de autenticación mutua fuerte. Se muestra que la teoría extendida de la lógica de eventos puede utilizarse para demostrar las propiedades de seguridad de esta clase de protocolos de RFID basados en ECC.