Case Study: Building a Login State Machine and Determinizing It

"A program is correct when you can explain why it works — to a skeptic."

Executive Summary

Authentication flows are state machines whether or not anyone admits it: a session is logged out, then logged in, maybe locked after too many failures, and every event (login, logout, fail, …) is a symbol that drives the session from one state to the next. In this build-focused case study you will construct, from a written security policy, a deterministic finite automaton that recognizes exactly the valid sequences of authentication events — and reject everything else, including the malformed sequences an attacker might try. You will encode it on the chapter's universal run_dfa engine (§35.2), grow it into a small reusable LoginDFA for the Toolkit, then meet a nondeterministic specification of an "alarm" rule and convert it to a DFA by the subset construction (§35.3) so it can run on real hardware. The thread is constructive throughout: policy → machine → code → determinized machine.

The payoff is a validator you can defend: not "it passes the tests," but "here is the automaton, here is why every accepted sequence is policy-compliant and every rejected one is not."

Skills applied

  • Translating an informal security policy into a formal language over an event alphabet (§35.1).
  • Designing a DFA — choosing states as "what must I remember?" — with a total $\delta$ and a dead state (§35.2).
  • Encoding and running a DFA on the universal driver; packaging it as a reusable DFA (§35.2, Project Checkpoint).
  • Building an NFA for a "guessing" rule and determinizing it via the subset construction (§35.3).
  • Tracing computations by hand to verify the build against the policy.

Background

The scenario

You are hardening the session layer of a service. The security team hands you a policy in prose and asks for a validator that, given the log of authentication events for a session, decides whether that log is a valid sequence under the policy. Invalid logs (impossible orderings, actions after lockout, etc.) should be flagged for investigation.

The event alphabet is $$\Sigma = \{\, \texttt{login},\ \texttt{logout},\ \texttt{fail},\ \texttt{reset} \,\},$$ where login is a successful authentication, fail is a failed attempt, logout ends a session, and reset is an administrator unlocking a locked account. The policy:

  1. A session starts logged out.
  2. From logged out, a successful login moves to logged in; a fail stays logged out (a failed attempt) but counts; logout and reset from logged out are invalid (nothing to log out of / nothing to reset).
  3. Two fails in a row (without an intervening login) move the account to locked.
  4. From logged in, logout returns to logged out; fail is invalid (you are already authenticated); login again is invalid (already logged in).
  5. From locked, only reset is valid (back to logged out); any other event is invalid.
  6. A log is valid iff it never takes an invalid step. (We accept a session in any of the legitimate states — logged out, logged in, or locked — as long as every step was allowed.)

💡 Intuition: "Valid sequence of events" is a language over $\Sigma$ (§35.1), and "never takes an invalid step" is exactly the job of a DFA with a dead state: the moment an illegal event occurs, we route to a trap from which we never escape, and the trap is non-accepting. Everything else is accepting. Building the machine is writing the validator.

Why this matters

Session and authentication logic is where security bugs hide: a missing transition lets an attacker reach a state the designers never intended ("logged in without logging in"). Modeling the flow as an explicit automaton makes the complete behavior visible — every state, every event — so you can audit it. The "total $\delta$" discipline of §35.2 is not pedantry here; a forgotten transition is a security hole. And because the same five-line engine runs every DFA, the validator is tiny and trustworthy.

Phase 1: Choose the states — "what must I remember?"

The design question of §35.2 is always what minimal fact about the prefix must I carry forward? Read the policy and the answer falls out. To decide the next legal event, the machine must know:

  • whether the session is logged out, logged in, or locked; and
  • while logged out, how many consecutive fails have occurred (0 or 1) — because the second in a row triggers lockout (policy 3).

That gives the states:

State Meaning Accepting?
$\text{Out}_0$ logged out, $0$ consecutive fails (start) yes
$\text{Out}_1$ logged out, $1$ consecutive fail yes
$\text{In}$ logged in yes
$\text{Lock}$ locked (awaiting reset) yes
$\text{Dead}$ an invalid event has occurred (trap) no

All legitimate states accept (policy 6 says we accept any session whose every step was legal); only the trap $\text{Dead}$ rejects. The start state is $\text{Out}_0$ (policy 1). Note we split "logged out" into $\text{Out}_0$ and $\text{Out}_1$ precisely because the machine must remember whether the previous event was a fail — the textbook move of "remember exactly the distinguishing fact, nothing more."

🔄 Check Your Understanding Why do we need two logged-out states but only one logged-in state?

Answer

The lockout rule (policy 3) depends on the count of consecutive fails while logged out, so the machine must distinguish "0 fails so far" from "1 fail so far" — two states. While logged in, no rule depends on any further count: every event from logged in has a fixed verdict regardless of history, so one state $\text{In}$ suffices. This is the §35.2 principle: add a state only when a rule forces you to remember something new.

Phase 2: Build the transition table (and make $\delta$ total)

Now translate each policy clause into transitions, being careful that every state has an arrow for every one of the four symbols (§35.2: $\delta$ must be total). Anything the policy calls "invalid" routes to $\text{Dead}$; $\text{Dead}$ loops to itself on everything.

$\delta$ login logout fail reset
$\to \text{Out}_0$ (accept) $\text{In}$ $\text{Dead}$ $\text{Out}_1$ $\text{Dead}$
$\text{Out}_1$ (accept) $\text{In}$ $\text{Dead}$ $\text{Lock}$ $\text{Dead}$
$\text{In}$ (accept) $\text{Dead}$ $\text{Out}_0$ $\text{Dead}$ $\text{Dead}$
$\text{Lock}$ (accept) $\text{Dead}$ $\text{Dead}$ $\text{Dead}$ $\text{Out}_0$
$\text{Dead}$ (reject) $\text{Dead}$ $\text{Dead}$ $\text{Dead}$ $\text{Dead}$

Walk a few cells against the policy to check the build. From $\text{Out}_0$ a login succeeds → $\text{In}$ (policy 2); a fail is the first failure → $\text{Out}_1$ (policy 2, and we now remember one fail); a logout or reset is invalid → $\text{Dead}$ (policy 2). From $\text{Out}_1$ a second fail locks the account → $\text{Lock}$ (policy 3); a login still succeeds and resets the count by landing in $\text{In}$ (policy 4 implies a success clears consecutive-fail tracking). From $\text{In}$, only logout is legal (policy 4). From $\text{Lock}$, only reset (policy 5).

⚠️ Common Pitfall: It is tempting to draw only the "interesting" arrows — login, logout, the lockout fail — and leave the rest blank. That is not a DFA, and in a security context a blank transition is undefined behavior an attacker can probe. The fix is exactly §35.2's prescription: a single explicit dead state absorbs every illegal event, and every state (including $\text{Dead}$) has all four arrows. A quick audit: $5$ states $\times$ $4$ symbols $= 20$ cells, and the table above has all $20$ filled — the count must be exact (it is the handshaking-style edge count of §35.2's Spaced Review).

Phase 3: Encode it on the universal engine and trace

The whole point of the formal 5-tuple is that one driver runs every DFA (§35.2). Encode the table as a delta dict and reuse run_dfa unchanged:

# Login-policy DFA. States: Out0 (start, accept), Out1, In, Lock all accept; Dead rejects.
S = ('login', 'logout', 'fail', 'reset')
delta = {
    ('Out0','login'):'In',   ('Out0','logout'):'Dead', ('Out0','fail'):'Out1', ('Out0','reset'):'Dead',
    ('Out1','login'):'In',   ('Out1','logout'):'Dead', ('Out1','fail'):'Lock', ('Out1','reset'):'Dead',
    ('In','login'):'Dead',   ('In','logout'):'Out0',   ('In','fail'):'Dead',   ('In','reset'):'Dead',
    ('Lock','login'):'Dead', ('Lock','logout'):'Dead', ('Lock','fail'):'Dead', ('Lock','reset'):'Out0',
    ('Dead','login'):'Dead', ('Dead','logout'):'Dead', ('Dead','fail'):'Dead', ('Dead','reset'):'Dead',
}
start, accept = 'Out0', {'Out0','Out1','In','Lock'}

def run_dfa(delta, start, accept, events):     # the §35.2 engine, verbatim
    state = start
    for ev in events:
        state = delta[(state, ev)]
    return state in accept

valid_log   = ['fail','login','logout']            # one fail, then a clean session
invalid_log = ['login','login']                    # logging in while already logged in
locked_log  = ['fail','fail','reset','login']      # lock, admin reset, then login
print(run_dfa(delta, start, accept, valid_log))
print(run_dfa(delta, start, accept, invalid_log))
print(run_dfa(delta, start, accept, locked_log))
# Expected output:
# True
# False
# True

Hand-trace each to confirm the build matches the policy — the trace-don't-trust habit of §35.2:

  • valid_log = [fail, login, logout]: $\text{Out}_0 \xrightarrow{\text{fail}} \text{Out}_1 \xrightarrow{\text{login}} \text{In} \xrightarrow{\text{logout}} \text{Out}_0$. Ends in $\text{Out}_0$ (accept) → True. One failed attempt, then a normal login and logout: legal.
  • invalid_log = [login, login]: $\text{Out}_0 \xrightarrow{\text{login}} \text{In} \xrightarrow{\text{login}} \text{Dead}$. Ends in $\text{Dead}$ (reject) → False. The second login while already in $\text{In}$ is illegal (policy 4), and the trap is sticky.
  • locked_log = [fail, fail, reset, login]: $\text{Out}_0 \xrightarrow{\text{fail}} \text{Out}_1 \xrightarrow{\text{fail}} \text{Lock} \xrightarrow{\text{reset}} \text{Out}_0 \xrightarrow{\text{login}} \text{In}$. Ends in $\text{In}$ (accept) → True. Two fails lock it, an admin reset clears it, then a clean login: every step legal.

🔗 Connection: This is the same run_dfa engine that ran the parity machine and the "ends in 01" machine in §35.2 — and it will reappear in the Project Checkpoint's DFA class. One interpreter, infinitely many machines: the abstraction (Theme 3) is that the 5-tuple is just data, so a login validator and a binary-parity checker share an engine.

Why totality is a security property, not a formality

It is tempting to treat the §35.2 rule "$\delta$ must be total" as bookkeeping. In a security model it is the opposite — it is the whole point. An undefined transition is, in a real authentication system, undefined behavior: what does the session layer do when it receives a reset while logged in, an event the designers never drew an arrow for? Maybe it crashes; maybe it silently ignores the event and leaves the session in a state the policy never sanctioned; maybe an attacker who can inject events probes exactly those gaps to reach In without ever sending a valid login. The dead state $\text{Dead}$ closes every such gap: every (state, event) pair has a defined verdict, and every illegal pairing routes to a non-accepting trap from which there is no escape. The automaton's completeness is the proof that no event sequence, however adversarial, reaches an accepting state except along a policy-compliant path.

This is why we audited the cell count in Phase 2: $5$ states $\times$ $4$ events $= 20$ transitions, all filled. That count is exact, not a target — it is the directed-graph edge count of §35.2's Spaced Review, and a table with $19$ entries has a hole. The discipline transfers directly: when you model any protocol or session layer as an automaton, "is $\delta$ total?" is the same question as "have I specified what happens for every event in every state?" — and in security, the unspecified case is the vulnerability.

💡 Intuition: The set of valid logs is a regular language $L_{\text{valid}} = L(\text{login DFA})$; the set of suspicious logs we want to flag is its complement $\overline{L_{\text{valid}}}$ — every sequence that took at least one illegal step. Because regular languages are closed under complement (§35.2: just swap $F$ and $Q\setminus F$, the construction of Exercise 35.8), "flag the bad logs" is not a separate algorithm — it is the same automaton with $\text{Dead}$ as its only accepting state. Validation and intrusion-flagging are two readings of one machine.

Phase 4: Package it as a reusable LoginDFA for the Toolkit

The §35.2 Project Checkpoint added a DFA class to dmtoolkit/automata.py. Our validator is just an instance of it, which means we get accepts and recognize for free — and a clean place to express "flag the invalid logs in this batch":

from dmtoolkit.automata import DFA          # the class from §35.2's Project Checkpoint

login_dfa = DFA(
    states={'Out0','Out1','In','Lock','Dead'},
    alphabet={'login','logout','fail','reset'},
    delta=delta,                            # the dict built in Phase 3
    start='Out0',
    accept={'Out0','Out1','In','Lock'},
)

batch = [
    ['login','logout'],                     # valid
    ['fail','fail','login'],                # invalid: login from Lock
    ['fail','login','logout','login'],      # valid
]
invalid = [log for log in batch if not login_dfa.accepts(log)]
print(login_dfa.accepts(['login','logout']))
print(invalid)
# Expected output:
# True
# [['fail', 'fail', 'login']]

Hand-derive the batch result. ['login','logout']: $\text{Out}_0\xrightarrow{\text{login}}\text{In}\xrightarrow{\text{logout}}\text{Out}_0$ → accept. ['fail','fail','login']: $\text{Out}_0\xrightarrow{\text{fail}}\text{Out}_1\xrightarrow{\text{fail}}\text{Lock} \xrightarrow{\text{login}}\text{Dead}$ → reject (from $\text{Lock}$ only reset is legal). So this is the one flagged log. ['fail','login','logout','login']: $\text{Out}_0\xrightarrow{\text{fail}}\text{Out}_1\xrightarrow{\text{login}}\text{In} \xrightarrow{\text{logout}}\text{Out}_0\xrightarrow{\text{login}}\text{In}$ → accept. Hence invalid contains exactly the middle log, matching the printed list.

🧩 Productive Struggle: Before reading Phase 5, try this on paper. The security team adds a rule: "raise a soft alarm if there is ever a login immediately followed (some time later) by a fail in the same logged-in session" — a pattern-detection rule layered on top of validity. Sketch how you might guess the moment the suspicious login occurs. If "guess a position, then verify" feels like the §35.3 third-from-last example, you have found the reason the next phase needs an NFA.

Phase 5: A nondeterministic alarm rule, then determinize it

Some rules are most naturally written with a guess. Consider a monitoring overlay (separate from the validity DFA) over the simplified alphabet $\Sigma' = \{\texttt{login}, \texttt{fail}, \texttt{other}\}$ that should alarm on any session log containing the contiguous pattern login fail — a failed attempt right after a success, a possible hijack signal. "Contains login fail somewhere" is the textbook case for an NFA (§35.3): guess where the pattern starts, verify the two symbols, then accept regardless of the rest.

The NFA. Three states: $r_0$ (scanning, "haven't started the match"), $r_1$ ("just guessed a login begins the pattern"), $r_2$ (accept, "saw login then fail"). State $r_0$ loops on everything (skip), but on login also branches to $r_1$ (the guess); from $r_1$ a fail confirms the pattern → $r_2$; and $r_2$ loops on everything (the rest of the log does not matter).

$\delta$ (NFA) login fail other
$\to r_0$ $\{r_0, r_1\}$ $\{r_0\}$ $\{r_0\}$
$r_1$ $\emptyset$ $\{r_2\}$ $\emptyset$
$r_2$ (accept) $\{r_2\}$ $\{r_2\}$ $\{r_2\}$

The two hallmarks of nondeterminism from §35.3 are both here: $r_0$ on login returns two states (skip or start the match), and $r_1$ returns the empty set on login/other (a dead branch — that guess was wrong). Real hardware cannot "guess," so to deploy this we determinize it with the subset construction (§35.3): the DFA's states are sets of NFA states, and we track the set the NFA could be in.

Build the reachable subsets from the start set $\{r_0\}$, applying $\delta_M(S, a) = \bigcup_{q\in S}\delta_N(q, a)$:

  • From $\{r_0\}$: on login $\to \{r_0, r_1\}$; on fail $\to \{r_0\}$; on other $\to \{r_0\}$.
  • From $\{r_0, r_1\}$: on login $\to \{r_0,r_1\}\cup\emptyset = \{r_0, r_1\}$; on fail $\to {r_0}\cup{r_2} = {r_0, r_2}$; on `other` $\to {r_0}$.
  • From $\{r_0, r_2\}$: on login $\to \{r_0,r_1\}\cup\{r_2\} = \{r_0,r_1,r_2\}$; on fail $\to {r_0,r_2}$; on `other` $\to {r_0,r_2}$.
  • From $\{r_0, r_1, r_2\}$: on login $\to \{r_0,r_1,r_2\}$; on fail $\to \{r_0,r_2\}$; on other $\to {r_0, r_2}$.

A subset is accepting iff it contains the NFA-accepting state $r_2$ (§35.3: $F' = {S \mid S\cap F\neq\emptyset}$) — so ${r_0,r_2}$ and ${r_0,r_1,r_2}$ accept. Four reachable subsets become four DFA states; rename them $D_0=\{r_0\}$, $D_1=\{r_0,r_1\}$, $D_2=\{r_0,r_2\}$ (accept), $D_3=\{r_0,r_1,r_2\}$ (accept):

# Determinized alarm DFA (from the subset construction). D2, D3 are accepting (contain r2).
dD = {
    ('D0','login'):'D1', ('D0','fail'):'D0', ('D0','other'):'D0',
    ('D1','login'):'D1', ('D1','fail'):'D2', ('D1','other'):'D0',
    ('D2','login'):'D3', ('D2','fail'):'D2', ('D2','other'):'D2',
    ('D3','login'):'D3', ('D3','fail'):'D2', ('D3','other'):'D2',
}
alarm = DFA(states={'D0','D1','D2','D3'}, alphabet={'login','fail','other'},
            delta=dD, start='D0', accept={'D2','D3'})

print(alarm.accepts(['login','fail']))                 # the bare pattern
print(alarm.accepts(['login','other','fail']))         # login, gap, fail -> no contiguous match
print(alarm.accepts(['other','login','fail','login'])) # pattern occurs mid-log
# Expected output:
# True
# False
# True

Hand-trace on the determinized machine — each step is one set-union from the construction:

  • [login, fail]: $D_0\xrightarrow{\text{login}}D_1\xrightarrow{\text{fail}}D_2$. $D_2$ accepts → True. The contiguous login fail is present.
  • [login, other, fail]: $D_0\xrightarrow{\text{login}}D_1\xrightarrow{\text{other}}D_0 \xrightarrow{\text{fail}}D_0$. $D_0$ rejects → False. The other between them breaks the contiguous pattern — the wrong guess ($r_1$) died, exactly the empty-set branch made deterministic.
  • [other, login, fail, login]: $D_0\xrightarrow{\text{other}}D_0\xrightarrow{\text{login}}D_1 \xrightarrow{\text{fail}}D_2\xrightarrow{\text{login}}D_3$. $D_3$ accepts → True. Once the pattern is seen we stay accepting forever (both $D_2$ and $D_3$ accept), matching "contains the pattern."

🚪 Threshold Concept. We just compiled away a guess. The NFA's "pick the right starting point" — a superpower no physical machine has — became a deterministic, four-state, one-pass DFA by the single idea of tracking the set of states the NFA could be in (§35.3). Nondeterminism gave us a clearer spec (3 states, easy to read) but no extra power; determinization gave us something runnable. That "expressiveness without extra power" is the same theme that, scaled up to polynomial time, becomes the P-versus-NP question (Chapter 37) — and the proof technique here, "track the reachable set," is why we can reason about nondeterminism at all.

Discussion Questions

  1. In Phase 2 we split "logged out" into $\text{Out}_0$ and $\text{Out}_1$ but kept a single $\text{In}$. Suppose the policy changes to "lock after three consecutive fails." How many logged-out states do you now need, and what does each remember? Generalize to "lock after $k$ fails."
  2. The validity DFA's $\delta$ has exactly $5 \times 4 = 20$ transitions. Explain, via the §35.2 Spaced Review's edge-counting, why this number is exact and not merely an upper bound — and why a missing entry would be a security defect rather than a stylistic one.
  3. The alarm rule "contains login fail" is regular. Is the rule "the number of logins equals the number of logouts in the log" regular? Argue informally (no full proof) by analogy with $\{0^{n}1^{n}\}$ and the pumping lemma (§35.5).
  4. Determinizing the 3-state alarm NFA produced a 4-state DFA. The subset construction's worst case is $2^{3} = 8$ states. Why did we get only $4$? What happened to the other $4$ subsets (e.g. $\{r_1\}$, $\{r_1, r_2\}$)?
  5. We ran the validity DFA and the alarm DFA separately. Sketch how the product construction (Exercise 35.31) would let a single machine track both — validity and the alarm pattern — in one pass. What would its state set be, in terms of the two machines' state sets?

Your Turn: Extensions

  • Option A (extend the policy). Add an event mfa (multi-factor challenge) with the rule "after a login, the session is pending until an mfa; only mfa or logout is valid while pending." Add the state(s), redraw the table keeping $\delta$ total, and re-trace the three logs from Phase 3.
  • Option B (build the NFA, then determinize, in code). Encode the alarm NFA as a dN dict and run it with the nfa_accepts driver from §35.3 on the three Phase-5 test logs. Confirm it agrees with the determinized alarm DFA on all three — a concrete check that the subset construction preserved the language (Theme 4: test what the proof guarantees).
  • Option C (complement = "flag the invalid"). Instead of collecting rejects with a list comprehension, build the complement of the validity DFA (swap accepting and non-accepting states, §35.2 / Exercise 35.8) so that the new machine accepts exactly the invalid logs. Verify it accepts ['login','login'] and rejects ['login','logout'].
  • Option D (minimize by hand). Two of the alarm DFA's states might be merge-able. Using the equivalence-relation idea of §35.2's Spaced Review (two strings are equivalent if they drive the machine to the same state), argue whether $D_2$ and $D_3$ can be merged. (Hint: do they ever differ in acceptance on any future input?)

Key Takeaways

  1. A policy is a language; a validator is a DFA. Reading "valid sequence of events" as a language over an event alphabet (§35.1) turns a security spec directly into a machine you can build and audit.
  2. A total $\delta$ with a dead state is the build discipline. Every state needs an arrow for every symbol (§35.2); the trap absorbs illegal events. In security, a missing transition is a hole, not a detail — and the cell count must come out exact.
  3. One engine runs every machine. The validity checker, the parity machine, and the alarm detector all ride the same run_dfa / DFA abstraction (§35.2, Project Checkpoint) — the 5-tuple is just data (Theme 3).
  4. Nondeterminism is a design convenience you can compile away. The "guess where the pattern starts" alarm NFA (3 readable states) became a runnable 4-state DFA by the subset construction (§35.3) — clearer spec, same power, deployable result.