Speed Me up if You Can: Conditional Lower Bounds on Opacity Verification

TL;DR

This paper establishes conditional lower bounds on the complexity of verifying opacity in security systems, showing that under certain hypotheses, no significantly faster algorithms than existing ones are likely to exist.

Contribution

It provides the first conditional lower bounds for opacity verification, linking its complexity to the Exponential Time Hypothesis and related automata problems.

Findings

No sub-exponential algorithms for opacity verification under ETH

Conditional lower bounds for automata universality problems

Existing exponential algorithms are essentially optimal

Abstract

Opacity is a property of privacy and security applications asking whether, given a system model, a passive intruder that makes online observations of system's behaviour can ascertain some "secret" information of the system. Deciding opacity is a PSpace-complete problem, and hence there are no polynomial-time algorithms to verify opacity under the assumption that PSpace differs from PTime. This assumption, however, gives rise to a question whether the existing exponential-time algorithms are the best possible or whether there are faster, sub-exponential-time algorithms. We show that under the (Strong) Exponential Time Hypothesis, there are no algorithms that would be significantly faster than the existing algorithms. As a by-product, we obtained a new conditional lower bound on the time complexity of deciding universality (and therefore also inclusion and equivalence) for nondeterministic finite automata.