{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/102456"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/102456","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Analysis of randomized security protocols","abstract":"Made available in DSpace on 2019-02-06T19:36:23Z (GMT). No. of bitstreams: 2 BAUER-DISSERTATION-2018.pdf: 942833 bytes, checksum: 783bd3a1adfd3dfd54474a5046e90152 (MD5) LICENSE.txt: 4210 bytes, checksum: 9c379298174d05b023e864fcc4653dd4 (MD5) Previous issue date: 2018-11-30","abstract_html":"Made available in DSpace on 2019-02-06T19:36:23Z (GMT). No. of bitstreams: 2 BAUER-DISSERTATION-2018.pdf: 942833 bytes, checksum: 783bd3a1adfd3dfd54474a5046e90152 (MD5) LICENSE.txt: 4210 bytes, checksum: 9c379298174d05b023e864fcc4653dd4 (MD5) Previous issue date: 2018-11-30","abstract_has_math":false,"creators":["Bauer, Matthew Steven"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Viswanathan, Mahesh","Meseguer, José","Bates, Adam","Chadha, Rohit"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-02-06T19:36:23Z","date_published":"2019-02-06T19:36:23Z","updated_at":"2026-07-22T22:24:40Z","subjects":["Symbolic verification","Dolev-Yao attacker","Randomized security protocols"],"languages":["en"],"rights":["Copyright 2018 Matthew Bauer"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/102456","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Viswanathan, Mahesh","Meseguer, José","Bates, Adam","Chadha, Rohit"]},{"key":"dc:creator","label":"Author","values":["Bauer, Matthew Steven"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-02-06T19:36:23Z","2018-11-30","2018-12"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Symbolic verification","Dolev-Yao attacker","Randomized security protocols"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Matthew Bauer"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/102456"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Made available in DSpace on 2019-02-06T19:36:23Z (GMT). No. of bitstreams: 2 BAUER-DISSERTATION-2018.pdf: 942833 bytes, checksum: 783bd3a1adfd3dfd54474a5046e90152 (MD5) LICENSE.txt: 4210 bytes, checksum: 9c379298174d05b023e864fcc4653dd4 (MD5) Previous issue date: 2018-11-30","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Matthew Bauer, accepted the attached license on 2018-11-29 at 20:10.","The student, Matthew Bauer, submitted this Dissertation for approval on 2018-11-29 at 20:18.","This Dissertation was approved for publication on 2018-11-30 at 16:44.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13151 on 2019-02-05 at 11:13:14"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Analysis of randomized security protocols"]}]}],"canonical_facts":{"dc:contributor":["Viswanathan, Mahesh","Meseguer, José","Bates, Adam","Chadha, Rohit"],"dc:creator":["Bauer, Matthew Steven"],"dc:date":["2019-02-06T19:36:23Z","2018-11-30","2018-12"],"dc:description":["Made available in DSpace on 2019-02-06T19:36:23Z (GMT). No. of bitstreams: 2 BAUER-DISSERTATION-2018.pdf: 942833 bytes, checksum: 783bd3a1adfd3dfd54474a5046e90152 (MD5) LICENSE.txt: 4210 bytes, checksum: 9c379298174d05b023e864fcc4653dd4 (MD5) Previous issue date: 2018-11-30","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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2019-02-05 without embargo terms","The student, Matthew Bauer, accepted the attached license on 2018-11-29 at 20:10.","The student, Matthew Bauer, submitted this Dissertation for approval on 2018-11-29 at 20:18.","This Dissertation was approved for publication on 2018-11-30 at 16:44.","DSpace SAF Submission Ingestion Package generated from Vireo submission #13151 on 2019-02-05 at 11:13:14"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/102456"],"dc:language":["en"],"dc:rights":["Copyright 2018 Matthew Bauer"],"dc:subject":["Symbolic verification","Dolev-Yao attacker","Randomized security protocols"],"dc:title":["Analysis of randomized security protocols"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:40Z"}