Visible to the public Verification of Randomized Security Protocols

TitleVerification of Randomized Security Protocols
Publication TypeConference Paper
Year of Publication2017
AuthorsChadha, R., Sistla, A. P., Viswanathan, M.
Conference Name2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
ISBN Number978-1-5090-3018-7
KeywordsComplexity theory, compositionality, computability, computational complexity, coNEXPTIME, cryptographic protocols, Electronic mail, Encryption, formal logic, indistinguishability, matching lower bound, monadic first order logic, nonsatisfiability problem, policy, policy-based collaboration, privacy, probability, protocol verification, Protocols, pubcrawl, randomized security protocol Verification, secrecy problem, secret sec, sequence, sequences, standard cryptographic primitives, Upper bound

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$overline$ in P1 is the same as that of observing 0$overline$ 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.

Citation Keychadha_verification_2017