Write a Blog >>
Fri 16 - Fri 23 October 2020
Fri 23 Oct 2020 15:20 - 15:40 at Room A - A7-Safety, Security and Testing Chair(s): Joanne M. Atlee

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 Oct
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

15:00 - 16:15: Technical Track - A7-Safety, Security and Testing at Room A
Chair(s): Joanne M. AtleeUniversity of Waterloo
models-2020-technical-track15:00 - 15:20
Katja TumaChalmers | University of Gothenburg, Laurens Sionimec-DistriNet, KU Leuven, Riccardo Scandariato, Koen Yskoutimec - DistriNet, KU Leuven
models-2020-technical-track15:20 - 15:40
models-2020-technical-track15:40 - 16:00
models-2020-technical-track16:00 - 16:10
Alessio Di Sandro, Gehan Selim, Sahar KokalyGeneral Motors, Torin Viger, Rick SalayUniversity of Toronto
Hide past events