def securityParameterExponent : Nat

セキュリティパラメータの指数（ビット長の指数表現）

securityParameter = 2^8 = 256 ビット 指数表現を使用することで、Leanの計算を軽量化しています。

Equations

• securityParameterExponent = 8

def securityParameter : Nat

セキュリティパラメータ（ビット長）

AMATELUSプロトコルのセキュリティパラメータは256ビットに設定されています。

値: 2^8 = 256

根拠:

• SHA3-512の衝突耐性: 2^256 計算量（512ビット出力の半分）
• Ed25519の安全性: 128ビットセキュリティ（≈ 2^128）
• 全体のセキュリティレベル: min(256, 128) = 128ビット

形式検証では256を使用することで、ハッシュ関数の衝突耐性を 保守的に評価しています（実際の安全性は署名方式の128ビットに律速）。

ポスト量子暗号 (PQC) での安全性:

• Groverのアルゴリズム適用後: √(2^256) = 2^128
• 依然として十分な安全性を維持

Equations

• securityParameter = 2 ^ securityParameterExponent

theorem securityParameter_eq_256 : securityParameter = 256

セキュリティパラメータが256であることの補助定理

structure PPTAlgorithm : Type

PPT (Probabilistic Polynomial Time) アルゴリズム

• timeComplexity : Nat → Nat
• isPolynomial : ∃ (k : Nat), ∀ (n : Nat), self.timeComplexity n ≤ n ^ k

structure ComputationalSecurityLevel : Type

計算コストモデル（新しいモデル - 量子脅威を考慮）

幻想の排除: 「Negligible」という抽象的な概念ではなく、具体的な計算コスト（ビット単位）で 安全性を評価します。これにより、量子脅威を明示的に考慮できます。

NISTセキュリティレベル:

• Level 1: 128ビット (AES-128相当、量子耐性なし)
• Level 3: 192ビット (AES-192相当)
• Level 5: 256ビット (AES-256相当、ポスト量子暗号推奨)

• classicalBits : Nat

  古典計算機での攻撃コスト（ビット単位）

  例: 128ビット = 2^128 の計算量が必要

• quantumBits : Nat

  量子計算機での攻撃コスト（ビット単位）

  Groverのアルゴリズム適用後の計算量 例: 探索問題の場合、古典的256ビット → 量子的128ビット

• grover_reduction : self.quantumBits ≤ self.classicalBits

  Groverのアルゴリズムによる軽減を反映

  探索問題の場合: quantumBits = classicalBits / 2 構造的問題（Shorのアルゴリズム等）の場合はさらに低下

def minSecurityLevel : ComputationalSecurityLevel

NIST推奨の最小セキュリティレベル

ポスト量子暗号時代の安全性基準:

• 量子計算機の脅威を考慮すると、最低128ビットの量子攻撃コストが必要
• これはNIST Level 3以上に相当
• 古典的には256ビット以上の安全性が必要（Grover適用後に128ビット）

Equations

• minSecurityLevel = { classicalBits := 256, quantumBits := 128, grover_reduction := minSecurityLevel._proof_1 }

structure ProbabilisticHashFunction : Type

確率的衝突安全性を持つハッシュ関数

具体的な計算コストをパラメータとして持つハッシュ関数モデル。 AMATELUSのセキュリティは、この具体的な計算コストにのみ依存する。

• hash : List UInt8 → Hash

  ハッシュ計算関数

• collisionSecurity : ComputationalSecurityLevel

  衝突探索の計算コスト

  誕生日攻撃により、n ビット出力のハッシュ関数の衝突探索には 約 2^(n/2) の計算量が必要。SHA3-512の場合、512/2 = 256ビット。

• quantum_secure : self.collisionSecurity.quantumBits ≥ minSecurityLevel.quantumBits

  量子脅威を考慮した安全性の保証

  量子計算機の脅威下でも、最小セキュリティレベル（128ビット）を満たす

def amtHashFunction : ProbabilisticHashFunction

SHA3-512ハッシュ関数のインスタンス

AMT仕様（amt.md）に準拠:

• アルゴリズム: SHA3-512（NIST FIPS 202準拠）
• 出力長: 64バイト（512ビット）固定

計算コスト（誕生日攻撃による衝突探索）:

• 古典計算機: 2^256 の試行が必要（512ビット出力の平方根）
• 量子計算機: 2^128 の試行が必要（Groverのアルゴリズム適用）

量子脅威下での安全性:

• 量子攻撃コスト: 128ビット
• NIST最小要件: 128ビット
• 結論: ポスト量子暗号時代でも安全（128 ≥ 128）

重要: AMATELUSのセキュリティは、この具体的な計算コストにのみ依存します。 「negligible」や「耐衝突性」という幻想ではなく、量子脅威を考慮した 具体的な数値を明示しています。

Equations

• One or more equations did not get rendered due to their size.

noncomputable def hashForDID : List UInt8 → Hash

DID生成用ハッシュ関数

CryptoTypes.leanからの循環インポートを避けるため、ここで定義します。 この関数は amtHashFunction.hash のエイリアスです。

Equations

• hashForDID = amtHashFunction.hash

theorem hashForDID_quantum_secure : amtHashFunction.collisionSecurity.quantumBits = 128

hashForDIDの衝突探索コスト

異なる入力から同じハッシュ値を見つけるには、具体的な計算コストが必要です。

計算コスト（SHA3-512）:

• 古典計算機: 2^256 の試行（誕生日攻撃）
• 量子計算機: 2^128 の試行（Grover適用）

量子脅威下での安全性評価:

• 量子攻撃コスト: 128ビット
• NIST最小要件: 128ビット
• 結論: ちょうど最小要件を満たす（128 = 128）

重要な注意: SHA3-512は量子脅威下で「ギリギリ安全」です。より高い安全性マージンが 必要な場合は、SHA3-512/256（出力256ビット → 量子コスト64ビット）では不十分で、 より長い出力（例：Blake3の1024ビット）を検討すべきです。

theorem hashForDID_meets_minimum : amtHashFunction.collisionSecurity.quantumBits ≥ minSecurityLevel.quantumBits

structure KeyPair : Type

鍵ペアを表す型

• secretKey : SecretKey
• publicKey : PublicKey

structure SignatureScheme : Type

署名方式を表す構造体（計算コストモデル）

• keyGen : Unit → KeyPair
• sign : SecretKey → List UInt8 → Signature
• verify : PublicKey → List UInt8 → Signature → Bool
• completeness (kp : KeyPair) (msg : List UInt8) : let σ := self.sign kp.secretKey msg; self.verify kp.publicKey msg σ = true

  完全性: 正当な署名は常に検証に成功する

• forgeryResistance : ComputationalSecurityLevel

  署名偽造の計算コスト

  攻撃者が有効な署名を偽造するには、以下の計算量が必要です。

  注意:

  • Ed25519のような楕円曲線署名は、Shorのアルゴリズムにより量子計算機で多項式時間で破られます
  • ポスト量子暗号（PQC）署名方式（CRYSTALS-Dilithium、Falconなど）の採用が必須です
• quantum_secure : self.forgeryResistance.quantumBits ≥ minSecurityLevel.quantumBits

  量子脅威を考慮した安全性の保証

  量子計算機の脅威下でも、最小セキュリティレベル（128ビット）を満たす

def amtSignature : SignatureScheme

AMATELUSで使用する署名方式（ポスト量子暗号）

推奨方式: CRYSTALS-Dilithium2 (NIST Level 2)

• アルゴリズム: CRYSTALS-Dilithium2（NIST FIPS 204準拠）
• セキュリティレベル: NIST Level 2

計算コスト（署名偽造）:

• 古典計算機: 256ビット以上（格子問題LWE/SISの困難性）
• 量子計算機: 128ビット（NIST Level 2の定義）

量子脅威下での安全性:

• 量子攻撃コスト: 128ビット
• NIST最小要件: 128ビット
• 結論: ポスト量子暗号時代でも安全（128 ≥ 128）

重要: Ed25519のような楕円曲線署名は、Shorのアルゴリズムにより 量子計算機で多項式時間で破られます。AMATELUSの長期的安全性のためには、 ポスト量子暗号署名方式の採用が必須です。

Equations

• One or more equations did not get rendered due to their size.

theorem amtSignature_forgery_quantum_secure : amtSignature.forgeryResistance.quantumBits ≥ minSecurityLevel.quantumBits

署名偽造の量子安全性

AMATELUSで採用する署名方式（Dilithium2）は、量子脅威下でも 署名偽造に128ビットの計算量が必要です。

def hashPreimageSecurity : ComputationalSecurityLevel

一方向性の計算コスト

ハッシュ値から元の値を復元（原像攻撃）するには、全探索が必要です。 SHA3-512の場合、出力空間は2^512なので、全探索には2^512の試行が必要。

計算コスト（SHA3-512の原像攻撃）:

• 古典計算機: 2^512 の試行
• 量子計算機: 2^256 の試行（Grover適用）

量子脅威下での安全性評価:

• 量子攻撃コスト: 256ビット
• NIST最小要件: 128ビット
• 結論: 十分安全（256 > 128）、2倍の安全性マージン

Equations

• hashPreimageSecurity = { classicalBits := 512, quantumBits := 256, grover_reduction := hashPreimageSecurity._proof_1 }

theorem hash_preimage_quantum_secure : hashPreimageSecurity.quantumBits ≥ minSecurityLevel.quantumBits

def hashRandomOracleSecurity : ComputationalSecurityLevel

ランダムオラクル性の計算コスト

異なる入力に対するハッシュ値を理想的なランダム関数の出力と識別するには、 出力空間全体を探索する必要があります。

計算コスト（SHA3-512の識別攻撃）:

• 古典計算機: 2^512 の試行
• 量子計算機: 2^256 の試行（Grover適用）

量子脅威下での安全性評価:

• 量子攻撃コスト: 256ビット
• NIST最小要件: 128ビット
• 結論: 十分安全（256 > 128）、2倍の安全性マージン

Equations

• hashRandomOracleSecurity = { classicalBits := 512, quantumBits := 256, grover_reduction := hashPreimageSecurity._proof_1 }

theorem hash_random_oracle_quantum_secure : hashRandomOracleSecurity.quantumBits ≥ minSecurityLevel.quantumBits

structure ZKPSystem : Type

ゼロ知識証明システムの性質（計算コストモデル）

• prover : Witness → PublicInput → Relation → Proof
• verifier : Proof → PublicInput → Relation → Bool
• completeness (w : Witness) (x : PublicInput) (R : Relation) : R x w = true → self.verifier (self.prover w x R) x R = true

  完全性: 正当な証明は常に検証に成功する

• soundnessSecurity : ComputationalSecurityLevel

  偽証明の生成困難性

  攻撃者が偽の主張に対する有効な証明を生成するには、以下の計算量が必要です。

  注意:

  • ZKPの種類（STARK、SNARK、Bulletproofs等）により異なる
  • ポスト量子暗号時代では、STARKsなど量子耐性のあるZKPが推奨される
• zeroKnowledgeSecurity : ComputationalSecurityLevel

  証明の識別不可能性

  実際の証明とシミュレートされた証明を識別するには、以下の計算量が必要です。

  注意:

  • 零知識性の強度は、識別問題の困難性に依存する
  • シミュレータの存在により、証明から秘密情報を抽出できないことが保証される
• soundness_quantum_secure : self.soundnessSecurity.quantumBits ≥ minSecurityLevel.quantumBits

  量子脅威を考慮した健全性の保証

  量子計算機の脅威下でも、最小セキュリティレベル（128ビット）を満たす

• zeroKnowledge_quantum_secure : self.zeroKnowledgeSecurity.quantumBits ≥ minSecurityLevel.quantumBits

  量子脅威を考慮した零知識性の保証

  量子計算機の脅威下でも、最小セキュリティレベル（128ビット）を満たす

def amtZKP : ZKPSystem

AMATELUSで使用するZKPシステム（STARKs推奨）

推奨方式: STARKs (Scalable Transparent ARguments of Knowledge)

• アルゴリズム: STARKs（ポスト量子暗号安全）
• セキュリティレベル: 128ビット以上

計算コスト（偽証明の生成）:

• 古典計算機: 256ビット以上（ハッシュベースの困難性）
• 量子計算機: 128ビット（Grover適用後）

計算コスト（証明の識別）:

• 古典計算機: 256ビット以上（ランダムオラクルモデル）
• 量子計算機: 128ビット（Grover適用後）

量子脅威下での安全性:

• 健全性の量子コスト: 128ビット
• 零知識性の量子コスト: 128ビット
• NIST最小要件: 128ビット
• 結論: ポスト量子暗号時代でも安全（128 ≥ 128）

重要: SNARKsの一部（Groth16など）は、楕円曲線ペアリングに依存しており、 Shorのアルゴリズムにより量子計算機で破られる可能性があります。 AMATELUSの長期的安全性のためには、STARKsなど量子耐性のあるZKPが推奨されます。

Equations

• One or more equations did not get rendered due to their size.

theorem amtZKP_soundness_quantum_secure : amtZKP.soundnessSecurity.quantumBits ≥ minSecurityLevel.quantumBits

ZKP健全性の量子安全性

AMATELUSで採用するZKPシステム（STARKs）は、量子脅威下でも 偽証明の生成に128ビットの計算量が必要です。

theorem amtZKP_zeroKnowledge_quantum_secure : amtZKP.zeroKnowledgeSecurity.quantumBits ≥ minSecurityLevel.quantumBits

ZKP零知識性の量子安全性

AMATELUSで採用するZKPシステム（STARKs）は、量子脅威下でも 証明の識別に128ビットの計算量が必要です。

def keyPairIndependenceSecurity : ComputationalSecurityLevel

鍵ペアの関連性発見の計算コスト

異なる鍵ペア間の関連性を発見するには、以下の計算量が必要です。

Dilithium2の場合:

• 古典計算機: 256ビット以上（格子問題LWEの困難性）
• 量子計算機: 128ビット（NIST Level 2）

注意: これは鍵生成に使用される擬似乱数生成器（PRNG）の安全性にも依存します。

Equations

• keyPairIndependenceSecurity = { classicalBits := 256, quantumBits := 128, grover_reduction := minSecurityLevel._proof_1 }

theorem keyPairIndependence_quantum_secure : keyPairIndependenceSecurity.quantumBits ≥ minSecurityLevel.quantumBits

def nonceCollisionSecurity : ComputationalSecurityLevel

ナンス衝突の計算コスト

独立に生成された2つのナンスが衝突する確率は、誕生日攻撃により計算されます。

256ビットナンスの場合:

• 古典計算機: 2^128 の試行で衝突確率50%（誕生日攻撃）
• 量子計算機: 2^128 の試行で衝突確率50%（Groverでは改善されない）

注意: 誕生日攻撃はGroverのアルゴリズムで改善されないため、 古典的な衝突確率がそのまま量子脅威下でも適用されます。

Equations

• nonceCollisionSecurity = { classicalBits := 128, quantumBits := 128, grover_reduction := nonceCollisionSecurity._proof_1 }

theorem nonceUniqueness_quantum_secure : nonceCollisionSecurity.quantumBits ≥ minSecurityLevel.quantumBits