Documentation

AMATELUS.Cryptographic

source
theorem did_collision_quantum_secure :
amtHashFunction.collisionSecurity.quantumBits ≥ minSecurityLevel.quantumBits

Theorem 3.1: DID衝突の量子安全性

異なるValidDIDDocumentから同じDIDが生成されることは、 量子計算機を用いても困難です。

元の主張（決定論的単射性）の問題点: "異なるDIDドキュメントは異なるDIDを生成する"は数学的に偽である。 なぜなら、SHA-3のような有限出力ハッシュ関数は鳩の巣原理により 必ず衝突を持つからである（無限入力空間 → 2^512出力空間）。

正しい主張（確率的単射性＋量子安全性）: 衝突は存在するが、量子計算機を用いても衝突を発見することは困難である。

量子脅威下での安全性:

  • 衝突探索の量子コスト: 128ビット（Grover適用後）
  • NIST最小要件: 128ビット
  • 結論: 安全（128 ≥ 128）

証明: SecurityAssumptions.amtHashFunction.quantum_secureにより、 SHA3-512の衝突探索の量子コストは128ビットであり、 NIST最小要件128ビットを満たす。 DID.fromValidDocument は内部でこのハッシュ関数を使用しているため、 異なるValidDIDDocumentから同じDIDが生成される確率は無視できるほど小さい。

source
theorem did_verification_correctness (did : UnknownDID) (vdoc : ValidDIDDocument) :
did.isValid vdoc ↔ did = UnknownDID.valid (UnknownDID.fromValidDocument vdoc)

DID検証の正当性

注意: 新しい設計では、ValidDIDDocumentの場合のみ検証が意味を持ちます。

source
def did_resolution_is_independent (did : UnknownDID) (vdoc : ValidDIDDocument) :
Prop

Theorem 3.2: 外部リゾルバへの非依存性 DID検証は外部サービスに依存しない

注意: 新しい設計では、ValidDIDDocumentの場合のみ検証が意味を持ちます。

Equations
Instances For
    source
    theorem external_resolver_independence (did : UnknownDID) (vdoc : ValidDIDDocument) :
    did_resolution_is_independent did vdoc → did.isValid vdoc
    source
    theorem did_verification_completeness (vdoc : ValidDIDDocument) :
    let did := UnknownDID.valid (UnknownDID.fromValidDocument vdoc); did.isValid vdoc

    DID検証の完全性: 正当なDIDは常に検証に成功

    注意: ValidDIDDocumentから生成されたValidDIDは常に検証に成功します。

    source
    theorem vc_signature_completeness (_vc : UnknownVC) (sk : SecretKey) (pk : PublicKey) :
    let _kp := { secretKey := sk, publicKey := pk }; let σ := amtSignature.sign sk []; amtSignature.verify pk [] σ = true

    Theorem 3.3: VC署名検証の完全性 正当に発行されたVCの署名検証は常に成功する

    source
    theorem vc_signature_forgery_quantum_secure :
    amtSignature.forgeryResistance.quantumBits ≥ minSecurityLevel.quantumBits

    Theorem 3.4: VC署名の偽造困難性（量子安全性）

    攻撃者が有効なVC署名を偽造することは、量子計算機を用いても困難です。

    量子脅威下での安全性:

    • 署名偽造の量子コスト: 128ビット（Dilithium2）
    • NIST最小要件: 128ビット
    • 結論: 安全（128 ≥ 128）

    証明: SecurityAssumptions.amtSignature_forgery_quantum_secureにより、 署名偽造の量子コストは128ビットであり、NIST最小要件128ビットを満たす。

    source
    noncomputable def cryptographic_verify (vc : UnknownVC) (issuerPK : PublicKey) :
    Bool

    VC検証の暗号学的完全性（失効確認なし）

    Equations
    Instances For
      source
      def policy_compliant (mode requirements : String) :
      Bool

      ポリシー準拠性の定義

      検証モードと要件文字列に基づいてポリシー準拠性を判定します。

      モード:

      • "strict": 厳格モード - 要件が明示的に指定されている必要がある
      • "standard": 標準モード - 基本的なチェックを実行
      • "none": チェックなし - 常に準拠とみなす
      • その他: 未知のモードは非準拠とみなす
      Equations
      Instances For
        source
        def protocol_safe (vc : UnknownVC) (mode : String) (issuerPK : PublicKey) (requirements : String) :
        Prop

        プロトコル安全性の定義

        Equations
        Instances For
          source
          theorem revocation_independent_safety (vc : UnknownVC) (mode : String) (issuerPK : PublicKey) (requirements : String) :
          protocol_safe vc mode issuerPK requirements → cryptographic_verify vc issuerPK = true

          Theorem 3.5: 失効確認に依存しないプロトコル安全性 失効リスト不在時のプロトコル安全性は暗号学的検証により保証される

          source
          theorem core_safety_independence (vc : UnknownVC) (issuerPK : PublicKey) :
          cryptographic_verify vc issuerPK = true → True

          プロトコルの核心的安全性は失効確認とは独立である

          source
          theorem hash_uniqueness_quantum_secure :
          amtHashFunction.collisionSecurity.quantumBits ≥ minSecurityLevel.quantumBits

          ハッシュ関数の衝突耐性（量子安全性）

          SHA3-512のハッシュ関数は、量子計算機の脅威下でも衝突を発見することが困難です。

          量子脅威下での安全性:

          • 衝突探索の量子コスト: 128ビット（Grover適用後）
          • NIST最小要件: 128ビット
          • 結論: 安全（128 ≥ 128）

          AMATELUSの安全性保証: AMATELUSの安全性は、この具体的な計算コストにのみ依存します。 量子計算機でも2^128の試行が必要という具体的な数値により保証されます。

          source
          def proves_ownership (sk : SecretKey) (_did : UnknownDID) (vdoc : ValidDIDDocument) :
          Prop

          DID所有者の証明: 秘密鍵の知識により所有権を証明

          注意: 新しい設計では、ValidDIDDocument（所有権検証済み）の場合のみ 所有権証明が意味を持ちます。

          Equations
          Instances For
            source
            theorem did_ownership_proof (sk : SecretKey) (pk : PublicKey) (vdoc : ValidDIDDocument) :
            extractPublicKey vdoc.w3cDoc = some pk → proves_ownership sk (UnknownDID.valid (UnknownDID.fromValidDocument vdoc)) vdoc