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

Published 20 hours ago • verified publisher icon project-everest

Key schedule

Open sishtiaq opened this issue 8 years ago • 6 comments

PSK and Late HS are still in draft for TLS1.3. For M1, PSK could be implemented without verification.

What is the function and the status of idealization and verification of these files?

  • [ ] PMS.fst
  • [ ] PRF.fst
  • [ ] HKDF.fst module implements HKDF on top of CoreCrypto
  • [ ] PSK defines pmk_id and psk leakage flags
  • [ ] MasterSecret
  • [ ] KeySchedule

sishtiaq avatar Apr 06 '16 14:04 sishtiaq

The current goal is to wrap all of this modules into a mini handshake KeySchedule.fst module.

markulf avatar Apr 06 '16 15:04 markulf

@markulf : do you want to change the title of this (to KeySchedule.fst), or is it ok as is?

sishtiaq avatar Apr 06 '16 16:04 sishtiaq

@ad-l is this issue closed with the implementation of the stateful key schedule?

Presumably we lost some modularity in the verification compared to the previous version of miTLS, do we try to restore it?

markulf avatar Aug 16 '16 16:08 markulf

@ad-l @sishtiaq I updated the issue, to track idealization and verification of the key schedule.

markulf avatar Aug 27 '16 13:08 markulf

@ad-l Can you comment on this? Added you as an assignee as you really did most of the work on integrating these files into the keyschedule.

markulf avatar Sep 10 '16 06:09 markulf

Our focus was on the record. I don't know how ambitious our goals are on this for M1 beyond interoperability?

markulf avatar Oct 23 '16 15:10 markulf