Many types of attacks on confidentiality stem from the nondeterministic nature of the
environment that computer programs operate in. We focus on verification of confidentiality in
nondeterministic environments by reasoning about asynchronous hyperproperties. We
generalize the temporal logic A-HLTL to allow nested trajectory quantification, where a
trajectory determines how different execution traces may advance and stutter. We propose a
bounded model checking algorithm for A-HLTL based on QBF-solving for a fragment of A …