Applying runtime verification to group key establishment

Abstract

Securing communication networks relies fundamentally on the availability of secure cryptographic primitives, which enable authentication, confidentiality, and integrity. A typical starting point to establish secure communication channels is the execution of a protocol that authenticates all involved users/devices and establishes a common secret key among them. This task is referred to as authenticated group key establishment (AGKE). It is standard cryptographic practice to establish provable security guarantees in a suitable theoretical model, abstracting from implementation details. Modeling parties as Turing machines and adversarial capabilities through abstract oracles is a common technique that facilitates a theoretical analysis, but the implementation of a “theoretically secure” protocol may well be susceptible to runtime attacks. A number of authors have explored the use of runtime verification as a means of hardening a security-critical protocol implementation [2, 10, 7, 8]. The aim of this presentation is to give a brief overview of these works.