Verification of randomized security protocols

Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781509030187
DOIs
StatePublished - Aug 8 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 - Reykjavik, Iceland
Duration: Jun 20 2017Jun 23 2017

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
CountryIceland
CityReykjavik
Period6/20/176/23/17

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'Verification of randomized security protocols'. Together they form a unique fingerprint.

Cite this