University of Illinois Urbana-Champaign

Analysis of randomized security protocols

Bauer, Matthew Steven

Content Files
BAUER-DISSERTATION-2018.pdf

Permalink

https://hdl.handle.net/2142/102456

Description

Title
Analysis of randomized security protocols
Author(s)
Bauer, Matthew Steven
Issue Date
2018-11-30
Director of Research (if dissertation) or Advisor (if thesis)
Viswanathan, Mahesh
Doctoral Committee Chair(s)
Viswanathan, Mahesh
Committee Member(s)
  • Meseguer, José
  • Bates, Adam
  • Chadha, Rohit
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Date of Ingest
2019-02-06T19:36:23Z
Keyword(s)
  • Symbolic verification
  • Dolev-Yao attacker
  • Randomized security protocols
Abstract
Formal analysis has a long and successful track record in the automated verification of security protocols. Techniques in this domain have converged around modeling protocols as non-deterministic processes that interact asynchronously through an adversarial environment controlled by a Dolev-Yao attacker. There are, however, a large class of protocols whose correctness relies on an explicit ability to model and reason about randomness. Lying at the heart of many widely adopted systems for anonymous communication, these protocols have so-far eluded automated verification techniques. The present work overcomes this long standing obstacle, providing the first framework analyzing randomized security protocols against Dolev-Yao attackers. In this formalism, we present algorithms for model checking safety and indistinguishability properties of randomized security protocols. Our techniques are implemented in the Stochastic Protocol ANalyzer (SPAN) and evaluated on a new suite of benchmarks. Our benchmark examples include a brand new class of protocols that have never been subject of formal (symbolic) verification, including: mix-networks, dinning cryptographers networks, and several electronic voting protocols. During our analysis, we uncover previously unknown vulnerabilities in two popular electronic voting protocols from the literature. The high overhead associated with verifying security protocols, in conjunction with the fact that protocols are rarely run in isolation, has created a demand for modular verification techniques. In our protocol analysis framework, we give a series of composition results for safety and indistinguishability properties of randomized security protocols. Finally, we study the model checking problem for the probabilistic objects that lie at the heart of our protocol semantics. In particular, we present a novel technique that allows for the precise verification of probabilistic computation tree logic (PCTL) properties of discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) at scale. Although our motivation comes from protocol analysis, the techniques further verification capabilities in many application areas.
Graduation Semester
2018-12
Type of Resource
text
Permalink
http://hdl.handle.net/2142/102456
Copyright and License Information
Copyright 2018 Matthew Bauer

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois
Dissertations and Theses - Computer Science
Dissertations and Theses from the Siebel School of Computer Science