fix: replay protection on the pull protocol (AAD-bound seq + per-direction keys)
ober
67ffd7fe6e2db56ad63722298267d575bdfb92ca
--- a/Makefile +++ b/Makefile @@ -447,6 +447,15 @@ crypto-psk-check: rust cd $(BUILD) && cargo build --release $(SCHEME) --libdirs $(LIBDIRS) --script examples/crypto_psk_check.ss +# Pull-protocol replay protection: the AAD-bound transport session (monotonic +# per-direction seq + replay high-water mark + per-direction keys) on top of the +# verified psk-transport-seal-aad/-open-aad kernels. Proves a captured frame is +# rejected on re-submit, a stale seq is rejected, reflection and cross-channel +# splicing fail, and fresh in-order frames still open. Needs the dylib. +transport-replay-check: rust + cd $(BUILD) && cargo build --release + $(SCHEME) --libdirs $(LIBDIRS) --script examples/transport_replay_check.ss + # ECIES public-key encryption end-to-end (secmon ecies.rs encrypt/decrypt): the # deterministic x25519+hkdf+aes-gcm core is the typed kernel (verified by `make # test`); this drives it through the FFI bridge + the ephemeral-keypair/nonce @@ -617,6 +626,7 @@ checks: kernels-check ensure-jsqlite $(SCHEME) --libdirs $(LIBDIRS) --script examples/dga_check.ss $(SCHEME) --libdirs $(LIBDIRS) --script examples/calendar_check.ss $(SCHEME) --libdirs $(LIBDIRS) --script examples/crypto_psk_check.ss + $(SCHEME) --libdirs $(LIBDIRS) --script examples/transport_replay_check.ss $(SCHEME) --libdirs $(LIBDIRS) --script examples/crypto_ecies_check.ss $(SCHEME) --libdirs $(LIBDIRS) --script examples/monitor_process_check.ss $(SCHEME) --libdirs $(LIBDIRS) --script examples/monitor_network_check.ss --- a/bin/collector.ss +++ b/bin/collector.ss @@ -48,9 +48,12 @@ message->bytes message-from-bytes make-serialized-event serialized-event-seq serialized-event-timestamp-ms serialized-event-encrypted-data) - (only (jsecmon kernels) hex-decode psk-hex-32? derive-auth-key derive-transport-key) + (only (jsecmon kernels) hex-decode psk-hex-32? derive-auth-key derive-transport-key + derive-transport-key-c2s derive-transport-key-s2c) (only (jsecmon crypto-psk) - transport-encrypt transport-decrypt respond-to-challenge) + transport-encrypt transport-decrypt respond-to-challenge + psk-challenge-nonce derive-channel-id make-client-transport-session + transport-session-seal transport-session-open) (only (jsecmon crypto-ecies) ecies-decrypt) (only (jsecmon event-codec) security-event-from-bytes) (only (jsecmon event-json) event-data-hash event-data-json) @@ -158,14 +161,29 @@ (if (not dec) (err "transport decryption failed") (message-from-bytes dec))))) -;; ── connect + PSK handshake → a live client (in out transport-key) ──────────── -(defstruct client (in out tk)) +;; Post-auth requests ride the replay-protected session (monotonic seq in the +;; AAD + per-direction keys), mirroring the agent's request loop. +(def (send-session-message out sess msg) + (put-bytevector out (frame-encode (transport-session-seal sess (message->bytes msg)))) + (flush-output-port out)) + +(def (recv-session-message in sess) + (let ((len (frame-read-length (read-exact in 4)))) + (when (> len *max-msg*) (raise-message 'recv-session-message "message too large")) + (let ((dec (transport-session-open sess (read-exact in len)))) + (if (not dec) (err "transport decryption failed") + (message-from-bytes dec))))) + +;; ── connect + PSK handshake → a live client (in out transport-key session) ──── +(defstruct client (in out tk sess)) (def (client-connect host psk-hex) ;; host = "addr:port"; throws on failure (let-values (((addr port) (split-host-port host))) (let* ((psk (hex-decode psk-hex)) (auth-key (derive-auth-key psk)) - (transport-key (derive-transport-key psk))) + (transport-key (derive-transport-key psk)) + (c2s-key (derive-transport-key-c2s psk)) + (s2c-key (derive-transport-key-s2c psk))) (let-values (((in out) (tcp-connect-binary addr port))) (let ((r (recv-message in transport-key))) (when (err? r) @@ -173,17 +191,21 @@ (let ((msg (unwrap r))) (unless (eq? (car msg) 'challenge) (raise-message 'connect "expected challenge")) - (send-message out transport-key - (list 'challenge-response (respond-to-challenge auth-key (cadr msg)))) - (make-client in out transport-key))))))) + (let* ((challenge (cadr msg)) + (sess (make-client-transport-session + c2s-key s2c-key + (derive-channel-id (psk-challenge-nonce challenge))))) + (send-message out transport-key + (list 'challenge-response (respond-to-challenge auth-key challenge))) + (make-client in out transport-key sess)))))))) (def (client-close c) (try (close-port (client-in c)) (catch (e) #f)) (try (close-port (client-out c)) (catch (e) #f))) (def (client-request c msg) ;; send one request, await one reply - (send-message (client-out c) (client-tk c) msg) - (let ((r (recv-message (client-in c) (client-tk c)))) + (send-session-message (client-out c) (client-sess c) msg) + (let ((r (recv-session-message (client-in c) (client-sess c)))) (if (err? r) (raise-message 'request (unwrap-err r)) (unwrap r)))) ;; GetEventsAfter → the SerializedEvent list (or signal auth/error). new file mode 100644 --- /dev/null +++ b/examples/transport_replay_check.ss @@ -0,0 +1,79 @@ +;;; Replay/reflection/splicing checks for the pull-protocol transport session. +;;; +;;; The verified AEAD core is `psk-transport-seal-aad`/`-open-aad` (pinned by +;;; tests/psk_vectors.rs). Here we drive the untyped session orchestration in +;;; `(jsecmon crypto-psk)` — the monotonic per-direction seq bound into the AAD +;;; and the replay high-water mark — proving a captured frame cannot be +;;; re-submitted, a stale seq is rejected, a reflected frame (wrong direction +;;; key) fails, a cross-channel splice fails, and fresh in-order frames still +;;; open. +;;; +;;; scheme --libdirs "$JERBOA/lib:." --script examples/transport_replay_check.ss + +(import (jerboa prelude) + (jsecmon kernels) + (jsecmon crypto-psk)) + +(def fails 0) +(def (check label got want) + (let ((ok (equal? got want))) + (unless ok (set! fails (+ fails 1))) + (displayln (if ok " ok " " FAIL ") label " => " got + (if ok "" (str " (want " want ")"))))) + +(def psk (make-bytevector 32 66)) +(def c2s (derive-transport-key-c2s psk)) +(def s2c (derive-transport-key-s2c psk)) +(def channel-id (derive-channel-id (make-bytevector 32 7))) +(def msg1 (string->utf8 "request-one")) +(def msg2 (string->utf8 "request-two")) + +(def (fresh-pair) + (values (make-client-transport-session c2s s2c channel-id) + (make-server-transport-session c2s s2c channel-id))) + +(displayln "direction keys (domain separation):") +(check "c2s != s2c" (equal? c2s s2c) #f) +(check "c2s != legacy transport" (equal? c2s (derive-transport-key psk)) #f) + +(displayln "replay-protected transport session:") +;; Regression guard: fresh, in-order frames are accepted in both directions. +(let-values (((client server) (fresh-pair))) + (let* ((f1 (transport-session-seal client msg1)) ;; seq 1 + (f2 (transport-session-seal client msg2))) ;; seq 2 + (check "fresh in-order frame 1 accepted" (transport-session-open server f1) msg1) + (check "fresh in-order frame 2 accepted" (transport-session-open server f2) msg2)) + (let ((r1 (transport-session-seal server (string->utf8 "reply")))) + (check "server->client frame accepted" + (transport-session-open client r1) (string->utf8 "reply")))) + +;; Replay: the same captured ciphertext is rejected the second time. +(let-values (((client server) (fresh-pair))) + (let ((f1 (transport-session-seal client msg1))) + (check "first submit accepted" (transport-session-open server f1) msg1) + (check "replayed frame rejected" (transport-session-open server f1) #f))) + +;; Stale/lower seq: a frame older than the high-water mark is rejected. +(let-values (((client server) (fresh-pair))) + (let* ((f1 (transport-session-seal client msg1)) ;; seq 1 + (f2 (transport-session-seal client msg2))) ;; seq 2 + (check "newer frame accepted first" (transport-session-open server f2) msg2) + (check "stale lower-seq frame rejected" (transport-session-open server f1) #f))) + +;; Reflection: a frame sealed for the opposite direction must not open. +(let-values (((client server) (fresh-pair))) + (let ((s2c-frame (transport-session-seal server msg1))) ;; sealed s2c + (check "reflected frame rejected" (transport-session-open server s2c-frame) #f) + (check "intended receiver accepts s2c" (transport-session-open client s2c-frame) msg1))) + +;; Cross-context splicing: a frame from another channel does not open. +(let ((other-channel (derive-channel-id (make-bytevector 32 8)))) + (let ((client-a (make-client-transport-session c2s s2c channel-id)) + (server-b (make-server-transport-session c2s s2c other-channel))) + (let ((fa (transport-session-seal client-a msg1))) + (check "cross-channel frame rejected" (transport-session-open server-b fa) #f)))) + +(newline) +(if (= fails 0) + (displayln "OK: replay/reflection/splicing rejected, fresh in-order frames accepted.") + (begin (displayln fails " FAILURES") (exit 1))) --- a/jsecmon/agent-server.ss +++ b/jsecmon/agent-server.ss @@ -52,17 +52,23 @@ (only (jsecmon local-store) local-store-persist local-store-count local-store-latest-seq) (only (jsecmon crypto-ecies) ecies-encrypt) - (only (jsecmon crypto-psk) - transport-encrypt transport-decrypt generate-challenge - verify-response current-epoch-seconds) - (only (jsecmon kernels) derive-auth-key derive-transport-key) + (only (jsecmon crypto-psk) + transport-encrypt transport-decrypt generate-challenge + verify-response current-epoch-seconds + psk-challenge-nonce derive-channel-id + make-server-transport-session + transport-session-seal transport-session-open) + (only (jsecmon kernels) + derive-auth-key derive-transport-key + derive-transport-key-c2s derive-transport-key-s2c) (only (jsecmon calendar) now-ms)) (def *max-msg* (* 10 1024 1024)) (def *challenge-max-age-secs* 60) (defstruct runtime - (buffer lock public-key auth-key transport-key start-ms hostname next-id local-store)) + (buffer lock public-key auth-key transport-key + transport-c2s-key transport-s2c-key start-ms hostname next-id local-store)) (defstruct agent-listener (tcp host port stopped guard pool policy)) (def agent-runtime? runtime?) @@ -71,6 +77,8 @@ (def agent-runtime-public-key runtime-public-key) (def agent-runtime-auth-key runtime-auth-key) (def agent-runtime-transport-key runtime-transport-key) + (def agent-runtime-transport-c2s-key runtime-transport-c2s-key) + (def agent-runtime-transport-s2c-key runtime-transport-s2c-key) (def agent-runtime-start-ms runtime-start-ms) (def agent-runtime-hostname runtime-hostname) (def agent-runtime-next-id runtime-next-id) @@ -86,6 +94,8 @@ public-key (derive-auth-key psk) (derive-transport-key psk) + (derive-transport-key-c2s psk) + (derive-transport-key-s2c psk) (now-ms) (if (and (pair? opts) (string? (car opts))) (car opts) "unknown") 0 @@ -185,6 +195,19 @@ (let ((dec (transport-decrypt transport-key (read-exact in len)))) (if dec (message-from-bytes dec) (err "transport decryption failed"))))) + ;; Post-auth frames ride a replay-protected session: a monotonic seq bound + ;; into the AAD plus per-direction keys. A captured request cannot be + ;; re-submitted (stale seq) nor reflected (wrong direction key). + (def (send-session-message out sess msg) + (put-bytevector out (frame-encode (transport-session-seal sess (message->bytes msg)))) + (flush-output-port out)) + + (def (recv-session-message in sess) + (let ((len (frame-read-length (read-exact in 4)))) + (when (> len *max-msg*) (error 'recv-session-message "message too large")) + (let ((dec (transport-session-open sess (read-exact in len)))) + (if dec (message-from-bytes dec) (err "transport decryption failed"))))) + (def (status-response rt) (list 'status (agent-buffered-count rt) @@ -225,19 +248,24 @@ *challenge-max-age-secs* (current-epoch-seconds))) (send-message out tk (list 'auth-failed)) - (let loop () - ;; This absolute per-frame deadline is reset only after a - ;; complete authenticated request, not after each byte. - (tcp-set-deadline-ms! conn (network-policy-idle-ms policy)) - (let ((rr (recv-message in tk))) - (unless (err? rr) - (let ((msg (unwrap rr))) - (send-message - out tk - (if (and (eq? (car msg) 'request) (pair? (cdr msg))) - (handle-request rt (cadr msg)) - (list 'error "expected request")))) - (loop)))))))))) + (let ((sess (make-server-transport-session + (agent-runtime-transport-c2s-key rt) + (agent-runtime-transport-s2c-key rt) + (derive-channel-id + (psk-challenge-nonce challenge))))) + (let loop () + ;; This absolute per-frame deadline is reset only after a + ;; complete authenticated request, not after each byte. + (tcp-set-deadline-ms! conn (network-policy-idle-ms policy)) + (let ((rr (recv-session-message in sess))) + (unless (err? rr) + (let ((msg (unwrap rr))) + (send-session-message + out sess + (if (and (eq? (car msg) 'request) (pair? (cdr msg))) + (handle-request rt (cadr msg)) + (list 'error "expected request"))) + (loop)))))))))))) (def (close-client! in out conn) (try (close-port in) (catch (e) #f)) --- a/jsecmon/crypto-psk.ss +++ b/jsecmon/crypto-psk.ss @@ -19,7 +19,12 @@ make-psk-response psk-response? psk-response-proof psk-response-counter-nonce generate-challenge respond-to-challenge verify-response - current-epoch-seconds) + current-epoch-seconds + derive-channel-id + make-transport-session transport-session? + make-server-transport-session make-client-transport-session + transport-session-seal transport-session-open + transport-session-send-seq transport-session-recv-top) (import (except (scheme) make-hash-table hash-table? sort sort! @@ -44,6 +49,77 @@ (define (transport-decrypt transport-key sealed) (psk-transport-open transport-key sealed)) + ;; --- replay-protected transport session (pull-protocol request loop) --- + ;; + ;; The post-auth request loop must not accept a captured frame twice. Each + ;; direction uses its own HKDF-derived key (so a frame sealed one way cannot + ;; be opened the other — reflection fails the tag) and a monotonic sequence + ;; number bound into the AEAD AAD as direction ‖ channel-id ‖ seq. The + ;; receiver keeps a high-water mark and rejects any seq it has already + ;; advanced past, so a replayed or stale frame fails before it can purge + ;; buffered evidence. The channel-id (SHA256 of the handshake challenge nonce) + ;; binds every frame to the session that established it, defeating + ;; cross-context splicing. The randomness the verified kernels leave out — the + ;; per-frame GCM nonce — is drawn here, as with transport-encrypt. + + (defstruct transport-session + (send-key recv-key send-dir recv-dir channel-id send-seq recv-top)) + + (define (transport-aad dir-byte channel-id seq) + (let* ((cid-len (bytevector-length channel-id)) + (aad (make-bytevector (+ 1 cid-len 8)))) + (bytevector-u8-set! aad 0 dir-byte) + (bytevector-copy! channel-id 0 aad 1 cid-len) + (bytevector-u64-set! aad (+ 1 cid-len) seq (endianness little)) + aad)) + + (define (seq->le64 seq) + (let ((bv (make-bytevector 8))) + (bytevector-u64-set! bv 0 seq (endianness little)) + bv)) + + ;; Frame layout: seq(8 LE) ‖ nonce(12) ‖ ciphertext‖tag. The seq rides in the + ;; clear so the receiver can rebuild the AAD before opening; the tag then + ;; authenticates it. + (define (transport-session-seal sess plaintext) + (let* ((seq (transport-session-send-seq sess)) + (_ (transport-session-send-seq-set! sess (+ seq 1))) + (aad (transport-aad (transport-session-send-dir sess) + (transport-session-channel-id sess) seq)) + (sealed (psk-transport-seal-aad (transport-session-send-key sess) + (random-bytes 12) plaintext aad))) + (bytevector-append (seq->le64 seq) sealed))) + + ;; Open a frame, rejecting anything stale or replayed. Returns the plaintext, + ;; or #f on a short frame, a non-fresh seq, or a failed tag (wrong direction + ;; key, wrong channel-id, or tampering). The high-water mark advances only + ;; after a successful open, so a forged seq cannot poison it. + (define (transport-session-open sess frame) + (let ((n (bytevector-length frame))) + (and (>= n 36) ;; seq(8) + nonce(12) + GCM tag(16) + (let* ((seq (bytevector-u64-ref frame 0 (endianness little))) + (top (transport-session-recv-top sess))) + (and (> seq top) ;; fresh, strictly monotonic: rejects stale + replay + (let* ((sealed-len (- n 8)) + (sealed (make-bytevector sealed-len)) + (_ (bytevector-copy! frame 8 sealed 0 sealed-len)) + (aad (transport-aad (transport-session-recv-dir sess) + (transport-session-channel-id sess) seq)) + (pt (psk-transport-open-aad (transport-session-recv-key sess) + sealed aad))) + (and pt + (begin (transport-session-recv-top-set! sess seq) pt)))))))) + + (define (derive-channel-id challenge-nonce) + (sha256-digest challenge-nonce)) + + ;; Direction byte 0 = client->server, 1 = server->client. The server sends on + ;; s2c and receives on c2s; the client is the mirror. + (define (make-server-transport-session c2s-key s2c-key channel-id) + (make-transport-session s2c-key c2s-key 1 0 channel-id 1 0)) + (define (make-client-transport-session c2s-key s2c-key channel-id) + (make-transport-session c2s-key s2c-key 0 1 channel-id 1 0)) + ;; --- challenge/response handshake (psk.rs generate/respond/verify) --- ;; ;; secmon's PskChallenge { nonce: [u8;32], timestamp: i64 } and --- a/jsecmon/kernels.ss +++ b/jsecmon/kernels.ss @@ -20,8 +20,10 @@ ;; psk crypto primitives constant-time-eq? hex-encode hex-decode hex-string? psk-hex-32? derive-auth-key derive-transport-key + derive-transport-key-c2s derive-transport-key-s2c compute-proof verify-proof psk-transport-seal psk-transport-open + psk-transport-seal-aad psk-transport-open-aad ;; ecies crypto primitives x25519-public-key ecies-seal ecies-open ;; analytics @@ -182,6 +184,17 @@ (define (derive-transport-key psk) (call->bytes (lambda (pp pl) (%derive-transport psk (bytevector-length psk) pp pl)))) + ;; Per-direction transport keys (HKDF domain separation): a frame sealed for + ;; one direction cannot be opened as the other, so reflections fail the tag. + (define %derive-transport-c2s + (fp "jt_jsecmon_typed_psk_derive_transport_key_c2s" (u8* size_t u8* u8*) unsigned-8)) + (define (derive-transport-key-c2s psk) + (call->bytes (lambda (pp pl) (%derive-transport-c2s psk (bytevector-length psk) pp pl)))) + (define %derive-transport-s2c + (fp "jt_jsecmon_typed_psk_derive_transport_key_s2c" (u8* size_t u8* u8*) unsigned-8)) + (define (derive-transport-key-s2c psk) + (call->bytes (lambda (pp pl) (%derive-transport-s2c psk (bytevector-length psk) pp pl)))) + ;; compute_proof: SHA256(auth_key ‖ nonce ‖ timestamp.to_le_bytes() ‖ ;; b"secmon-challenge-proof"). The i64 epoch-seconds timestamp marshals as ;; integer-64; the kernel encodes it little-endian internally. @@ -225,6 +238,28 @@ (%transport-open transport-key (bytevector-length transport-key) sealed (bytevector-length sealed) pp pl)))) + ;; AAD-bound transport: the request loop authenticates direction ‖ channel-id + ;; ‖ seq into the AEAD tag so a replayed, reflected, or spliced frame fails to + ;; open. Same nonce ‖ ciphertext‖tag frame shape as the empty-AAD kernel. + (define %transport-seal-aad + (fp "jt_jsecmon_typed_psk_psk_transport_seal_aad" + (u8* size_t u8* size_t u8* size_t u8* size_t u8* u8*) unsigned-8)) + (define (psk-transport-seal-aad transport-key nonce plaintext aad) + (call->bytes (lambda (pp pl) + (%transport-seal-aad transport-key (bytevector-length transport-key) + nonce (bytevector-length nonce) + plaintext (bytevector-length plaintext) + aad (bytevector-length aad) pp pl)))) + + (define %transport-open-aad + (fp "jt_jsecmon_typed_psk_psk_transport_open_aad" + (u8* size_t u8* size_t u8* size_t u8* u8*) unsigned-8)) + (define (psk-transport-open-aad transport-key sealed aad) + (call->maybe-bytes (lambda (pp pl) + (%transport-open-aad transport-key (bytevector-length transport-key) + sealed (bytevector-length sealed) + aad (bytevector-length aad) pp pl)))) + ;; ── ecies (x25519 ECDH + HKDF-SHA256 + AES-256-GCM, all vetted crates) ───── ;; The recipient's X25519 public key from a 32-byte secret scalar (clamped in ;; the dalek crate), used to derive an ephemeral public for the payload. --- a/tests/psk_vectors.rs +++ b/tests/psk_vectors.rs @@ -8,8 +8,10 @@ //! here we pin the literal expected encodings. use jerboa_typed_generated::jsecmon_typed_psk::{ - compute_proof, constant_time_eq_p, derive_auth_key, derive_transport_key, hex_decode, - hex_encode, hex_string_p, psk_hex_32_p, psk_transport_open, psk_transport_seal, verify_proof, + compute_proof, constant_time_eq_p, derive_auth_key, derive_transport_key, + derive_transport_key_c2s, derive_transport_key_s2c, hex_decode, hex_encode, hex_string_p, + psk_hex_32_p, psk_transport_open, psk_transport_open_aad, psk_transport_seal, + psk_transport_seal_aad, verify_proof, }; fn hex(data: &[u8]) -> String { @@ -179,3 +181,48 @@ fn psk_transport_seal_open_round_trips() { bad[last] ^= 0x01; assert_eq!(psk_transport_open(tk, bad), None); } + +#[test] +fn transport_direction_keys_are_domain_separated() { + // The two pull-protocol directions derive distinct keys (distinct HKDF info + // tags), and both differ from the legacy single bidirectional transport key. + let c2s = derive_transport_key_c2s(PSK_42.to_vec()); + let s2c = derive_transport_key_s2c(PSK_42.to_vec()); + assert_ne!(c2s, s2c); + assert_ne!(c2s, derive_transport_key(PSK_42.to_vec())); + assert_ne!(s2c, derive_transport_key(PSK_42.to_vec())); + // deterministic, 32 bytes + assert_eq!(c2s, derive_transport_key_c2s(PSK_42.to_vec())); + assert_eq!(c2s.len(), 32); + assert_eq!(s2c.len(), 32); +} + +#[test] +fn psk_transport_aad_round_trips_and_binds_aad() { + // The replay-protected request loop binds direction ‖ channel-id ‖ seq into + // the AEAD AAD. A frame opens only under the same key AND the same AAD, so a + // capture replayed under another seq, direction, or channel fails the tag. + let key = derive_transport_key_c2s(PSK_42.to_vec()); + let nonce = unhex("000102030405060708090a0b"); + let pt = b"request payload".to_vec(); + let aad = b"\x00channel-id-bytes\x01\x00\x00\x00\x00\x00\x00\x00".to_vec(); + let sealed = psk_transport_seal_aad(key.clone(), nonce.clone(), pt.clone(), aad.clone()); + // the 12-byte nonce is carried verbatim at the front of the frame. + assert_eq!(&sealed[..12], &nonce[..]); + // opens with the same key + AAD. + assert_eq!( + psk_transport_open_aad(key.clone(), sealed.clone(), aad.clone()), + Some(pt) + ); + // a different AAD (replayed under another seq/direction/channel) fails. + let mut other_aad = aad.clone(); + let last = other_aad.len() - 1; + other_aad[last] ^= 0x01; + assert_eq!(psk_transport_open_aad(key.clone(), sealed.clone(), other_aad), None); + // the wrong direction key fails (reflection rejected). + let other_key = derive_transport_key_s2c(PSK_42.to_vec()); + assert_eq!(psk_transport_open_aad(other_key, sealed.clone(), aad.clone()), None); + // empty AAD does not open an AAD-bound frame (and vice versa is covered by + // psk_transport_seal_open_round_trips above). + assert_eq!(psk_transport_open_aad(key, sealed, vec![]), None); +} --- a/typed/psk.ss +++ b/typed/psk.ss @@ -12,8 +12,11 @@ (typed-library (jsecmon typed psk) (export constant-time-eq? hex-encode hex-decode hex-string? psk-hex-32? - derive-auth-key derive-transport-key compute-proof verify-proof - psk-transport-seal psk-transport-open) + derive-auth-key derive-transport-key + derive-transport-key-c2s derive-transport-key-s2c + compute-proof verify-proof + psk-transport-seal psk-transport-open + psk-transport-seal-aad psk-transport-open-aad) ;; --- constant-time comparison (psk.rs::constant_time_eq) --- @@ -102,6 +105,15 @@ (def (derive-transport-key (psk : Bytes)) : Bytes (hkdf-sha256 (string->utf8 "") psk (string->utf8 "secmon-psk-transport-v1") 32)) + ;; Per-direction transport keys (domain separation). The pull protocol runs + ;; client->server and server->client under two distinct HKDF info tags so a + ;; frame sealed for one direction cannot be opened as the other — a reflected + ;; frame fails the AEAD tag instead of decrypting. + (def (derive-transport-key-c2s (psk : Bytes)) : Bytes + (hkdf-sha256 (string->utf8 "") psk (string->utf8 "secmon-psk-transport-v2:c2s") 32)) + (def (derive-transport-key-s2c (psk : Bytes)) : Bytes + (hkdf-sha256 (string->utf8 "") psk (string->utf8 "secmon-psk-transport-v2:s2c") 32)) + ;; secmon compute_proof: SHA256(auth_key ‖ nonce ‖ timestamp.to_le_bytes() ‖ ;; b"secmon-challenge-proof"). The i64 timestamp is encoded little-endian. (def (compute-proof (auth-key : Bytes) (nonce : Bytes) (timestamp : Int)) : Bytes @@ -139,4 +151,24 @@ (aes-256-gcm-open transport-key (bytevector-copy sealed 0 12) (bytevector-copy sealed 12 n) - (string->utf8 "")))))) + (string->utf8 ""))))) + + ;; --- replay-protected transport (AAD-bound) --- + ;; + ;; The pull protocol's request loop binds extra data into the AEAD tag instead + ;; of encrypting with an empty AAD. The caller supplies the AAD (direction ‖ + ;; channel-id ‖ seq); sealing authenticates it and opening re-checks it, so a + ;; frame replayed under a different seq, direction, or channel fails the tag. + ;; The frame is still nonce ‖ ciphertext‖tag, exactly like the empty-AAD form. + (def (psk-transport-seal-aad (transport-key : Bytes) (nonce : Bytes) (plaintext : Bytes) (aad : Bytes)) : Bytes + (bytevector-append nonce + (aes-256-gcm-seal transport-key nonce plaintext aad))) + + (def (psk-transport-open-aad (transport-key : Bytes) (sealed : Bytes) (aad : Bytes)) : (Option Bytes) + (let ((n (bytevector-length sealed))) + (if (< n 28) + (option-none Bytes) + (aes-256-gcm-open transport-key + (bytevector-copy sealed 0 12) + (bytevector-copy sealed 12 n) + aad)))))