The Gap Between Tamarin and Implementation: Recording Correspondence

What moment in the implementation does Accepted mean?

A Tamarin lemma says that every accepted capability was previously issued by an authority. Months later, a developer asks where Accepted occurs in the Rust implementation. Is it successful signature verification, a database update, completion of a business action, or an audit record?

Action facts label rule transitions in a Tamarin trace. Lemmas describe those observations, so the moment an event denotes determines the meaning of the property. A familiar event name is insufficient. [1][3]

Following Formal Verification in the Development Loop, this article connects messages, state, actions and assumptions to implementation, tests and operations through a correspondence manifest.

The example bundle contains two theories, a Rust encoding example, SQL transaction templates, a manifest and review obligations. Tamarin parsing/proving, Rust builds/tests, SQL execution, cryptographic integration, concurrency and recovery exercises were not executed. All remain NOT_RUN. These are design examples and proposed obligations, with no claim of successful verification or production adoption.

1. Separate a model proof from its application to code

Tamarin analyzes symbolic messages and multiset rewriting rules. Cryptographic primitives are expressed through equational theories. One equation provided by signing is: [2]

verify(sign(m, sk), m, pk(sk)) = true

This does not establish the correctness of a signature library, parser, side-channel defenses or key management. The selected model and equational theory bound the analysis, and proof search is not guaranteed to terminate in general. [1]

Applying a result requires an account of how implementation behavior maps to model observations. A formal refinement proof would justify that abstraction of implementation traces. The manifest and review plan here make the correspondence inspectable; they do not themselves prove refinement.

A rule may correspond to several functions. Internal implementation steps need not each produce a model event. However, intermediate state that an attacker can observe or influence may invalidate the abstraction of several operations as one atomic step.

2. Separate signature origin from one-time consumption

The illustrative capability signs its version, key-generation identifier kid, receiving service S, subject, resource, action and nonce:

cap = <'cap-v1', kid, S, U, R, Act, nonce>

The bundle separates two theories. capability-auth.spthy models stateless signature validation; capability-once.spthy adds an issuance ledger and one-time consumption.

A signature can be validated repeatedly. Calling that event Validated keeps it distinct from one-time acceptance. A key-compromise exception also needs an actual rule that can reveal the key:

rule RevealAuthorityKey:
  [ !AuthorityKey(kid, sk) ]
  --[ KeyReveal(kid) ]-> [ Out(sk) ]

lemma validated_requires_issuance:
  "All kid S cap #i. Validated(kid,S,cap) @i ==>
     ((Ex #j. Issued(kid,S,cap) @j & j < i)
      | (Ex #r. KeyReveal(kid) @r & r < i))"

In the stateful theory, only issuance creates Unused, and consumption removes it. Consequently, prior issuance follows from ledger provenance as well. That ordering could remain true even if signature checking were removed. The ledger lemma alone therefore cannot serve as independent evidence of signature security.

Both theories contain an exists-trace obligation for normal issuance followed by validation or acceptance. The authentication theory also asks for a trace with repeated validation. These help detect a vacuous safety implication in a model where acceptance is impossible. They remain unexecuted obligations. [4][5]

3. Give each action fact a commit point

The stateful consumption rule and replay lemma are shown below. The full theory also includes key and service registration, issuance, key reveal and the equality restriction.

rule ConsumeCapability:
  let cap = <'cap-v1', kid, S, U, R, Act, nonce>
  in
  [ !AuthorityPk(kid, pkA), !Service(S), Unused(kid, S, cap)
  , In(<cap, sig>) ]
  --[ Eq(verify(sig, cap, pkA), true), Accepted(kid, S, cap) ]-> []

lemma capability_cannot_be_replayed:
  "All kid S cap #i #j.
     Accepted(kid,S,cap) @i & Accepted(kid,S,cap) @j ==> i = j"

We map Accepted to the logical commit of the transaction that consumes unused state. A SQL statement returning or an audit log being written is not that point.

The issuance rule combines ledger creation and publication of the signed message. An implementation may prepare a signature, commit the transaction, and then publish the token. Exposing the signature before commit would break this correspondence.

A tracing::info!("accepted") line can help observe the commit, but log loss, sampling or relocation must not define domain semantics. Define the domain event first, then map telemetry to it.

4. Keep a correspondence manifest between model and code

A theory comment is hard to discover from implementation code. A Rust comment saying “See model” does not identify the assumptions. Keep a separate manifest and reference its claim IDs from both sides.

formal/
  capability-auth.spthy
  capability-once.spthy
  correspondence.json
  claims/CAP-REPLAY-001.md
src/encoding.rs
sql/schema.sql
sql/issue.sql
sql/consume.sql
review/correspondence-cases.csv

The acceptance mapping in the supplied manifest is:

{
  "fact": "Accepted(kid,S,cap)",
  "claim": "CAP-REPLAY-001",
  "source": "sql/consume.sql",
  "commit_point": "conditional consume and outbox insert commit together",
  "not_included": [
    "signature validation alone",
    "HTTP response delivery",
    "external business action completion"
  ],
  "integration_status": "PROPOSED_NOT_IMPLEMENTED",
  "execution_status": "NOT_RUN"
}

Distinguish concrete source artifacts from proposed integration. This bundle supplies no database driver, signature library, HTTP handler or outbox dispatcher. An imaginary CapabilityService::consume must not be recorded as an existing implementation symbol.

Record owners, model and implementation revisions, and correspondence-review dates when known. Unassigned ownership remains unassigned. The existence of a manifest does not establish operational responsibility or completed review.

5. Follow a message term all the way to signed bytes

A symbolic tuple has clear field boundaries. Implementation must agree on the bytes being signed, the values being decoded and the values used for authorization. The example uses a deliberately small, fixed 88-byte format:

The Rust decode function checks the exact length, tag and action; trailing bytes are rejected. This is an illustrative codec, not a verified-capability type or authorization library. The mapping also records that implementation actions refine the symbolic Act to two variants.

Canonical encoding is useful, but it is not a universal prerequisite. A protocol may verify the exact immutable wire bytes, decode them unambiguously once, and use that decoded value consistently. If verification reserializes the payload, field ordering, numbers, Unicode and other encoding rules must agree.

The security requirement is to avoid attacker-useful alternate interpretations. Include version, audience and key ID in the signed payload. Select a trusted (audience, kid) and algorithm profile; do not trust an arbitrary public key supplied with a message.

fixtures/encoding-v1.json contains candidate expected bytes derived from the format. It is neither measured Rust output nor a cryptographic signature vector. Adoption requires independently reviewed encoding vectors and separate signature vectors for the selected cryptographic implementation.

6. Map linear facts to atomic durable state

Tamarin consumes linear facts and retains persistent facts. State is a multiset: naming a fact Unused does not make it unique. One-time consumption also depends on unique nonce creation, no cloning and no rule that recreates consumed state. [3]

The schema uses (key_id, audience, nonce) as its primary key and requires an immutable payload. A nonce collision must fail insertion rather than overwrite an existing row. Tamarin fresh names idealize a finite random space and a real CSPRNG; collision handling is a separate obligation.

The core consumption operation conditionally updates the row matching the verified payload:

BEGIN;
WITH consumed AS (
    UPDATE capabilities
    SET consumed_at = transaction_timestamp(), consume_request_id = $5
    WHERE key_id = $1 AND audience = $2 AND nonce = $3
      AND payload = $4 AND consumed_at IS NULL
    RETURNING key_id, audience, nonce, payload
)
INSERT INTO capability_outbox (event_id, event_kind, key_id, audience, nonce, payload)
SELECT $5, 'capability.consumed', key_id, audience, nonce, payload FROM consumed
RETURNING event_id;
COMMIT;

Under PostgreSQL Read Committed, a competing UPDATE waits for an earlier transaction and reevaluates its WHERE condition on the updated row. That behavior supports this conditional-consumption design. A SELECT followed by an unconditional UPDATE does not support the same argument. [6][7]

One row from RETURNING does not establish that the enclosing transaction committed. A new acceptance requires a successful commit including the outbox insertion. Zero rows also does not uniquely diagnose replay: an unknown capability or mismatched payload can produce the same result. [8]

The SQL templates do not themselves enforce immutable payloads, prohibit administrative resets, configure database roles, or establish durability and failover behavior. Those implementation and operational obligations remain necessary for correspondence.

7. Separate commit, response and external action

A transaction can commit while its response is lost. A caller timeout does not establish rollback; the outcome is unknown. Use a stable request ID to reconcile against the authoritative database and recover the same acceptance receipt. Returning an existing receipt is not a second Accepted event.

Persisting domain events in the same transaction through an outbox can avoid exposing an event for a rolled-back change. Outbox delivery may still be duplicated. Downstream idempotency or business updates within the same transaction require separate design.

One-time consumption does not establish exactly-once execution of an external business action. Failure after consumption can leave zero completed actions; a retry can cause duplicates. If the business claim includes completion, introduce the additional state and events needed to describe it.

8. Map restrictions, cryptography and channel assumptions

The equality restriction permits traces containing Eq(x,y) only when x=y. In implementation, this corresponds to proceeding only after signature verification succeeds. Adding a restriction as an “obvious condition” can silently remove attacks that the real implementation permits. [4][5]

The signing theory is not verification of Ed25519 or a particular library. Record algorithm, library version, dependency review, key storage and API permissions separately. The bundle cites RFC 8032 Ed25519 as a candidate profile; it selects and runs no cryptographic library or integration. [10]

In and Out expose messages to a network attacker able to obtain, construct and replay messages. Using mTLS does not provide reliable or exactly-once delivery. If a model hides a channel from the attacker, distinguish its confidentiality, peer-authentication and delivery assumptions.

KeyReveal abstracts disclosure of key material. Real compromise rarely has a perfectly observable timestamp. Revocation is not disclosure, and unauthorized use of a KMS signing API is not necessarily key extraction. A signing-oracle capability may need its own model. The absence of monitoring alerts does not prove absence of compromise.

9. Include crashes, restore and clocks in the mapping

Surviving a process restart differs from never reverting across failover or backup restoration. PostgreSQL durability depends on WAL and synchronous-commit settings; replica guarantees also depend on configuration. Writing COMMIT in a template does not establish persistence under every failure. [9]

Restoring yesterday’s backup can make a consumed row unused again. The supplied theory has no rollback rule, so this trace is outside its analysis. Recovery may require rejecting an earlier token epoch, reconciling an independent consumption ledger or invalidating outstanding tokens.

Key rotation alone is insufficient if old verification keys remain trusted. A short TTL only bounds the exposure period. State when acceptance may safely resume in the recovery procedure.

Expiry is absent from the sample. If introduced, remember that Tamarin’s #i < #j denotes trace ordering, not UTC comparison. Define validity, permitted skew, clock source and the interval between checking and committing. Natural numbers alone do not provide correspondence with a deployed clock.

10. Distinguish correspondence tests from operational evidence

Correspondence tests do not reproduce universal trace exploration. They check whether implementation preserves model observations and assumptions.

The supplied CSV is a NOT_RUN review plan, not an executed test suite. Future runs should identify inputs, revisions, environment, raw evidence and outcomes.

Linking runtime issuance and consumption events to claim IDs helps describe incidents using model vocabulary. A finite log is not proof of a universal property. Account for missing, duplicated and reordered delivery. A replay-rejection metric cannot by itself establish replay resistance.

11. Track change and evidence through claim IDs

A claim ID can connect model, implementation, tests and operations even when different teams own them.

Keep formal execution status, implementation-correspondence review, deployed revision and operational-assumption checks separate. A passing model commit does not establish applicability to current production. Identify the reviewed source, including any uncommitted changes.

Changes to signed fields, key selection, consumption atomicity, expiry or recovery should trigger correspondence review. A proposal to replace database state with stateless tokens removes the implementation counterpart of Unused; the replay claim must be reconsidered.

CI can check manifest syntax, claim IDs and the existence of referenced files or symbols. A function’s existence does not establish that it represents the correct commit point. The bundle implements no CI or reference validator. Assign ownership for semantic review that mechanical checks cannot close.

12. Connect proofs to production assurance

The model need not reproduce every function and table. Abstract the security-relevant semantics and record the evidence supporting each abstraction.

Here, those semantics include signed fields, trusted authority and audience, current unused state, atomic consumption, and assumptions about compromise and recovery. Similar function names matter less than explaining how implementation preserves these meanings.

Which commit is Accepted? Which state is Unused? What happens when restoration rolls it back? Keep those answers reachable through the correspondence manifest and claim record. Maintain the evidence that explains the mapping, and the formal model can remain part of the development loop as implementation evolves.

The related authentication and authorization PoC provides attributed design context. This capability model, codec, SQL and unexecuted review plan are not presented as evidence from that engagement.

References

Tamarin manual sources are pinned to the revision below. This is a documentation baseline, not an installed toolchain or proof-execution version. Database references use PostgreSQL 18 documentation; the cryptographic reference is RFC 8032.

1. Tamarin: Introduction
2. Tamarin: Cryptographic Messages
3. Tamarin: Protocol Specification Using Rules
4. Tamarin: Property Specification
5. Tamarin: Modeling Issues
6. PostgreSQL: UPDATE
7. PostgreSQL: Transaction Isolation
8. PostgreSQL: COMMIT
9. PostgreSQL: Write Ahead Log Configuration
10. RFC 8032: Edwards-Curve Digital Signature Algorithm