nip-ab: Tamarin formal verification (strengthened)#349
Draft
tlongwell-block wants to merge 3 commits intomainfrom
Draft
nip-ab: Tamarin formal verification (strengthened)#349tlongwell-block wants to merge 3 commits intomainfrom
tlongwell-block wants to merge 3 commits intomainfrom
Conversation
* origin/main: nip-ab: clarify transcript_hash role and fix protocol diagram (#346) chore: fix deprecation warnings and decompose AgentsView (#347) chore: improve thread panel inline replies and nesting behavior (#339) feat: NIP-AB device pairing — Phase 2 (desktop + mobile UI) (#343) fix(huddle): prevent phantom huddle from late-arriving relay events (#344) perf(tts): reduce Kokoro time-to-first-audio with session warmup and threading (#342)
Model changes: - Split Target_Receives_Payload into Target_Buffers_Payload (opaque ciphertext, linear TgtCanBuffer gate) + Target_Decrypts_Payload (senc pattern match gated on TgtTransferring). Faithfully captures #346's dual-consent buffering semantics. - New lemmas: injective_target_source_agreement, target_decrypts_payload_only_after_dual_consent, decryption_requires_prior_buffering, executable_payload_buffered_before_approval - Renamed TgtReadyPayload -> TgtTransferring, TargetReceivedPayload -> TargetDecryptedPayload for spec alignment - Added SAS abstraction comment, transcript hash detection-not- prevention note Spec changes: - SAS denial is now MUST-abort (primary MITM defense) - SHOULD->MUST for SAS prompt text and secure storage - Added payload zeroization requirement - Tightened protocol_error to exclude peer-triggered responses (anti-oracle) - Clarified decrypt ambiguity: implementations may NIP-44-decrypt for type routing but MUST NOT extract payload field before dual consent; recommends ciphertext buffering as safest strategy - Defense-in-depth scoped to session establishment, not payload confidentiality - All 16 lemmas named in Formal Verification section with precise descriptions and explicit no-compromise preconditions - Expanded abstractions list to 11 categories All 16 lemmas verified by Tamarin Prover (14.5s).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Builds on #345 (Jordan's Tamarin proof) with post-#346 consistency fixes.
Model: split payload receipt into ciphertext buffering + gated decryption, added injective agreement and buffer-sequencing lemmas. 16/16 verified.
Spec: SAS denial is now MUST-abort, payload zeroization explicit, protocol_error scoped to local faults, all 16 lemmas named with preconditions, abstractions list expanded.
cc @jmecom