Show simple item record

dc.contributor.authorCanetti, Ranen_US
dc.contributor.authorStoughton, Alleyen_US
dc.contributor.authorVaria, Mayanken_US
dc.date.accessioned2020-05-05T19:11:12Z
dc.date.available2020-05-05T19:11:12Z
dc.date.issued2019-06
dc.identifier.citationRan Canetti, Alley Stoughton, Mayank Varia. 2019. "EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security." 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). 2019-06-25 - 2019-06-28. https://doi.org/10.1109/csf.2019.00019
dc.identifier.urihttps://hdl.handle.net/2144/40575
dc.description.abstractWe present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way: Specifying a protocol and the desired ideal functionality; Constructing a simulator and demonstrating its validity, via reduction to hard computational problems; Invoking the universal composition operation and demonstrating that it indeed preserves security. We demonstrate our methodology on a simple example: stating and proving the security of secure message communication via a one-time pad, where the key comes from a Diffie-Hellman key-exchange, assuming ideally authenticated communication. We first put together EasyCrypt-verified proofs that: (a) the Diffie-Hellman protocol UC-realizes an ideal key-exchange functionality, assuming hardness of the Decisional Diffie-Hellman problem, and (b) one-time-pad encryption, with a key obtained using ideal key-exchange, UC-realizes an ideal secure-communication functionality. We then mechanically combine the two proofs into an EasyCrypt-verified proof that the composed protocol realizes the same ideal secure-communication functionality. Although formulating a methodology that is both sound and workable has proven to be a complex task, we are hopeful that it will prove to be the basis for mechanized UC security analyses for significantly more complex protocols and tasks.en_US
dc.language.isoen_US
dc.publisherIEEEen_US
dc.relation.ispartof2019 IEEE 32nd Computer Security Foundations Symposium (CSF)
dc.subjectFormal verificationen_US
dc.subjectComputer aided cryptographyen_US
dc.subjectUniversal composabilityen_US
dc.subjectEasyCrypten_US
dc.subjectCryptographyen_US
dc.subjectGamesen_US
dc.subjectCryptographic protocolsen_US
dc.subjectTask analysisen_US
dc.subjectComplexity theoryen_US
dc.titleEasyUC: using EasyCrypt to mechanize proofs of universally composable securityen_US
dc.typeConference materialsen_US
dc.description.versionAccepted manuscripten_US
dc.identifier.doi10.1109/csf.2019.00019
pubs.elements-sourcecrossrefen_US
pubs.notesEmbargo: No embargoen_US
pubs.organisational-groupBoston Universityen_US
pubs.organisational-groupBoston University, College of Arts & Sciencesen_US
pubs.organisational-groupBoston University, College of Arts & Sciences, Department of Computer Scienceen_US
pubs.publication-statusPublisheden_US
dc.identifier.mycv502237


This item appears in the following Collection(s)

Show simple item record