アーキテクチャと原則
形式検証によるプロトコルの安全性保証とプライバシーモデルの設計原則
INTMAX は、強固なセキュリティとプライバシーを実現するために設計された L2（Layer 2）の zk-Rollup です。コアロジックは Nethermind の支援のもと、Lean 定理証明器を用いて形式検証（Formal Verification）されています。これにより、残高更新、Withdrawal ロジック、プルーフの妥当性の正しさが保証されています。
形式検証
INTMAX のコアプロトコルロジックは、Nethermind Formal Verification チームの指導のもと、Lean 定理証明器を用いて 機械的に検証されています。検証の対象は以下のとおりです：
残高計算モデルの正しさ
Withdrawal ロジックの健全性（二重支出の防止）
Merkle Inclusion Proof の妥当性
BLS 署名集約（Aggregate Signature）の一貫性
設計上の意義：Withdrawal が成功した場合、それは有効なプルーフが存在することを意味します。無効なプルーフは、アグリゲーターや L1 の敵対的な振る舞いにかかわらず、必ず拒否されます。
リプレイ攻撃・遅延攻撃への対策（任意だが推奨）
コアプロトコルは最小限の信頼と調整を前提としていますが、悪意のあるアグリゲーターが以下を試みる可能性があります：
リプレイ攻撃 — 過去に承認された Transfer ブロックを再送信する攻撃
遅延攻撃 — 有効なブロックを保留し、インクルージョンを遅延させる攻撃
これらの攻撃を分散性を損なわずに軽減するため、プロトコルでは 任意のリレイヤーコントラクトを使用して以下を強制できます：
Transfer ブロックへの単調タイムスタンプの付与
ファイナリティ期限 — ブロックが一定の時間枠内に公開されることを要求
ホワイトリスト — セッション中にブロックを送信できるアグリゲーターの鍵を限定
この機能はプロトコル外のパーミッションレス（Permissionless）な仕組みであり、ユーザーはソーシャルまたはマーケットインセンティブを通じて任意に利用できます。
プライバシー保証
INTMAX は、ミキサー、暗号化メモプール、シールドプールに依存することなくプライバシーを最大化するよう設計されています。
コア特性
トランザクションデータがオンチェーンに一切公開されない — 送信者、受信者、金額のいずれも明かされません
アグリゲーターがトランザクションの内容を知り得ない — 受け取るのはソルト付きハッシュのみです
トランザクションの詳細にアクセスできるのは受信者のみ — 送信者からのピアツーピア（P2P）メッセージを通じて共有されます
残高証明（Balance Proof）と Transfer はローカルで管理される — Withdrawal 時に ZK proof を通じてコントラクトに対してのみ開示されます
このモデルにより、以下のプライバシーが実現されます：
外部の観察者（L1 バリデーターを含む）が知り得るのは、誰が Deposit し誰が Withdrawal したかだけであり、その間の操作は一切不明
アグリゲーターはトランザクション内容を把握できないため、フロントランや内容に基づく検閲が不可能
ユーザーは残高の履歴をオフチェーンで選択的に開示できますが、自発的に開示しない限り プロトコルレベルでの紐付けは存在しない
まとめ
状態改ざん
残高ロジックの形式検証
✅
トランザクションリプレイ
単調性チェック付きの任意リレイヤー
⚠️ 任意
インクルージョン検閲
パーミッションレスなアグリゲーション（リーダー不要）
✅
トランザクション漏洩
オフチェーンでのトランザクション構築とプルーフ共有
✅
アグリゲーター漏洩
ハッシュベースのコミットメント、平文へのアクセス不可
✅
🔒 詳細情報： INTMAX のセキュリティテスト、監査、プライバシーアーキテクチャの包括的な概要については、以下のレポートを参照してください。
最終更新