mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
b774664d17
- QuasarConsensus: bound `msg` by taking In(<msg,cert>) in Verify_Triple (was unbound/underivable). - MPCBridge: bound the relayer message fields via In(<action,chainId,token, amount,nonce>) in Relayer_Combine (were unbound). - RNSHybridHandshake: derive the session key K once in the responder's Msg2 rule and carry it in state, so Msg4 binds K directly instead of recomputing the DH product inline (cleared the global derivation-check timeout). All 11 lemmas and key-agreement semantics unchanged. All Tamarin wellformedness checks pass. Co-authored-by: Hanzo Dev <[email protected]>