Analysis of randomized security protocols

Bauer, Matthew Steven

Permalink

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

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

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