Files in this item



application/pdftechreport.pdf (457kB)
(no description provided)PDF


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
Date Available in IDEALS:2017-04-18

This item appears in the following Collection(s)

Item Statistics