Biblio

Analyzing safety and security requirements remains a difficult task in the development of real-life network protocols. Although numerous modeling and analyzing methods have been proposed in the past decades, most of them handle safety and security requirements separately without considering their interplay. In this work, we propose a collaborative modeling framework that enables co-analysis of safety and security requirements for network protocols. Our modeling framework is based on a well-defined type system and supports modeling of network topology, message flows, protocol behaviors and attacker behaviors. It also supports the specification of safety requirements as temporal logical formulae and typical security requirements as queries, and leverages on the existing verification tools for formal safety and security analysis via model transformations. We have implemented this framework in a prototype tool CMSS, and illustrated the capability of CMSS by using the 5G AKA initialization protocol as a case study.