Verification of Randomized Security Protocols
Title | Verification of Randomized Security Protocols |
Publication Type | Conference Paper |
Year of Publication | 2017 |
Authors | Chadha, R., Sistla, A. P., Viswanathan, M. |
Conference Name | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
ISBN Number | 978-1-5090-3018-7 |
Keywords | Complexity 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 |
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 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. |
URL | https://ieeexplore.ieee.org/document/8005126/ |
DOI | 10.1109/LICS.2017.8005126 |
Citation Key | chadha_verification_2017 |
- Policy
- Upper bound
- standard cryptographic primitives
- sequences
- sequence
- secret sec
- secrecy problem
- randomized security protocol Verification
- pubcrawl
- Protocols
- protocol verification
- probability
- privacy
- policy-based collaboration
- Complexity theory
- nonsatisfiability problem
- monadic first order logic
- matching lower bound
- Indistinguishability
- formal logic
- encryption
- Electronic mail
- Cryptographic Protocols
- coNEXPTIME
- computational complexity
- computability
- Compositionality