diff --git a/crates/sprout-core/src/pairing/NIP-AB.md b/crates/sprout-core/src/pairing/NIP-AB.md index d901030bf..1f92a9f58 100644 --- a/crates/sprout-core/src/pairing/NIP-AB.md +++ b/crates/sprout-core/src/pairing/NIP-AB.md @@ -274,7 +274,7 @@ Where `be_u32(bytes)` interprets the first 4 bytes of `sas_input` as a big-endia Both devices display the `sas_code` as a zero-padded 6-digit decimal string (e.g., `"047291"`). The user MUST visually confirm the codes match on both screens before proceeding. -**UX requirement**: The confirmation prompt MUST clearly state what is being authorized. Example: *"You are about to transfer your Nostr identity to another device. Does your other device show: **047291**?"* with prominent Confirm and Deny buttons. +**UX requirement**: The confirmation prompt MUST clearly state what is being authorized. Example: *"You are about to transfer your Nostr identity to another device. Does your other device show: **047291**?"* with prominent Confirm and Deny buttons. If the user denies the SAS on either device, that device MUST immediately send `abort` with reason `"user_denied"`, discard all session state, and terminate the session. SAS denial is the primary MITM defense — implementations MUST NOT allow the protocol to continue after a denial. After the user confirms on the _source_ device, _source_ publishes a `sas-confirm` event: @@ -315,7 +315,7 @@ transcript_hash = HKDF-SHA256( _target_ MUST compute the same `transcript_hash` and verify it matches before proceeding. Implementations MUST use constant-time comparison when checking `transcript_hash` to prevent timing side-channels. A mismatch indicates session inconsistency or parameter tampering; _target_ MUST send `abort` with reason `"sas_mismatch"`, discard any payload received in this session, and terminate. Note: because _source_ sends the payload immediately after `sas-confirm` (without waiting for an acknowledgment), the payload may already be in transit or delivered when the mismatch is detected. The transcript hash is a **detection** mechanism, not a prevention gate — MITM prevention relies on the user's visual SAS comparison on the _source_ device *before* the source confirms and sends the payload. -After verifying the transcript hash, _target_ enters the `AwaitingConfirmation` state. _target_ transitions to `Transferring` when the user confirms the SAS on the target device. _target_ MUST NOT decrypt, import, or act on any received `payload` until **both** the transcript hash has been verified **and** the user has confirmed the SAS on the target device. +After verifying the transcript hash, _target_ enters the `AwaitingConfirmation` state. _target_ transitions to `Transferring` when the user confirms the SAS on the target device. _target_ MUST NOT import, process, or act on the secret material within any received `payload` event until **both** the transcript hash has been verified **and** the user has confirmed the SAS on the target device. (Implementations may NIP-44-decrypt the event content to validate the message `type` for state-machine routing. However, implementations MUST NOT deserialize, extract, log, persist, or act on the `payload` field within a `payload`-type message until both conditions are met. If early decryption is used, the decrypted content MUST be treated as opaque for all purposes other than `type` classification, and MUST be zeroized if the session is aborted before dual consent. The safest implementation strategy — and the one closest to the formal proof — is to buffer the raw NIP-44 ciphertext and defer all decryption until after dual consent.) ### Step 4: Payload Transfer @@ -386,7 +386,7 @@ _target_ decrypts the payload, imports the secret into secure storage, and SHOUL _source_ MUST process at most one `complete` event per session. Subsequent `complete` events MUST be silently discarded. -Both devices MUST close their subscriptions and discard their ephemeral keypairs after either (a) receiving `complete`, (b) the per-step timeout expires, or (c) the session timeout (120 seconds) expires. Implementations MUST zero the ephemeral private keys and session secret from memory before freeing. +Both devices MUST close their subscriptions and discard their ephemeral keypairs after either (a) receiving `complete`, (b) the per-step timeout expires, or (c) the session timeout (120 seconds) expires. Implementations MUST zero the ephemeral private keys, session secret, and any decrypted payload plaintext from memory before freeing. On the _target_ side, the decrypted payload MUST be zeroed from working memory once it has been committed to platform-secure storage. ### Implementation Pseudocode @@ -473,7 +473,7 @@ Defined reason strings: | `"sas_mismatch"` | SAS codes did not match, or transcript hash verification failed | | `"user_denied"` | User explicitly denied the pairing | | `"timeout"` | Session timed out | -| `"protocol_error"` | Unexpected message or validation failure | +| `"protocol_error"` | Local fatal condition (e.g., internal state corruption, unrecoverable implementation error). MUST NOT be sent in response to a peer's out-of-order or validation-failing event — those MUST be silently discarded per §Event Validation. | Upon receiving an `abort`, the other device MUST terminate the session, discard ephemeral keys, and inform the user. Implementations MAY define additional reason strings; unknown reasons SHOULD be treated as `"protocol_error"`. @@ -526,7 +526,7 @@ An attacker who intercepts the QR code (e.g., by photographing the screen or cre This is the same defense used by Matrix (emoji verification), Bluetooth Secure Simple Pairing, and ZRTP. Signal's device linking omitted SAS verification and was subsequently exploited by state-level attackers who created fake QR codes to silently link unauthorized devices. -Clients MUST display an unambiguous confirmation prompt. The prompt SHOULD explicitly state what is being authorized and display the SAS code prominently with a clear option to deny. +Clients MUST display an unambiguous confirmation prompt. The prompt MUST explicitly state what is being authorized and display the SAS code prominently with a clear option to deny. ### Relay Compromise @@ -558,7 +558,7 @@ Implementations MUST enforce a session timeout (recommended: 120 seconds from QR ### Key Material on Two Devices -After an `nsec` transfer, the private key exists on both devices. This is an inherent tradeoff of key transfer versus remote signing ([NIP-46](46.md)). Clients SHOULD store imported keys in platform-secure storage (iOS Keychain, Android Keystore, OS-level credential managers). +After an `nsec` transfer, the private key exists on both devices. This is an inherent tradeoff of key transfer versus remote signing ([NIP-46](46.md)). Clients MUST store imported keys in platform-secure storage (iOS Keychain, Android Keystore, OS-level credential managers). ### Replay Protection @@ -594,7 +594,7 @@ If a relay rejects an event with an `invalid: event creation date` error (NIP-01 ### Why `session_secret` in the QR code instead of deriving it from the ephemeral keypair? -The `session_secret` is independent of the ephemeral keypair. This means that even if an attacker somehow learns the ephemeral private key (e.g., via a side-channel), they cannot compute the `session_id` or `sas_input` without also knowing `session_secret`. The QR code is a separate out-of-band channel; requiring knowledge of both the QR code AND the ECDH handshake provides defense-in-depth. +The `session_secret` is independent of the ephemeral keypair. This means that even if an attacker somehow learns the ephemeral private key (e.g., via a side-channel), they cannot compute the `session_id` or `sas_input` without also knowing `session_secret`. The QR code is a separate out-of-band channel; requiring knowledge of both the QR code AND the ECDH handshake provides defense-in-depth for session establishment (offer authentication and SAS derivation). Note: the payload encryption key is derived purely from ECDH and does not depend on `session_secret`, so this defense-in-depth applies to the pairing handshake, not to payload confidentiality directly. ### Why transcript binding (`transcript_hash`)? @@ -608,6 +608,73 @@ NIP-44 is the Nostr standard for authenticated encryption. Using it here means N An independent security audit of this protocol is planned. Until an audit is completed, implementations in high-security contexts should treat this NIP as `draft` and conduct their own review. +## Formal Verification + +A Tamarin model of the protocol lives at [NIP-AB.spthy](NIP-AB.spthy). The model focuses on the security-critical core of the protocol: + +- QR distribution of `session_secret` and `source_ephemeral_pubkey` +- `offer` authentication via possession of the QR secret +- SAS comparison as an explicit user-mediated gate +- `sas-confirm` transcript binding +- encrypted `payload` delivery +- advisory `complete` acknowledgment + +The model treats the relay and network as a full **Dolev-Yao attacker**: the adversary can intercept, reorder, replay, drop, and fabricate messages. It also includes explicit compromise rules for: + +- QR-code exposure (`session_secret` leaks out-of-band) +- source-session compromise +- target-session compromise + +Under those assumptions, the proved lemmas are: + +**Core security invariants:** + +- **`executable_core_flow`** *(executability)*: the happy-path protocol completes — both sides reach `complete` with the same session and payload. +- **`payload_requires_successful_sas_match`** *(SAS gate)*: an honest source can only send `payload` after a successful SAS match. +- **`payload_secrecy_without_endpoint_compromise`** *(payload secrecy)*: the payload remains unknown to the attacker unless one endpoint session is compromised. QR-code exposure alone does not break secrecy, because the SAS gate pins delivery to an honest target-role execution in the model. (This assumes correct SAS verification — the model treats SAS comparison as perfect; the ~20-bit collision bound is a separate computational argument, see §Design Rationale.) +- **`target_completion_agrees_on_source_payload`** *(target agreement)*: under no-compromise assumptions, if the target completes, then the source previously sent that exact payload in the same session. +- **`source_completion_implies_prior_target_completion_without_compromise`** *(source completion soundness)*: under the same no-compromise assumptions, if the source accepts `complete`, the target previously sent `complete` for the same session. (The model abstracts away `success:true/false` semantics — this proves the `complete` event is authentic, not that import succeeded.) + +- **`injective_target_source_agreement`** *(injective agreement, target → source)*: each target completion corresponds to a unique prior source payload send with the same `(sid, pkS, pkT, payload)`, and that send is itself unique. This is a one-directional injective mapping; the reverse (every send leads to a completion) is a liveness property not provable under Dolev-Yao scheduling. + +**MITM resistance:** + +- **`sas_match_implies_genuine_target`**: every SAS match is bound to a `pkT` that an honest target-role instance in the model actually generated (i.e., from `Target_Scan_QR_And_Send_Offer` with a fresh ephemeral). A network adversary that substitutes the offer's ephemeral key with an attacker-chosen value cannot cause the SAS-match rule to fire. This proves resistance to network key-substitution, not physical-device authenticity — the latter relies on the user's physical verification of the SAS code and is outside the symbolic model's scope. +- **`payload_delivery_requires_genuine_target`** *(composition)*: no payload is ever sent under a `pkT` that lacks a prior honest target-role execution. Follows from the SAS gate combined with the genuine-target lemma. + +**Dual consent and payload buffering:** + +- **`target_decrypts_payload_only_after_dual_consent`**: the target never decrypts the payload without **both** transcript verification **and** an explicit user-approval step. The model proves a stronger abstraction than the spec requires: payload plaintext is not made available to protocol logic before both conditions are met. (The spec permits implementations to NIP-44-decrypt the event content early for message-type classification, but the model conservatively defers all decryption — this is strictly stronger. Early type-field decryption on the target is a local operation that does not emit network-observable messages or alter protocol flow; since the Dolev-Yao attacker already possesses the ciphertext, local decryption reveals nothing new to the adversary, and all proved properties (secrecy, agreement, MITM resistance) hold a fortiori for the spec's more permissive buffering model.) +- **`decryption_requires_prior_buffering`**: every decryption is preceded by buffering — the intended two-phase flow (buffer ciphertext, then decrypt after approval) is explicit in the proof surface. +- **`executable_payload_buffered_before_approval`** *(sanity)*: the payload **can** arrive and be buffered before the target user approves, proving the buffering path is reachable and the dual-consent gate is not vacuously enforced by message ordering alone. + +**Reachability and anti-vacuousness:** + +- **`executable_with_qr_leak`**, **`executable_with_source_compromise`**, **`executable_with_target_compromise`**: each compromise rule is reachable from protocol state (i.e., the compromise rules are not dead code), so the no-compromise guards in the secrecy and agreement lemmas are non-trivial. +- **`source_compromise_can_leak_payload`**, **`target_compromise_can_leak_payload`**: there exist traces where endpoint compromise (leakage of session-ephemeral private keys) leads to attacker knowledge of the payload, confirming that the no-compromise guards in the secrecy lemma are load-bearing. + +The Tamarin model intentionally abstracts away details that are orthogonal to the cryptographic proof: + +- exact NIP-01 event IDs / Schnorr signatures — relay anti-forgery relies on these but is not proved symbolically +- exact NIP-44 ciphertext framing, padding, version bytes, and nonce handling — modeled as ideal authenticated encryption (`senc`) over a DH-derived key +- HKDF-SHA256 — collapsed to tagged hashes (`h(< label, inputs >)`) preserving domain separation but not RFC 5869 internals +- ECDH — modeled as symbolic Diffie-Hellman, not exact secp256k1 x-coordinate extraction +- SAS comparison — modeled as perfect (requiring actual key agreement); the ~20-bit collision bound (1/10^6) is a separate computational argument (see §Design Rationale) +- timeout and abort branches +- duplicate-event bookkeeping +- `p`-tag validation and within-session replay protection — these are state-machine / implementation requirements, not Tamarin results +- version negotiation (`version` field in `offer`) +- `complete` success/failure semantics +- payload typing (`nsec` / `bunker` / `connect` / `custom`) + +Those behaviors remain normative in this document and in the Rust implementation; they are simply not the focus of the symbolic proof. + +Run the proof with: + +```bash +tamarin-prover --prove crates/sprout-core/src/pairing/NIP-AB.spthy +``` + ## Cryptographic Primitives ### ECDH diff --git a/crates/sprout-core/src/pairing/NIP-AB.spthy b/crates/sprout-core/src/pairing/NIP-AB.spthy new file mode 100644 index 000000000..65b5d2670 --- /dev/null +++ b/crates/sprout-core/src/pairing/NIP-AB.spthy @@ -0,0 +1,455 @@ +theory NIP_AB +begin + +builtins: diffie-hellman, hashing, symmetric-encryption + +rule Source_Start: + [ Fr(~qr), Fr(~xs) ] + --[ + SourceStarted(h(< 'session-id', ~qr >), 'g'^~xs) + ]-> + [ + SrcWaiting(~qr, ~xs), + !QrVisible(~qr, 'g'^~xs), + !SourceSecrets(~qr, ~xs) + ] + +rule Leak_QR: + [ !QrVisible(qr, pkS) ] + --[ + QrLeaked(h(< 'session-id', qr >), pkS) + ]-> + [ Out(< qr, pkS >) ] + +rule Compromise_Source_Session: + [ !SourceSecrets(qr, xs) ] + --[ + SourceCompromised(h(< 'session-id', qr >), 'g'^xs) + ]-> + [ Out(< qr, xs >) ] + +rule Target_Scan_QR_And_Send_Offer: + [ !QrVisible(qr, pkS), Fr(~xt) ] + --[ + TargetStarted(h(< 'session-id', qr >), pkS, 'g'^~xt) + ]-> + [ + TgtOfferSent(qr, pkS, ~xt, 'g'^~xt), + !TargetSecrets(qr, pkS, ~xt), + Out( + < + 'offer_evt', + 'g'^~xt, + senc( + < 'offer', h(< 'session-id', qr >) >, + h(< 'pair-key', pkS^~xt >) + ) + > + ) + ] + +rule Compromise_Target_Session: + [ !TargetSecrets(qr, pkS, xt) ] + --[ + TargetCompromised(h(< 'session-id', qr >), pkS, 'g'^xt) + ]-> + [ Out(< qr, xt >) ] + +rule Source_Accepts_Offer: + [ SrcWaiting(qr, xs), + In( + < + 'offer_evt', + pkT, + senc( + < 'offer', h(< 'session-id', qr >) >, + h(< 'pair-key', pkT^xs >) + ) + > + ) + ] + --[ + SourceAcceptedOffer(h(< 'session-id', qr >), 'g'^xs, pkT) + ]-> + [ + SrcSasReady(qr, xs, pkT) + ] + +// SAS comparison is modeled as perfect: the rule requires both devices' +// state facts with matching cryptographic material, so it only fires when +// the ECDH shared secret (and therefore the SAS code) genuinely agrees. +// In reality SAS provides ~20 bits of entropy (1/10^6 collision); that +// computational bound is argued separately in §Design Rationale. +rule User_Compares_Matching_SAS: + [ SrcSasReady(qr, xs, pkT), + TgtOfferSent(qr, 'g'^xs, xt, pkT) + ] + --[ + SasMatched( + h(< 'session-id', qr >), + 'g'^xs, + pkT, + h(< 'sas', pkT^xs, qr >) + ) + ]-> + [ + SrcUserConfirmed(qr, xs, pkT), + TgtAwaitingSasConfirm(qr, 'g'^xs, xt) + ] + +// Transcript hash matches spec §Step 3 (see also PR #346 clarifications): +// transcript_hash = HKDF(IKM = session_id || pkS || pkT || sas_input, +// salt = session_secret, info = "nostr-pair-transcript-v1") +// Symbolically we collapse HKDF to h(.) and rely on collision resistance; +// qr (session_secret) is already committed via session_id and sas_input, so +// we do not include it again here. +// +// Per §Step 3, the transcript hash is a detection mechanism for session +// inconsistency, not the MITM prevention gate (that role belongs to the +// user's SAS comparison, modeled by User_Compares_Matching_SAS above). +rule Source_Sends_SAS_Confirm: + [ SrcUserConfirmed(qr, xs, pkT) ] + --[ + SourceSentSasConfirm(h(< 'session-id', qr >), 'g'^xs, pkT) + ]-> + [ + SrcReadyPayload(qr, xs, pkT), + Out( + < + 'sas_confirm_evt', + senc( + < + 'sas-confirm', + h( + < + 'transcript', + h(< 'session-id', qr >), + 'g'^xs, + pkT, + h(< 'sas', pkT^xs, qr >) + > + ) + >, + h(< 'pair-key', pkT^xs >) + ) + > + ) + ] + +rule Target_Receives_SAS_Confirm: + [ TgtAwaitingSasConfirm(qr, pkS, xt), + In( + < + 'sas_confirm_evt', + senc( + < + 'sas-confirm', + h( + < + 'transcript', + h(< 'session-id', qr >), + pkS, + 'g'^xt, + h(< 'sas', pkS^xt, qr >) + > + ) + >, + h(< 'pair-key', pkS^xt >) + ) + > + ) + ] + --[ + TargetVerifiedTranscript(h(< 'session-id', qr >), pkS, 'g'^xt) + ]-> + [ + TgtAwaitingUserApproval(qr, pkS, xt), + TgtCanBuffer(qr, pkS, xt) + ] + +// Target user approval: AwaitingConfirmation -> Transferring (spec §Step 3). +// This fires only after transcript verification (Target_Receives_SAS_Confirm). +rule Target_User_Approves_After_Transcript: + [ TgtAwaitingUserApproval(qr, pkS, xt) ] + --[ + TargetUserApproved(h(< 'session-id', qr >), pkS, 'g'^xt) + ]-> + [ + TgtTransferring(qr, pkS, xt) + ] + +rule Source_Sends_Payload: + [ SrcReadyPayload(qr, xs, pkT), Fr(~payload) ] + --[ + SourceSentPayload(h(< 'session-id', qr >), 'g'^xs, pkT, ~payload), + PayloadMarkedSecret(h(< 'session-id', qr >), ~payload) + ]-> + [ + SrcAwaitingComplete(qr, xs, pkT, ~payload), + Out( + < + 'payload_evt', + senc( + < 'payload', ~payload >, + h(< 'pair-key', pkT^xs >) + ) + > + ) + ] + +// --- Payload buffering (spec §Event Validation, §Step 3-4) --- +// +// Per #346, the source sends payload immediately after sas-confirm without +// waiting for the target. The target may therefore receive the encrypted +// payload while still in AwaitingConfirmation (before user approval). +// The spec requires: buffer the ciphertext, do NOT decrypt or import until +// both transcript_hash is verified AND the user confirms SAS on the target. +// +// We model this as two rules: +// 1. Target_Buffers_Payload — receives ciphertext into a holding fact +// WITHOUT extracting the plaintext. The rule validates that the +// ciphertext is encrypted under the session's DH-derived key +// (h(< 'pair-key', pkS^xt >)), matching the spec's requirement that +// invalid events are silently discarded without advancing state. +// Only fires after transcript verification (linear TgtCanBuffer), +// matching the spec's state table where `payload` is valid only in +// AwaitingConfirmation or Transferring (both post-transcript-verify). +// The linear fact is consumed, so at most one payload can be buffered +// per session — matching the spec's single-payload semantics. +// 2. Target_Decrypts_Payload — pattern-matches senc() to extract plaintext. +// Requires both TgtTransferring (post-approval) and the buffered +// ciphertext. This is the dual-consent gate: decryption only happens +// after transcript verification + user approval. + +rule Target_Buffers_Payload: + [ TgtCanBuffer(qr, pkS, xt), + In(< 'payload_evt', senc(msg, h(< 'pair-key', pkS^xt >)) >) + ] + --[ + TargetBufferedPayload(h(< 'session-id', qr >), pkS, 'g'^xt) + ]-> + [ + TgtPayloadBuffer(qr, pkS, xt, senc(msg, h(< 'pair-key', pkS^xt >))) + ] + +// Target decrypts the payload only after entering Transferring state +// (transcript verified + user approved). This is the dual-consent gate: +// the senc() pattern match here is the symbolic decryption operation. +rule Target_Decrypts_Payload: + [ TgtTransferring(qr, pkS, xt), + TgtPayloadBuffer(qr, pkS, xt, + senc( + < 'payload', payload >, + h(< 'pair-key', pkS^xt >) + ) + ) + ] + --[ + TargetDecryptedPayload(h(< 'session-id', qr >), pkS, 'g'^xt, payload) + ]-> + [ + TgtHasPayload(qr, pkS, xt, payload) + ] + +rule Target_Sends_Complete: + [ TgtHasPayload(qr, pkS, xt, payload) ] + --[ + TargetCompleted(h(< 'session-id', qr >), pkS, 'g'^xt, payload) + ]-> + [ + TgtDone(qr, pkS, xt, payload), + Out( + < + 'complete_evt', + senc('complete', h(< 'pair-key', pkS^xt >)) + > + ) + ] + +rule Source_Receives_Complete: + [ SrcAwaitingComplete(qr, xs, pkT, payload), + In( + < + 'complete_evt', + senc('complete', h(< 'pair-key', pkT^xs >)) + > + ) + ] + --[ + SourceCompleted(h(< 'session-id', qr >), 'g'^xs, pkT, payload) + ]-> + [ + SrcDone(qr, xs, pkT, payload) + ] + +// ============================================================================ +// Core security lemmas (invariants) +// ============================================================================ + +// Happy path: both sides complete with the same session and payload. +lemma executable_core_flow: + exists-trace + "Ex sid pkS pkT payload #i #j. + TargetCompleted(sid, pkS, pkT, payload) @ i + & SourceCompleted(sid, pkS, pkT, payload) @ j" + +// SAS gate: source never sends the payload without a prior SAS match. +lemma payload_requires_successful_sas_match: + "All sid pkS pkT payload #i. + SourceSentPayload(sid, pkS, pkT, payload) @ i + ==> (Ex sas #j. + SasMatched(sid, pkS, pkT, sas) @ j + & #j < #i)" + +// Payload secrecy: without endpoint compromise, the payload is secret. +// Note: this holds even under QR-code leak. The SAS gate prevents a MITM +// from causing the source to send the payload under the attacker's key, +// because the SAS rule only fires when the source's accepted pkT matches +// a genuine fresh target ephemeral (see sas_match_implies_genuine_target). +lemma payload_secrecy_without_endpoint_compromise: + "All sid payload #i. + PayloadMarkedSecret(sid, payload) @ i + & not (Ex pkS #r. SourceCompromised(sid, pkS) @ r) + & not (Ex pkS pkT #r. TargetCompromised(sid, pkS, pkT) @ r) + ==> not (Ex #j. K(payload) @ j)" + +// Target-side agreement: if the target completes, the source genuinely +// sent that exact payload under this session. +lemma target_completion_agrees_on_source_payload: + "All sid pkS pkT payload #i. + TargetCompleted(sid, pkS, pkT, payload) @ i + & not (Ex pkS2 #r. SourceCompromised(sid, pkS2) @ r) + & not (Ex pkS2 pkT2 #r. TargetCompromised(sid, pkS2, pkT2) @ r) + ==> (Ex #j. + SourceSentPayload(sid, pkS, pkT, payload) @ j + & #j < #i)" + +// Source-side completion soundness: if the source sees `complete`, the +// target really completed this session. +lemma source_completion_implies_prior_target_completion_without_compromise: + "All sid pkS pkT payload #i. + SourceCompleted(sid, pkS, pkT, payload) @ i + & not (Ex pkS2 #r. SourceCompromised(sid, pkS2) @ r) + & not (Ex pkS2 pkT2 #r. TargetCompromised(sid, pkS2, pkT2) @ r) + ==> (Ex #j. + TargetCompleted(sid, pkS, pkT, payload) @ j + & #j < #i)" + +// Injective agreement (target → source): each target completion corresponds +// to a unique source payload send, and that send is itself unique. This is +// one-directional; the reverse (every send leads to a completion) is a +// liveness property not provable under Dolev-Yao scheduling. +lemma injective_target_source_agreement: + "All sid pkS pkT payload #i. + TargetCompleted(sid, pkS, pkT, payload) @ i + & not (Ex pkS2 #r. SourceCompromised(sid, pkS2) @ r) + & not (Ex pkS2 pkT2 #r. TargetCompromised(sid, pkS2, pkT2) @ r) + ==> (Ex #j. + SourceSentPayload(sid, pkS, pkT, payload) @ j + & #j < #i + & not (Ex #i2. + TargetCompleted(sid, pkS, pkT, payload) @ i2 + & not (#i2 = #i)) + & not (Ex #j2. + SourceSentPayload(sid, pkS, pkT, payload) @ j2 + & not (#j2 = #j)))" + +// ============================================================================ +// MITM-resistance test cases +// ============================================================================ + +// "MITM does not work": any SAS match pins the source's view of pkT to an +// actual target-generated ephemeral ('g'^~xt from Target_Scan_QR_And_Send_Offer). +// A network adversary who substitutes the offer's pkT with an attacker-chosen +// value can never make this lemma's conclusion hold, because the fresh ~xt +// in TargetStarted is outside attacker knowledge. +lemma sas_match_implies_genuine_target: + "All sid pkS pkT sas #i. + SasMatched(sid, pkS, pkT, sas) @ i + ==> (Ex #j. + TargetStarted(sid, pkS, pkT) @ j + & #j < #i)" + +// Composition: no payload is ever sent under a pkT the real target did not +// produce. Follows from payload_requires_successful_sas_match combined with +// sas_match_implies_genuine_target, and is the explicit no-MITM guarantee. +lemma payload_delivery_requires_genuine_target: + "All sid pkS pkT payload #i. + SourceSentPayload(sid, pkS, pkT, payload) @ i + ==> (Ex #j. + TargetStarted(sid, pkS, pkT) @ j + & #j < #i)" + +// Dual-consent gate (spec §Step 3, PR #346): the target never processes +// (decrypts/imports) a payload without BOTH transcript verification AND +// an explicit user-approval step. The payload may arrive and be buffered +// earlier (see Target_Buffers_Payload), but processing is gated. +lemma target_decrypts_payload_only_after_dual_consent: + "All sid pkS pkT payload #i. + TargetDecryptedPayload(sid, pkS, pkT, payload) @ i + ==> (Ex #j #k. + TargetVerifiedTranscript(sid, pkS, pkT) @ j + & TargetUserApproved(sid, pkS, pkT) @ k + & #j < #i + & #k < #i)" + +// ============================================================================ +// Reachability / sanity test cases +// ============================================================================ +// +// These exists-trace lemmas prove that the compromise model is meaningful +// (each compromise rule is actually reachable within a valid protocol run) +// and that compromise genuinely breaks payload confidentiality. Without +// these, a trivially unreachable compromise rule would make the no-compromise +// secrecy claims vacuous. + +lemma executable_with_qr_leak: + exists-trace + "Ex sid pkS #r. QrLeaked(sid, pkS) @ r" + +lemma executable_with_source_compromise: + exists-trace + "Ex sid pkS #r. SourceCompromised(sid, pkS) @ r" + +lemma executable_with_target_compromise: + exists-trace + "Ex sid pkS pkT #r. TargetCompromised(sid, pkS, pkT) @ r" + +// Buffer-then-decrypt sequencing: every decryption is preceded by buffering. +// Makes the intended two-phase flow explicit in the proof surface. +lemma decryption_requires_prior_buffering: + "All sid pkS pkT payload #i. + TargetDecryptedPayload(sid, pkS, pkT, payload) @ i + ==> (Ex #j. + TargetBufferedPayload(sid, pkS, pkT) @ j + & #j < #i)" + +// Sanity: the payload CAN arrive (be buffered) before the target user +// approves. This proves the buffering path is reachable and the dual-consent +// gate is not vacuously enforced by message ordering alone. +lemma executable_payload_buffered_before_approval: + exists-trace + "Ex sid pkS pkT #i #j. + TargetBufferedPayload(sid, pkS, pkT) @ i + & TargetUserApproved(sid, pkS, pkT) @ j + & #i < #j" + +// Source-side compromise: an attacker who learns xs can decrypt the payload. +// Counter-example to a naive "secrecy always holds" claim; justifies the +// `not SourceCompromised` guard in payload_secrecy_without_endpoint_compromise. +lemma source_compromise_can_leak_payload: + exists-trace + "Ex sid pkS payload #i #j #k. + PayloadMarkedSecret(sid, payload) @ i + & SourceCompromised(sid, pkS) @ j + & K(payload) @ k" + +// Target-side compromise: same story, from the target side. +lemma target_compromise_can_leak_payload: + exists-trace + "Ex sid pkS pkT payload #i #j #k. + PayloadMarkedSecret(sid, payload) @ i + & TargetCompromised(sid, pkS, pkT) @ j + & K(payload) @ k" + +end