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.

Within a framework for verifying parametric network protocols through induction, one needs to find invariants based on a protocol instance of a small number of nodes. In this paper, we propose a new approach to accelerate parameterized verification by adopting decision trees to represent the state space of a protocol instance. Such trees can be considered as a knowledge base that summarizes all behaviors of the protocol instance. With this knowledge base, we are able to efficiently construct an oracle to effectively assess candidates of invariants of the protocol, which are suggested by an invariant finder. With the discovered invariants, a formal proof for the correctness of the protocol can be derived in the framework after proper generalization. The effectiveness of our method is demonstrated by experiments with typical benchmarks.