Attack Nets, Concurrency, and the State-Space Explosion

Attack trees and attack graphs both describe an attack as a completed sequence: the tree asserts that a set of steps suffices, the graph asserts that a set of facts is reachable. Neither represents partial progress, and neither represents two attacker actions in flight at once. Both gaps matter for a specific class of attack, the one where the adversary exploits the system’s own concurrency: a check and a use separated by a window, a lock held across a slow operation, a race between two requests that each individually respect every rule.

Representing that requires a model with state, and the standard formal tool for state with concurrency is the Petri net. Both structures it replaces, the attack tree and the attack graph, assume that a step only establishes a fact and never consumes a resource. An attack net is a Petri net whose places hold tokens representing the attacker’s progress, transitions represent actions, and a transition fires only when every input place holds a token. The firing consumes those tokens and produces tokens in the output places, which is what makes the model capable of expressing a step that consumes a resource rather than merely establishing a fact.

The firing rule and what it buys

A Petri net is a bipartite graph of places and transitions with a marking that assigns a non-negative integer to each place. A transition is enabled when each of its input places holds at least as many tokens as the arc weight requires; firing removes those tokens and adds tokens to its output places. That is the whole semantics, and three properties follow immediately.

Consumption is expressible. A one-time password is a place with one token; the transition that uses it consumes the token, so a second attempt cannot fire unless another token is produced. This is the property that monotone attack graphs cannot represent, and it is the reason a graph model will happily report that an attack succeeds twice with a single credential.

Parallelism is expressible. Two tokens in the same place enable two firings of the same transition concurrently, and two independent branches proceed without interfering. Whether they interfere is a property of the net: a shared place with limited tokens is a shared resource, and contention for it is exactly the structure that produces race conditions in the modeled system.

Nondeterminism is expressible. When several transitions are enabled, any may fire, and the analysis must consider all interleavings. That is the source of both the model’s fidelity and its cost.

The standard analysis computes the reachability graph: nodes are markings, edges are firings, and the graph is generated by exploring from the initial marking until no new marking appears. A marking that places a token in the goal place is a successful attack, and the path to it is a concrete interleaving of attacker actions.

from collections import deque

def reachable_markings(transitions, initial, max_states=200000):
    """transitions: (input_places, output_places), each a tuple of place indices."""
    start = tuple(initial)
    seen, queue = {start}, deque([start])
    while queue:
        m = queue.popleft()
        for ins, outs in transitions:
            # Enabled only if each input place holds enough tokens for every arc.
            if all(m[i] >= ins.count(i) for i in set(ins)):
                nxt = list(m)
                for i in ins:
                    nxt[i] -= 1                      # firing consumes its inputs
                for i in outs:
                    nxt[i] += 1
                nxt = tuple(nxt)
                if nxt not in seen:
                    if len(seen) >= max_states:
                        return seen, True            # truncated: state space too large
                    seen.add(nxt)
                    queue.append(nxt)
    return seen, False

The max_states parameter is not defensive coding; it is a necessary admission. The number of markings for a net with $n$ places and a fixed total of $k$ tokens is the number of ways to distribute them, $\binom{n+k-1}{k}$, and the reachable subset is frequently a large fraction of that. Allowing the token count to grow removes the bound entirely, which is why capacity limits are usually imposed before analysis. Adding places and tokens multiplies rather than adds, which is why the state space of a modest net reaches millions of markings.

Where the explosion comes from

Three mechanisms drive the growth, and distinguishing them matters because each has a different reduction.

Interleaving of independent actions produces a factorial factor. If $m$ independent transitions are enabled at a marking, the reachability graph contains $m!$ distinct paths that permute them, all of which reach the same marking. The markings are the same, so the marking graph does not duplicate them; the paths do. This distinction is what makes partial-order reduction effective: two firings that touch disjoint place sets commute, so the analysis may explore one order and ignore the other without losing any reachable marking.

Concurrency of dependent actions produces genuine state. Two attacker branches that contend for a shared token interleave in ways that produce distinct markings, and no reduction collapses them because the markings differ. This is the part of the state space that carries real information, and it is the part that the model exists to capture.

Unbounded place capacity produces infinity. A place with no capacity bound allows an unbounded token count, and the reachability set becomes infinite. Real attacks are bounded by the attacker’s budget, so the standard fix is to bound every place by the maximum number of tokens the attacker could plausibly accumulate, which converts an infinite problem into a finite one at the cost of an assumption that must be stated.

Reductions that preserve the answer

The reductions worth applying are the ones with a proof, not the ones that merely make the graph smaller.

Partial-order reduction is the most valuable. The correctness condition is that the reduced exploration preserves the set of reachable markings, which holds when the reduction respects a stubborn-set or ample-set condition: for each explored marking, the chosen subset of transitions is sufficient to represent every equivalence class of interleavings. The practical effect on a net with $m$ independent attacker steps is a reduction from factorial to linear in the number of orderings explored, while the marking set stays identical.

Symmetry reduction applies when the net has interchangeable components. Ten identical worker processes produce states that differ only in which worker holds which token, and the analysis can quotient by the permutation group. The gain is proportional to the size of the group, which for $w$ workers is $w!$, so the reduction is substantial for large $w$ and the modeling cost is proving the symmetry, which requires that no transition distinguishes the workers.

Abstraction applies when a subsystem’s internal states are irrelevant to the goal. Replacing a detailed authentication flow with a single transition that either yields a session or does not collapses a large state space into a few states, and the correctness condition is that the abstraction is a simulation: every concrete behavior maps to an abstract behavior that preserves the property being checked. Where the property is reachability of a goal place, this holds whenever the abstraction does not add behaviors the concrete system lacks, which is a condition that must be checked per abstraction rather than assumed.

What the extra fidelity actually buys

The reason to pay the state-space cost is that a class of findings exists only in a state model. A time-of-check-to-time-of-use defect is not visible in a graph of facts, because the facts are both true; it is visible in a net, because the check consumes a token that the use assumes is still present. The same holds for double-spend patterns, for lock-free structures that are correct only under a specific memory ordering, and for authorization decisions made on a value that another request can change between the decision and the effect.

For those, the model’s value is not the numeric result but the structure it forces: the analyst must name the resource, the operation that consumes it, and the interleaving that violates the invariant. Naming those three is most of the finding, and the reachability analysis confirms that the interleaving is possible given the modeled capacities. Where the analysis is truncated by the state bound, the model has still produced the hypothesis, and the confirmation moves to a targeted test rather than an exhaustive search.

The limitation to state plainly is that the model’s fidelity is bounded by its place set, and every place is a decision the analyst made. A net that omits the token representing a cached authorization decision will not find the defect that depends on it, and no amount of analysis recovers the omission. That is the same limitation that applies to every representation in this family: the structure constrains what can be found, and the choice of structure is the analysis.