Markulf Kohlweiss
Markulf Kohlweiss
Yes, for the complete review. We should carve out a task for those modules that we verify for Milestone 1. Mostly on the Record protocol.
Redundant with, https://github.com/mitls/mitls-fstar/issues/127 Could be seen as a subtask. Should this be assigned to M1, might be a punt but we could re-prioritize if it is important.
What is the status of this?
Maybe reopen a more specific issue with regards to refactoring TLSExtensions later. Extensions are intimately related to negotiation and downgrade.
Should this be an epic, or part of a verified record stack epic?
The following experiment might help find a good verification style: https://github.com/FStarLang/FStar/issues/643 @nikswamy @s-zanella
Related to crypto code review https://github.com/mitls/mitls-fstar/issues/80
you mean into both ideal and concrete/non-ideal branches? I agree, this is important. One could even have tests that ideal and concrete cannot be trivially distinguished via simple strategies. E.g....
Let me know once you get started and whenever you need domain knowledge for this.
Related to crypto code review https://github.com/mitls/mitls-fstar/issues/80