## Files in this item

FilesDescriptionFormat

application/pdf

techreport.pdf (457kB)
(no description provided)PDF

## Description

 Title: Verification of Randomized Security Protocols Author(s): Chadha, Rohit; Sistla, A. Parsad; Viswanathan, Mahesh Subject(s): Verification, Security, randomized protocols, computational complexity 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 --- \emph{secrecy}, which asks if no adversary interacting with a protocol $P$ can determine a secret $\secret$ with probability $> 1-p$; and \emph{indistinguishability}, which asks if the probability observing any sequence $\obseq$ in $P_1$ is the same as that of observing $\obseq$ in $P_2$, 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 $\conexp$. We also prove a matching lower bound for the secrecy problem by reducing the non-satisfiability problem of monadic first order logic without equality. Issue Date: 2017-04-18 Citation Info: IEEE Symposium on Logic in Computer Science, 2017 Genre: Technical Report Type: Text Language: English URI: http://hdl.handle.net/2142/95900 Date Available in IDEALS: 2017-04-18
﻿