  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.
