jonnify·redis /redis-patterns/caching/session-management/auth-session

R1.06.3 · Session management — dive 3

Bound to the namespace.

A session is born at sign-in, ended by a logout, and refused at the door when its id is the wrong kind — so a session key can only ever be a session.

Grounding: echo/apps/echo_store/lib/echo_store/table.ex (put/3, invalidate/3, gate/2) · echo/apps/codemojex/lib/codemojex/locks.ex (the per-player lock hash) — the session the store holds and the kind law that guards it.

The lifecycle, login to logout. Select a phase to read the command that runs and what the gate does next.
sign input/3 a requestfetch — load log outinvalidate/3 next reqempty — deny the cookie carries the SES id; the store carries the row; the kind gate guards the door
readout · Select a phase. A session’s life is the login’s life: keyed at sign-in, loaded on each request, dropped on logout.
§1

Key at login, drop at logout

source · Session Creation Flow

The session’s life runs alongside the login. At sign-in, the application verifies the credentials, keys a session record under a fresh random id, and returns that id to the browser as a cookie. The session id must be cryptographically random — a guessable id is a way into someone else’s signed-in session — and the password is never stored in the session; only the user id and a token go in.

On each request, the application reads the cookie’s id, loads the session, and resolves the user from it. A loaded session means signed in; a missing one means signed out. This is the read that every protected page depends on, and it is where a sliding deadline from the last dive keeps an active session alive.

At logout, the application removes the session with DEL session:abc123. The id in the browser’s cookie now points at nothing. The very next request loads an absent session, so the gate fails closed — it treats the request as anonymous and redirects to sign in. Logout is one delete, and its effect is immediate and total.

sign in
Verify credentials, key the session, set a cryptographically random id in the cookie. No password in the session.
load
Read the cookie id, fetch the session, resolve the user. Loaded means signed in; absent means out.
DEL key
The logout. Removes the session at once; the cookie id now resolves to nothing.
fail closed
An absent session is treated as anonymous and redirected to sign in — never admitted.

Never store a password or credential in the session; keep the session lean and fetch user details from the source when needed. The session holds only the user id and an opaque token.

§2

One device, or all of them

source · Multi-Device Tracking

A learner signs in on a laptop, a phone, and a library computer — three sessions, three ids, one user. Two operations follow: “sign out this device” and “sign out everywhere”. The single-device logout is the DEL from above: remove the one session id this browser holds. “Sign out everywhere” needs to find every session a user owns.

The source pattern tracks them in a Set. On each sign-in, SADD user:1:sessions abc123 records the new session id under the user. To list a user’s active sessions, SMEMBERS user:1:sessions; to sign out everywhere, delete each session key the Set names, then delete the Set. A single-device logout also drops the id from the Set with SREM user:1:sessions abc123, so the Set stays an accurate roster.

Pick an action below to see which keys are removed and which sessions survive. A single-device logout removes one session and leaves the others signed in; sign-out-everywhere removes the whole roster at once.

Three devices, sign out one or all. Choose an action; the readout names the commands and which sessions survive.
laptop session:abc phone session:def library session:ghi user:1:sessions = {abc, def, ghi}

A Set of session ids per user turns “sign out everywhere” into a roster delete: list the Set, drop each session, drop the Set. A single-device logout removes one id and leaves the rest signed in.

§3

The session on EchoStore — the kind gate

table.ex:290, :171, :495 · verbatim

EchoStore holds a session as a branded-id-keyed row with no auth surface of its own — there is no sign or verify call in the cache. Sign-in keys the row to a branded SES id and stores it with EchoStore.Table.put/3, which sets both layers under the declared TTL — SET ecc:{sessions}:<id> (version<>value) PX ttl_ms (table.ex:290), the value framed with the write’s mint-time version. A re-auth re-puts with a fresh version, the sliding move. Logout is EchoStore.Table.invalidate/3 (table.ex:171 — a DEL on L2 plus an :ets.delete): the next read finds nothing and the gate fails closed.

The tie to a player is the kind gate, not a credential check. Before either layer is touched, gate/2 (table.ex:495) requires byte_size(id) == 14 and binary_part(id, 0, 3) == kind and BrandedId.valid?(id), returning {:error, :kind} otherwise — so a USR id can never be used as a SES key, and a wrong-namespace id is refused with zero keys on the wire. codemojex holds the same shape one level down: a player’s per-round state is a per-player hash cm:{round}:lock:{player} (Codemojex.Locks — field = position, value = code, written with HSET), so a locked position persists across guesses with no client state to lose, keyed by the player’s USR brand. How a credential is verified and a SES id is minted is the functional-Elixir and OTP craft of the /elixir course; this dive is the session the store holds and the kind law that guards it.

# A session as an EchoStore row — keyed by a branded SES id, framed and TTL'd.
# put/3 writes L2 and L1 in one synchronous call; there is no sign/verify in the cache.
SET ecc:{sessions}:SES0KH... <version<>value> PX 1800000   # EchoStore.Table.put/3 — table.ex:290
GET ecc:{sessions}:SES0KH...                                # the read splits version<>value back apart
DEL ecc:{sessions}:SES0KH...                                # EchoStore.Table.invalidate/3 — logout, table.ex:171

# the kind gate refuses a wrong-namespace id before either layer is touched (table.ex:495)
gate("SES", "USR0KH...")   # -> {:error, :kind}  (a USR id can never be a SES key)
Place the fact. Select a fact from the as-built cache; the readout names the function or law it lives in.
readout · Select a fact. Each is quoted from the real EchoStore or codemojex surface, and each lives in exactly one function or law.

Static verdicts — put/3 SET…PX → table.ex:290 · invalidate/3 → table.ex:171 · the kind gate → gate/2, table.ex:495 · the player lock → Codemojex.Locks, locks.ex.

the application · the kind law at the door

A wrong-kind id is refused before the wire

The kind gate stands at every door in the series exactly as it stands here — a wrong-namespace id never reaches Valkey. The committed cache record gates it:

bcs.4.md · the kind law at the doorfrozen
a wrong-kind id is refused at the door   zero loader runs, zero keys on the wire
the L2 row                               SET … PX, PTTL 300 ms of 300
the L1 hit                               762 ns   ← caller-side, after the gate
the pattern

Bind the session’s life to the login: key it at sign-in under a random id, load it on each request, drop it with a DEL on logout, and track ids in a Set for sign-out-everywhere. An absent session fails closed.

its EchoStore application

A branded SES row via put/3, dropped by invalidate/3 on logout, and refused at the kind gate so a USR id can never be a session key. codemojex holds the same shape in cm:{round}:lock:{player} — a player’s state in Valkey, keyed by the USR brand.

A session’s life is the login’s life: keyed on sign-in, read on each request, dropped on logout, and bound to one namespace by the kind law. That closes the session module — encode the record, set the deadline, bind it to the namespace.

Notes on Valkeythe kind law runs in the caller’s process before any key is composed; a wrong-namespace id is refused with zero keys on the wire, so a malformed id never reaches the engine — the cache’s own keyspace discipline (ecc:{<table>}:<id>, valkey.io/topics/cluster-spec).

§4

Recap — the session is the login

bind

A session ties cache state to a namespace. Sign-in keys it under a random SES id; each request loads it to find the user; logout drops it with invalidate/3 and the gate fails closed on the next request. A per-user Set of session ids makes “sign out everywhere” a roster delete. EchoStore is the worked case: put/3 frames and TTLs the row, invalidate/3 drops it, and gate/2 refuses a wrong-namespace id at the door. The functional-Elixir and OTP craft that verifies a credential is the /elixir course. That closes the session module — encode the record, set the deadline, bind it to the namespace.

§5

References

sources · related

Sources

  • Valkey — SET — set a key with PX; the framed-and-TTL’d row EchoStore.Table.put writes for a session.
  • Redis — DEL — remove a key; the logout EchoStore.Table.invalidate runs against L2.
  • Redis — SADD — add a member to a Set; the per-user roster that records each device’s session id.
  • Redis — SMEMBERS — list a Set’s members; the active-session list behind “sign out everywhere”.

Related in this course