A blocking-based approach to protocol validation

One common approach to protocol validation is reachability analysis, which involves systematically exploring the state space of a protocol. The main challenge of reachability analysis is dealing with the state explosion problem. In this paper, we present a new reachability analysis approach, called blocking-based simultaneous reachability analysis, for protocol validation. This approach has the potential to significantly reduce the number of states that have to be explored but can still be used to detect several logical errors that are commonly found in a protocol.