Model checking indistinguishability of randomized security protocols

Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

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

Abstract

The design of security protocols is extremely subtle and vulnerable to potentially devastating flaws. As a result, many tools and techniques for the automated verification of protocol designs have been developed. Unfortunately, these tools don’t have the ability to model and reason about protocols with randomization, which are becoming increasingly prevalent in systems providing privacy and anonymity guarantees. The security guarantees of these systems are often formulated by means of the indistinguishability of two protocols. In this paper, we give the first practical algorithms for model checking indistinguishability properties of randomized security protocols against the powerful threat model of a bounded Dolev-Yao adversary. Our techniques are implemented in the Stochastic Protocol ANalayzer (Span) and evaluated on several examples. As part of our evaluation, we conduct the first automated analysis of an electronic voting protocol based on the 3-ballot design.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsGeorg Weissenbacher, Hana Chockler
PublisherSpringer
Pages117-135
Number of pages19
ISBN (Print)9783319961415
DOIs
StatePublished - 2018
Event30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: Jul 14 2018Jul 17 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10982 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/TerritoryUnited Kingdom
CityOxford
Period7/14/187/17/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Model checking indistinguishability of randomized security protocols'. Together they form a unique fingerprint.

Cite this