TY - GEN
T1 - Verification of randomized security protocols
AU - Chadha, Rohit
AU - Sistla, A. Prasad
AU - Viswanathan, Mahesh
N1 - Funding Information:
Acknowledgements. We thanks the anonymous reviewers for their useful comments and suggestions. Rohit Chadha was partially supported by NSF CNS 1314338 and NSF CNS 1553548. A. Prasad Sistla was partially supported by NSF CCF 1319754, NSF CCF 1564296 and NSF CNS 1314485. Mahesh Viswanathan was partially supported by NSF CNS 1314485.
Publisher Copyright:
© 2017 IEEE.
PY - 2017/8/8
Y1 - 2017/8/8
N2 - 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 P1 is 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.
AB - 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 P1 is 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.
UR - http://www.scopus.com/inward/record.url?scp=85029486645&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029486645&partnerID=8YFLogxK
U2 - 10.1109/LICS.2017.8005126
DO - 10.1109/LICS.2017.8005126
M3 - Conference contribution
AN - SCOPUS:85029486645
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
Y2 - 20 June 2017 through 23 June 2017
ER -