TY - GEN
T1 - Modular verification of protocol equivalence in the presence of randomness
AU - Bauer, Matthew S.
AU - Chadha, Rohit
AU - Viswanathan, Mahesh
N1 - Funding Information:
M.S. Bauer and M. Viswanathan—Partially supported by grant NSF CNS 1314485. R. Chadha—Partially supported by grants NSF CNS 1314338 and NSF CNS 1553548.
Publisher Copyright:
© 2017, Springer International Publishing AG.
PY - 2017
Y1 - 2017
N2 - Security protocols that provide privacy and anonymity guarantees are growing increasingly prevalent in the online world. The highly intricate nature of these protocols makes them vulnerable to subtle design flaws. Formal methods have been successfully deployed to detect these errors, where protocol correctness is formulated as a notion of equivalence (indistinguishably). The high overhead for verifying such equivalence properties, in conjunction with the fact that protocols are never run in isolation, has created a need for modular verification techniques. Existing approaches in formal modeling and (compositional) verification of protocols for privacy have abstracted away a fundamental ingredient in the effectiveness of these protocols, randomness. We present the first composition results for equivalence properties of protocols that are explicitly able to toss coins. Our results hold even when protocols share data (such as long term keys) provided that protocol messages are tagged with the information of which protocol they belong to.
AB - Security protocols that provide privacy and anonymity guarantees are growing increasingly prevalent in the online world. The highly intricate nature of these protocols makes them vulnerable to subtle design flaws. Formal methods have been successfully deployed to detect these errors, where protocol correctness is formulated as a notion of equivalence (indistinguishably). The high overhead for verifying such equivalence properties, in conjunction with the fact that protocols are never run in isolation, has created a need for modular verification techniques. Existing approaches in formal modeling and (compositional) verification of protocols for privacy have abstracted away a fundamental ingredient in the effectiveness of these protocols, randomness. We present the first composition results for equivalence properties of protocols that are explicitly able to toss coins. Our results hold even when protocols share data (such as long term keys) provided that protocol messages are tagged with the information of which protocol they belong to.
UR - http://www.scopus.com/inward/record.url?scp=85029472052&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029472052&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66402-6_12
DO - 10.1007/978-3-319-66402-6_12
M3 - Conference contribution
AN - SCOPUS:85029472052
SN - 9783319664019
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 187
EP - 205
BT - Computer Security – ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Proceedings
A2 - Snekkenes, Einar
A2 - Foley, Simon N.
A2 - Gollmann, Dieter
PB - Springer
T2 - 22nd European Symposium on Research in Computer Security, ESORICS 2017
Y2 - 11 September 2017 through 15 September 2017
ER -