SpecMon Annotations

SpecMon extends Tamarin’s rule syntax with annotations that control how rules are processed during monitoring. These annotations let you align runtime events with symbolic terms without changing the core protocol logic.

How rules apply

SpecMon processes an incoming event stream and matches each event against rule annotations. In practice:

• Triggers define which concrete events can apply a rule and how return values are bound.
• Hints are a lookahead mechanism used by start rules to decide whether a rule is worth pursuing for the current event.
• Rules that contain function applications and have no trigger or hint are automatically decomposed into trigger- and hint-annotated rules.

If you add a trigger or hint yourself, SpecMon will use the rule as written and will not decompose it.

Triggers

A trigger specifies which event causes a rule to fire and how the return value is bound:

rule Encrypt [trigger=[<senc(~k, $m), c>]]:
  [ In($m), !Ltk(~k) ]
--[ Encrypted($m, c) ]->
  [ Out(senc(~k, $m)) ]

The trigger <senc(~k, $m), c> matches a runtime event where senc is called on ~k and $m, and binds the result to c. When the rule is applied, the function term senc(~k, $m) is replaced with its return value.

SpecMon also supports multiple triggers per rule. This is useful for modeling paired enter/leave events and rules that should only fire after all required calls have been seen.

The triggers of such a rule may arrive in any order. The first one that matches starts the rule and consumes its linear premises; persistent premises stay available. The conclusions, actions and restrictions apply when the last trigger arrives. An event that advances a started application does not start the same rule again, and equal started applications complete one at a time.

Hints

Hints are a lookahead mechanism used by start rules. They indicate which triggers the rule expects next, so the monitor can decide whether the rule is worth pursuing for the current event.

rule Send_Start [hint=[<h($m), hm>, <senc(~k, $m), c>]]:
  [ In($m), !Ltk(~k) ]
  -->
  [ ... ]

In practice, hints are generated automatically during decomposition. You typically only write them when you need a custom decomposition strategy.

Rule decomposition

Tamarin rules can contain nested function terms like h(senc(~k, $m)), but they do not specify the order in which these computations occur. Runtime traces do have an order, and the monitor needs to connect each observable call with the right symbolic term.

SpecMon handles this by decomposing rules that contain function applications. A rule without a trigger or hint is decomposed automatically into:

• A start rule annotated with hint (lookahead)
• One or more mid rules each annotated with a single trigger
• An end rule that completes the original conclusion (often with no trigger)

Two of these boundaries are fused when keeping them apart gains nothing. If the rule has premises and a single innermost computation, there is nothing to look ahead for: the start rule is left out, and the rule of that computation matches the premises of the original rule. A rule without premises keeps its start rule. If the conclusions and actions together have a single outermost computation, its rule and the end rule become one rule, triggered by that computation. A chain such as Out(f(g(x))) therefore becomes two rules. With an action that computes something else, such as --[ Log(h(x)) ]->, it stays split.

Generated state facts distinguish each use of a shared computation with an occurrence argument. Translation also rejects an exact generated fact name shared by different source-rule names. Rename one of the reported rules to remove the collision. This check does not reserve user-written state names or require unique source-rule names.

Example: decomposition and dependencies

Given the rule:

rule Send:
  [ In($m), !Ltk(~k) ] --> [ Out(h(senc(~k, $m)), h($m)) ]

Two computations can happen independently (h($m) and senc(~k, $m)), and h(senc(~k, $m)) depends on the encryption result. Decomposition makes those dependencies explicit with triggers like:

<h($m), hm>
<senc(~k, $m), c>
<h(c), hc>

Why hints matter

Because h($m) and senc(~k, $m) can occur in either order, the monitor would otherwise need to explore many interleavings. Hints let the monitor look ahead at the incoming event and choose the matching path, avoiding an exponential blowup in the number of rule variants.

Conclusions that no rule consumes

After role selection, and before decomposition, SpecMon drops each conclusion that no premise of the selected rules consumes, that is, no premise with the same fact name and number of arguments. This also happens with --decompose=false. A function call in a dropped conclusion stays as a Compute_(...) fact, so the call is still matched and evaluated. A fact whose name ends in _ is evaluated but never stored.

role — Filter rules by protocol role

The role attribute restricts rules to specific protocol participants:

rule ClientSend [role=client]:
  [ ClientState(x) ]
--[ Send(x) ]->
  [ Out(x) ]

rule ServerReceive [role=server]:
  [ In(x) ]
--[ Receive(x) ]->
  [ ServerState(x) ]

When running SpecMon with --role client, only rules with role=client (or no role attribute) are active.

Usage:

specmon monitor --role client protocol.spthy

Best practices

• Prefer automatic decomposition; it produces correct triggers and hints for nested terms.
• When writing manual triggers, ensure the function names and argument shapes match the runtime events you emit.
• Use hints when a rule has multiple independent computations to avoid ambiguous interleavings.
• Every variable of a rule must occur in a premise or in the trigger or hint that selects it. See Model Requirements for what SpecMon checks when it loads a model.

Next steps

• Creating Unified Models — Write specifications that work with both Tamarin and SpecMon
• Encoding Message Formats — Define concrete message formats
• Event Format — Understand the event stream structure