mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
abf62ef0d0
Derive the session key K in the responder's Msg2 rule and carry it in state (Msg4 binds K from state, no inline DH recomputation) — clears the global derivation-check timeout. Same fix in lean/ and formal/ trees; all lemmas and semantics unchanged. Co-authored-by: Hanzo Dev <[email protected]>