Resumen

La comprobación de modelos se ha aplicado con éxito a la verificación de protocolos de seguridad, pero el proceso de modelado es siempre tedioso y también se necesita un conocimiento competente del método formal, aunque la verificación final podría ser automática en función de herramientas específicas. Al mismo tiempo, debido a la aparición de nuevos tipos de redes, como las redes inalámbricas de sensores (WSN) y las redes inalámbricas de área corporal (WBAN), el modelado formal y la verificación de estos sistemas específicos de dominio son todo un reto. En este artículo, se propone un método específico y novedoso de modelado formal y verificación que se implementa utilizando una herramienta ampliable llamada PAT para realizar la verificación de seguridad específica de las WSN. En primer lugar, se desarrolla una estructura de datos de modelado abstracto para CSP#, que se construye en PAT, para dar soporte a la especificación relacionada con la movilidad de los nodos para modelar la actividad de los nodos basada en la localización. A continuación, se redefine el modelo tradicional Dolev-Yao para facilitar el modelado de los comportamientos de ataque específicos de la localización sobre el mecanismo de seguridad. Se describe en detalle una aplicación de verificación formal de un protocolo de seguridad basado en la localización en WSN para demostrar la utilidad y eficacia de la metodología propuesta. Además, también se puede modelar y verificar con éxito un nuevo protocolo de seguridad de autenticación basado en la localización en WBAN utilizando directamente nuestro método, que es, hasta donde sabemos, el primer esfuerzo en el empleo de la comprobación de modelos para el análisis automático del protocolo de autenticación para WBAN.

• Materias:Biotecnología Nanotecnología Redes de sensores Sistema de sensores Tecnología de sensores
• Subjects:Biotechnology Nanotechnology Sensor networks Sensor system Sensor technology
• Palabras claves:wban, wsn, localización, estructura de datos de modelado abstracto, redes inalámbricas de área corporal, protocolo de seguridad de autenticación, aplicación de verificación formal, modelado formal novedoso, comportamientos de ataque específicos, verificación de seguridad específica
• Keywords:wban, wsn, location, abstract modeling data structure, wireless body area networks, authentication security protocol, formal verification application, novel formal modeling, specific attack behaviors, specific security verification