Scenario-based Specification of Security Protocols and Transformation to Security Model CheckersFT
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.
Fri 23 OctDisplayed time zone: Eastern Time (US & Canada) change
15:00 - 16:15 | A7-Safety, Security and TestingTechnical Track at Room A Chair(s): Joanne M. Atlee University of Waterloo | ||
15:00 20mFull-paper | Automating the Early Detection of Security Design FlawsFT Technical Track Katja Tuma Chalmers | University of Gothenburg, Laurens Sion imec-DistriNet, KU Leuven, Riccardo Scandariato , Koen Yskout imec - DistriNet, KU Leuven Pre-print | ||
15:20 20mFull-paper | Scenario-based Specification of Security Protocols and Transformation to Security Model CheckersFT Technical Track | ||
15:40 20mFull-paper | Automating Test Schedule Generation with Domain-Specific Languages: A Configurable, Model-Driven ApproachP&I Technical Track | ||
16:00 10mDemonstration | MMINT-A 2.0: Tool Support for Lifecycle of Model-Driven Safety ArtifactsDemo Technical Track Alessio Di Sandro , Gehan Selim , Sahar Kokaly General Motors, Torin Viger , Rick Salay University of Toronto |