[Busec] This Thursday 10:30-12 @ Hariri: Alley Stoughton on Mechanizing Proofs of Security of Cryptographic Protocols

Ran Canetti canetti at bu.edu
Sun Mar 12 17:56:58 EDT 2017

BUSec talk this Thursday, March 16, 10:30-12pm, Hariri Seminar room (MCS 

(Lunch to be served after the talk)

Mechanizing the Proof of Adaptive, Information-theoretic Security of 
Cryptographic Protocols in the Random Oracle Model

Alley Stoughton, BU

We report on our research on proving the security of multi-party 
cryptographic protocols using the EasyCrypt proof assistant. We work in 
the computational model using the sequence of games approach, and define 
honest-but-curious (semi-honest) security using a variation of the 
real/ideal paradigm in which, for each protocol party, an adversary 
chooses protocol inputs in an attempt to distinguish the party's real 
and ideal games. Our proofs are information-theoretic, instead of being 
based on computational assumptions. We employ oracles (e.g., random 
oracles for hashing) whose encapsulated states depend on 
dynamically-made, random choices. By limiting an adversary's oracle use, 
one may obtain concrete upper bounds on the distances between a party's 
real and ideal games. Furthermore, our proofs work for adaptive 
adversaries, ones that, when choosing the value of a protocol input, may 
condition this choice on their current protocol view and oracle 
knowledge. We provide an analysis in EasyCrypt of a three party private 
count retrieval protocol. Our proof reduces the security of the protocol 
to the unpredictability of the random oracle on unqueried inputs. We 
emphasize the lessons learned from completing this proof.

Joint work with Mayank Varia.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs-mailman.bu.edu/pipermail/busec/attachments/20170312/1e75de4a/attachment.html>

More information about the Busec mailing list