TY - CHAP
T1 - Modelchecking Safety Properties in Randomized Security Protocols
AU - Bauer, Matthew S.
AU - Chadha, Rohit
AU - Viswanathan, Mahesh
N1 - Funding Information:
Rohit Chadha was partially supported by grants NSF 1553548 CNS and NSF CCF 1900924. Mahesh Viswanathan was partially supported by NSF CCF 1901069.
Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through 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. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed.
AB - Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through 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. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed.
UR - http://www.scopus.com/inward/record.url?scp=85094945218&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85094945218&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-62077-6_12
DO - 10.1007/978-3-030-62077-6_12
M3 - Chapter
AN - SCOPUS:85094945218
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 183
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PB - Springer
ER -