一句话：证明随机化安全协议的保密性与不可区分性可在 coNEXPTIME 内判定，并给出保密性匹配下界。
论文研究有限会话下随机化安全协议在 Dolev-Yao 敌手模型中的安全性验证。协议除标准密码原语外还可抛硬币产生随机性。作者考察两个性质：保密性，即敌手确定秘密的概率是否至多 1-p；以及不可区分性，即同一敌手下两个协议产生同一观测序列的概率是否相同。非随机协议的这两个问题已知为 coNP 完全。本文证明随机化协议的保密性与不可区分性均可在 coNEXPTIME 内判定，并通过将无等号一元一阶逻辑的不可满足性归约到保密性问题，给出保密性问题的匹配下界。
We consider the problem of verifying the security of finitely many sessions of a protocol that tosses coins in addition to standard cryptographic primitives against a Dolev-Yao adversary. Two properties are investigated here - secrecy, which asks if no adversary interacting with a protocol P can determine a secret sec with probability > 1 - p; and indistinguishability, which asks if the probability observing any sequence 0̅ in P1is the same as that of observing 0̅ in P2, under the same adversary. Both secrecy and indistinguishability are known to be coNP-complete for non-randomized protocols. In contrast, we show that, for randomized protocols, secrecy and indistinguishability are both decidable in coNEXPTIME. We also prove a matching lower bound for the secrecy problem by reducing the non-satisfiability problem of monadic first order logic without equality.