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.

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 -