Tamarinモデルと実装の距離 — 対応関係をどこに残すか

Acceptedは，実装のどの瞬間か

Tamarinで「Capabilityが受理されたなら，先にAuthorityが発行している」というLemmaを書いた．数か月後，実装を読むDeveloperから「Acceptedは，どの瞬間ですか」と聞かれる．署名検証の成功なのか，Databaseの更新なのか，Business Actionの完了なのか．ここを説明できなければ，ModelとProduction Codeは別々に進化してしまいます．

Action Factは，TamarinのRule遷移に付けるTrace上の観測点です．Lemmaはその観測点について記述されるため，名前だけでなく何が成立した瞬間を表すかがPropertyの意味を決めます．[1][3]

本稿は形式検証を開発ループへに続く，Proof Engineeringの話です．Correspondence Manifestを中心に，Message，State，Action，前提を実装・テスト・運用へつなぎます．

サンプル一式には，二つのTheory，RustのEncoding例，SQL Transactionの雛形，対応表とReview項目を収録しています．TamarinのParse・Proof，RustのBuild・Test，SQL・署名・並行実行・復旧の検証は実行していません．すべてNOT_RUNです． 以下は設計と確認すべきObligationの説明であり，証明成功やProductionでの採用実績の報告ではありません．

1．モデルの証明と，実装への適用を分ける

Tamarinが解析するのは，Symbolic MessageとMultiset Rewriting RulesからなるModelです．暗号PrimitiveもEquational Theoryで表現されます．signingの代表的な式は次です．[2]

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

この式は，署名Libraryの実装，Parser，Side Channel，鍵管理の正しさを証明しません．解析の範囲は選んだModelとEquational Theoryで決まり，一般に探索の終了も保証されません．[1]

実装へ適用するには，Model上の観測を実装上の振る舞いへ対応させる説明が必要です．完全なRefinement Proofを行うなら，実装の振る舞いがどの抽象Traceへ写るかまで形式的に扱います．本稿のManifestとTest計画は，その対応をReview可能にするArtifactです．それだけでRefinementを証明したことにはしません．

一つのRuleに複数の関数が対応して構いません．内部処理の各Stepが毎回Model Eventになる必要もありません．ただし，Modelで一つのAtomic Stepとした途中に，攻撃者が観測・介入できる状態がないかは確認します．

2．署名の由来と，一回限りの消費を別モデルにする

説明用のCapabilityは，Version，鍵の世代を識別するkid，受理先Service S，Subject，Resource，Action，Nonceを署名対象にします．

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

サンプルは二つのTheoryに分けています．capability-auth.spthyは状態を持たない署名検証，capability-once.spthyは発行台帳と一回限りの消費です．

署名だけのModelでは，同じ正当なMessageを何度でも検証できます．Validatedを一回限りの受理と呼ばないことが大切です．また，鍵侵害の例外を書くなら，実際に侵害を発生させるRuleも必要です．

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))"

一方，状態付きModelでは発行RuleだけがUnusedを生成し，消費Ruleがそれを取り除きます．この構造では，発行の先行性は台帳の由来からも導かれます．署名検証を外しても同じ先行性が残り得るため，このLemmaだけを署名の安全性のEvidenceにしてはいけません．

各Theoryには正常な発行・検証／受理のTraceを求めるexists-trace Lemmaも含めます．署名だけのTheoryには再検証が可能なTraceのObligationを置きます．安全性の含意が，そもそも受理不能なModelで空虚に成立していないかを別に確認するためです．これらも未実行です．[4][5]

3．Action FactにCommit Pointを与える

状態付きModelの消費RuleとReplay Lemmaは次です．完全なTheoryには鍵・Service登録，発行，鍵侵害，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"

Acceptedは，未消費状態を消費するTransactionがCommitした論理的な瞬間に対応させます．SQLの実行が返った瞬間や，Audit Logの出力位置ではありません．

Modelの発行Ruleは署名付きMessageの公開と台帳生成を一つのStepにしています．実装では署名を準備し，TransactionをCommitしてからTokenを公開します．途中で生成された署名をCommit前に外部へ渡すと，この対応が崩れます．

tracing::info!("accepted")は，このCommitを観測する補助情報にはなります．しかしLogの欠落，Sampling，位置変更がDomainの意味を変えてはいけません．Domain Eventを先に定義し，LogやTelemetryをそこへ結び付けます．

4．Correspondence Manifestを中間Artifactにする

Theoryのコメントだけでは実装から見つけにくく，Rustの「See model」だけでは前提を追えません．対応関係を独立したManifestに置き，CodeとTheoryにはClaim IDとその参照を残します．

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

サンプルのManifestから，受理の対応を抜き出します．

{
  "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"
}

既存のCodeと，まだ実装していない連携処理は分けて記録します．このサンプルにはDB Driver，署名Library，HTTP Handler，Outbox Dispatcherがありません．存在しないCapabilityService::consumeを実装済みの参照先として書くことは避けます．

Owner，Model版，実装版，対応Reviewの日時も記録できるようにします．未割当は未割当のまま残します．Manifestがあるだけで，運用責任やReview完了を推定しません．

5．Message Termを署名対象のBytesまで追う

Symbolic TupleにはField境界があります．実装では，何を署名し，何をDecodeし，どの値を認可へ使うかを一致させます．サンプルは説明を小さくするため，次の88 Bytes固定形式を採用しています．

Rust例のdecodeは，長さ，Tag，Actionを確認します．余分なBytesも受理しません．これは説明用Codecであり，署名検証済み型や認可処理を提供するLibraryではありません．SymbolicなActを実装では二つのVariantへ具体化することも対応表に残します．

Canonical Encodingは有力な方法ですが，すべてのProtocolで必須とは限りません．受信した不変のBytesそのものを検証し，曖昧さなく一度Decodeし，その結果を後続処理に使う方式もあります．再Serializationして検証する場合は，Field順序，数値，Unicode等の規則が一致する必要があります．

重要なのは，攻撃者に都合のよい別の解釈が生じないことです．Version，Audience，Key IDも署名対象へ含め，受信Messageが指定する任意の公開鍵をそのまま信頼しないようにします．実装は信頼済みの(audience, kid)とAlgorithm Profileを選びます．

fixtures/encoding-v1.jsonは仕様から作った期待Bytesの候補です．Rustの出力を測定した結果でも，署名Test Vectorでもありません．採用時は独立にReviewしたEncoding Vectorと，選択した暗号実装の署名Vectorを別途用意します．

6．Linear FactをAtomicな永続状態へ対応させる

TamarinのLinear FactはRuleで消費され，Persistent Factは保持されます．ただしStateはMultisetです．Unusedと名付けただけで一意になるわけではありません．一回限りの性質には，Nonceの一意生成，同じFactの複製がないこと，再生成Ruleがないことも必要です．[3]

実装では(key_id, audience, nonce)を主キーにし，保存したPayloadを不変に保ちます．Nonce衝突はInsert失敗として扱い，既存行を上書きしません．TamarinのFresh Nameは，有限の乱数空間とCSPRNGの実装を理想化しています．衝突の扱いは別のObligationです．

消費の核心は，検証した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;

PostgreSQLのRead Committedでは，競合するUPDATEは先行Transactionを待ち，更新後の行に対してWHERE条件を再評価します．この性質が条件付き消費の根拠の一部になります．SELECTしてから無条件にUPDATEする構成では同じ説明ができません．[6][7]

一行のRETURNINGは，外側のTransactionのCommit完了ではありません．Outbox Insertも含めてCommitしたことを確認し，初めて新しい受理結果として返します．ゼロ行の理由も，Replayだけとは限りません．未知のCapabilityやPayload不一致を含み得ます．[8]

SQL雛形だけでは，不変Payload，状態のReset禁止，DB Role，Durability，Failoverの設定を強制できていません．それらを実装・運用で満たして初めて，Modelとの対応を主張できます．

7．Commit，応答，外部Actionを区別する

TransactionがCommitした後，応答だけが失われることがあります．CallerがTimeoutを観測しても，Rollbackしたとは限りません．この場合の結果はUnknownです．安定したRequest IDで権威あるDBを照会し，同じ受理のReceiptへ対応付けます．既存Receiptを再返却することは，二度目のAcceptedではありません．

消費状態とDomain Eventを同じTransactionでOutboxへ保存すれば，Commit前だけEventが見える不整合を避ける設計にできます．ただしOutboxの配送は重複し得ます．下流の冪等性や同一Transaction内の業務更新は，別途必要です．

一回限りの消費は，外部Business ActionのExactly-once実行を意味しません． 消費後に外部処理が失敗すれば，実行はゼロ回かもしれません．再送時に重複実行すれば二回になるかもしれません．業務上のClaimがAction完了まで含むなら，別のStateとEventをModelへ足します．

8．Restrictionと暗号・Channelの前提を対応させる

Equality Restrictionは，Eq(x,y)が出るTraceをx=yの場合へ限定します．実装では，署名検証が成功した場合だけ次の処理へ進むGuardに対応します．任意のRestrictionを「当然の条件」として足すと，実装では可能な攻撃Traceを除外する危険があります．[4][5]

signingは，Ed25519や特定Libraryの検証結果ではありません．実装Algorithm，Library版，依存Review，鍵保管，API利用権限を別Evidenceとして持ちます．サンプルはRFC 8032のEd25519を候補Profileとして参照しますが，Libraryも署名連携も選択・実行していません．[10]

InとOutは，攻撃者がMessageを取得・構成・再送できる公開Networkの境界です．mTLSを実装に使っても，確実な配送やExactly-onceが付くわけではありません．逆にModelで攻撃者に見せないChannelを使うなら，秘匿性・Peer認証・配送のどれを仮定したかを分けます．

KeyRevealは鍵Materialが攻撃者へ渡る抽象Eventです．現実の侵害時刻を正確に観測できるとは限りません．失効は侵害そのものではなく，KMS APIの不正利用は鍵抽出とも異なります．必要ならSigning Oracleのような別の攻撃能力をModel化します．監視Logがないことを，侵害がなかった証明にしてはいけません．

9．Crash，Restore，時計も対応関係に含める

Processが再起動してもDBの消費状態が残ることと，FailoverやBackup Restoreでも二度と戻らないことは別です．PostgreSQLのDurabilityはWALと同期Commit等の設定に依存し，Replicaへの保証も構成で変わります．SQLにCOMMITと書くだけで，すべての障害に対する永続性は確立しません．[9]

昨日のBackupをRestoreすれば，消費済み行が未消費へ戻る可能性があります．今回のTheoryにはRollback Ruleがないため，そのTraceは解析対象外です．復旧時は古いTokenを受理しないEpoch管理，独立した消費台帳との照合，未処理Tokenの失効などを検討します．

鍵のRotationだけでは，古い検証鍵を引き続き信頼する場合にReplayを防げません．短いTTLも露出期間を狭めるだけです．どの条件で受理を再開してよいかをRecovery Procedureへ残します．

Expiryはこのサンプルにありません．追加するなら，Tamarinの#i < #jがUTCの比較ではなくTrace上の順序であることに注意します．有効期限の意味，許容Skew，Clock Source，検査からCommitまでの時間差を別途定義します．Natural Numberを導入しただけで，現実の時計と一致するわけではありません．

10．対応を守るTestと，運用Evidenceを分ける

Correspondence Testは，Lemmaの全Trace探索を再現するものではありません．実装がModelの観測点と前提を守っているかを確認します．

サンプルのCSVは，これらをNOT_RUNで並べたReview計画です．実行済みTest Suiteではありません．将来実行したら，入力，Revision，環境，実行Log，判定を結び付けます．

Runtimeの発行・消費EventをClaim IDと結ぶと，IncidentをModelの用語で説明しやすくなります．ただし有限のLog列は普遍的なPropertyのProofではありません．Log欠落や重複，配送順の入れ替わりも考慮します．Replay拒否MetricだけでReplay不能を証明することもできません．

11．Claim IDで変更とEvidenceを追う

Model，実装，テスト，運用が別Teamに分かれていても，Claim IDを共通の入口にできます．

Claim Recordには，Modelの実行結果，実装との対応Review，Deployment Revision，運用前提の確認結果を別々に持ちます．Proofが通ったModelのCommitだけで，現在のProductionへの適用を済ませません．未Commit差分を含め，何をReviewしたかを識別できるようにします．

PRでは，署名Field，鍵選択，消費のAtomicity，Expiry，復旧方針が変わったら対応Reviewを起動します．DBをStateless Tokenへ変える提案なら，Unusedに対応する状態が消えるため，Replay Claimを再検討する必要があります．

Manifestの構文，Claim ID，参照File・Symbolの存在をCIで確認することはできます．しかし関数が存在することと，その関数が正しいCommit Pointであることは別です．サンプルにはCIや参照Validatorを実装していません．自動検査で覆えない意味の対応は，Ownerを定めてReviewします．

12．ProofをProductionのAssuranceへつなぐ

Modelへ実装の全FunctionやTableを写す必要はありません．Securityに関係する意味を抽象化し，抽象化した箇所にどのEvidenceを置くかを残します．

今回なら，署名対象Field，信頼するAuthorityとAudience，現在の未消費状態，Atomicな消費，鍵侵害と復旧の前提が重要です．Function名が似ていることより，これらの意味を実装側で説明できることが保証を支えます．

AcceptedはどのCommitか．Unusedはどの状態か．Restoreでその状態が戻ったらどうするか．Correspondence ManifestとClaim Documentを入口に，その答えへ辿れる状態を維持します．Modelと実装の距離を消すのではなく，対応を説明できるEvidenceを更新し続けることが，形式検証を開発ループへ定着させます．

関連する認証・認可基盤PoCは担当範囲と設計判断の文脈です．本稿のCapability Model，Codec，SQL，未実行の確認計画を，その案件で実施済みのEvidenceとするものではありません．

参考資料

Tamarin Manualは以下のSource Revisionへ固定しています．これは文献の参照版であり，インストール済みToolchainやProof実行版ではありません．PostgreSQLは18のDocumentation，暗号方式は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