Re: [MLS] Formal proof for PR 713 / "Improve parent hash guarantees"

Thanks Théophile for doing that work!

@Richard: I’d like to join please.

Raphael

> On 8. Jun 2022, at 15:21, Richard Barnes <rlb@ipv.sx> wrote:
> 
> I've got a calendar invite going with Webex coords.  Let me know if you'd like to join.
> --RLB
> 
> On Wed, Jun 8, 2022 at 4:14 AM Théophile Wallez <theophile.wallez@inria.fr <mailto:theophile.wallez@inria.fr>> wrote:
> Hello All,
> 
> During the last interim, when discussing PR 713, people raised concerns 
> that this PR might introduce bugs in MLS, because the parent-hash is a 
> complex thing and contained many bugs in the past.
> 
> During the last days, I formalized a small part of MLS in F*, and proved 
> that the invariants checked in the "Verifying Parent Hashes" section are 
> actually invariants of the protocol.
> 
> Of course I can't just say "believe my I have a formal proof". I also 
> can't just send my model as-is and expect everyone to decipher the F* 
> code without explanations.
> Richard therefore proposed to meet during one hour before the next 
> interim, for the people interested, during which I will explain my 
> model, hoping that afterwards:
> - you will agree that my code faithfully models the parts of MLS dealing 
> with parent-hashes,
> - you will agree that the theorem I proved actually state that the new 
> invariants are preserved.
> The only prerequisite will be to be a bit familiar with functional 
> programming (no need to know super fancy stuff, just algebraic datatypes 
> / pattern matching / recursion should be enough).
> 
> Richard will take care of setting up a Webex link.
> 
> Cheers,
> Théophile.
> 
> _______________________________________________
> MLS mailing list
> MLS@ietf.org <mailto:MLS@ietf.org>
> https://www.ietf.org/mailman/listinfo/mls <https://www.ietf.org/mailman/listinfo/mls>
> _______________________________________________
> MLS mailing list
> MLS@ietf.org
> https://www.ietf.org/mailman/listinfo/mls