[Busec] This Thursday 10:30-12 @ Hariri: Alley Stoughton on Mechanizing Proofs of Security of Cryptographic Protocols
varia at bu.edu
Wed Mar 15 21:26:21 EDT 2017
Reminder: this talk is happening tomorrow (Thursday) morning at 10:30am in
the Hariri seminar room.
On Sun, Mar 12, 2017 at 17:57 Ran Canetti <canetti at bu.edu> wrote:
> 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.
> Busec mailing list
> Busec at cs.bu.edu
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Busec