Scenario-based specification of security protocols and transformation to security model checkers

Abstract

Security protocols ensure secure communication between and within systems such as internet services, factories, and smartphones. As evidenced by numerous successful attacks against popular protocols such as TLS, designing protocols securely is a tedious and error-prone task. Model checkers greatly aid protocol verification, yet any single model checker is oftentimes insufficient to check a protocol's security in full. Instead, engineers are forced to maintain multiple overlapping and hopefully non-contradicting and non-diverging specifications, one per model-checking tool---an error-prone task. To address this problem, this paper presents VICE, a scenario-based approach to security-protocol verification. It provides a visual modeling language based for specifying security protocols independent of the model checker. It then automatically transforms the relevant fragments of these models into equivalent inputs to multiple model checkers. In result, VICE completely relieves the security engineer from choosing and specifying queries via a fully automatic generation of all necessary queries. Through a case study involving real-world specifications of eight security protocols, we show that VICE is applicable in practice.