JPYCv2 形式検証

外観

JPYC.receiveWithAuthorization_no_replay ​

名称・種別 ​

  • 名称: JPYC.receiveWithAuthorization_no_replay
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:466-478
  • 概要: 一度消費された認可は二度と receiveWithAuthorization に使えない（再生不可）。
  • 仕様: 対象

型シグネチャ ​

lean
∀ {O : JPYC.SigOracle} {s s' : JPYC.State} {ctx : JPYC.CallContext} {frm dst : JPYC.Address} {value validAfter validBefore : JPYC.U256} {nonce : JPYC.Bytes32} {v : JPYC.U8} {r sig : JPYC.Bytes32}, Eq (JPYC.receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig) (Except.ok s') → ∀ {ctx' : JPYC.CallContext} {dst' : JPYC.Address} {value' validAfter' validBefore' : JPYC.U256} {v' : JPYC.U8} {r' sig' : JPYC.Bytes32} {s'' : JPYC.State}, Ne (JPYC.receiveWithAuthorization O s' ctx' frm dst' value' validAfter' validBefore' nonce v' r' sig') (Except.ok s'')

一度成功した receiveWithAuthorization と同じ (認可者, nonce) では、その後どんな引数・文脈でも receiveWithAuthorization は二度と成功しない、という リプレイ防止 の定理です。

和訳 docstring ​

リプレイ不可。 一度消費された (from, nonce) では receiveWithAuthorization は二度と成功しない。

解説 ​

何を述べているか。 receiveWithAuthorization が一度成功して状態が s' になったあと、同じ (from, nonce) を使う receiveWithAuthorization（他の引数・受取人・時刻・署名は自由）は、結果状態がどうであれ .ok にはならないことを示します。背理法で、*_marks_used（成功後は 1）と再実行側の *_unused（成功には 0 が必要）が矛盾することを使います。

直感。 「同じ署名付き指示は一度しか効かない」。一度使った authorization は使用済み（1）なので、未使用ガード（0 が必要）を二度と通れません。

なぜ安全性に効くか。 EIP-3009 の 最重要保証 です。攻撃者が成立済みのトランザクションを再送（リプレイ）しても、二重に送金が実行されることはありません。署名そのものを傍受されても、認可は一回限りで使い切られます。

図解 ​

Lean ソースコード ​

lean
/-- **No replay** for `receiveWithAuthorization`. -/
theorem receiveWithAuthorization_no_replay {O : SigOracle} {s s' : State} {ctx : CallContext}
    {frm dst : Address} {value validAfter validBefore : U256} {nonce : Bytes32}
    {v : U8} {r sig : Bytes32}
    (h : receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig = .ok s')
    {ctx' : CallContext} {dst' : Address} {value' validAfter' validBefore' : U256} {v' : U8}
    {r' sig' : Bytes32} {s'' : State} :
    receiveWithAuthorization O s' ctx' frm dst' value' validAfter' validBefore' nonce v' r' sig' ≠ .ok s'' := by
  intro hreplay
  have hused := receiveWithAuthorization_marks_used h
  have hunused := receiveWithAuthorization_unused hreplay
  rw [hused] at hunused
  exact absurd hunused (by decide)

依存 ​