mitls-fstar icon indicating copy to clipboard operation
mitls-fstar copied to clipboard

Idealization coverage

Open sishtiaq opened this issue 8 years ago • 5 comments

Make sure that tests go into both of ideal's branches.

sishtiaq avatar Jun 03 '16 10:06 sishtiaq

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. keys that are the same concretely should also be the same ideally.

markulf avatar Jun 06 '16 17:06 markulf

Yes, that's what I meant.

sishtiaq avatar Jun 07 '16 10:06 sishtiaq

Let me know once you get started and whenever you need domain knowledge for this.

markulf avatar Jun 07 '16 10:06 markulf

Related to crypto code review https://github.com/mitls/mitls-fstar/issues/80

markulf avatar Sep 10 '16 06:09 markulf

We made progress on the use of idealization flags and their handling in Kremlin. Can someone summarize? @protz @fournet

Should this issue be assigned to a milestone?

markulf avatar Oct 23 '16 15:10 markulf