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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
techreport.pdf
