search

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
8 stars 0 forks source link

feat: add support for KDF #11

Closed TWal closed 3 weeks ago

TWal commented 1 month ago

The difficulty of implementing KDFs is that HKDF.Extract is (in several protocols) used to mix two secrets together, as a dual-PRF.

I have been looking on how the KDFs are used in TLS 1.3, Signal and MLS, I think the proof interface here would allow to prove these protocols (so hopefully, any other protocol that has reasonable usage of KDFs!)

qaphla commented 1 month ago

I've looked through and have no major objections. I am reminded that the encoding as int lists is quite bulky --- I might see how much work it is to automate that.

TWal commented 3 weeks ago

I merged main and adapted the printing functions, does it look fine @fabian-hk? If so, I will merge this PR!