Visible to the public Biblio

Filters: Keyword is monadic first order logic  [Clear All Filters]
2018-05-24
Chadha, R., Sistla, A. P., Viswanathan, M..  2017.  Verification of Randomized Security Protocols. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). :1–12.

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 textgreater 1 - p; and indistinguishability, which asks if the probability observing any sequence 0$øverline$ in P1 is the same as that of observing 0$øverline$ 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.