El protocolo European Installation Bus (EIB), también conocido como KNX/EIB, se utiliza ampliamente en la automatización de edificios y hogares. Una extensión del protocolo KNX/EIB, EIBsec, está diseñada principalmente para cumplir con los requisitos de seguridad en la transmisión de datos en sistemas de automatización de edificios distribuidos. Sin embargo, este protocolo presenta algunos problemas de seguridad en los procesos de solicitud, distribución de claves y autenticación de identidad. Este documento emplea un método de análisis formal que combina la teoría de Redes de Petri Coloreadas (CPN) con el modelo de ataque de Dolev-Yao para evaluar y mejorar el protocolo EIBsec. Utiliza las herramientas CPN para realizar un análisis de modelado CPN sobre el protocolo e introduce un modelo de evaluación de seguridad para llevar a cabo la detección de intrusiones y la evaluación de seguridad. A través de este análisis, se identifican vulnerabilidades en el protocolo, como ataques de manipulación y de repetición. Para abordar estas preocupaciones de seguridad, introducimos métodos de verificación de hash y juicio de marcas de tiempo en el protocolo original para mejorar su seguridad. Posteriormente, basándonos en el protocolo mejorado, realizamos modelado CPN y verificamos la seguridad del nuevo esquema. Finalmente, a través de una comparación y análisis del rendimiento y la seguridad entre el protocolo original y el esquema mejorado, se encuentra que el esquema mejorado tiene una mayor seguridad.