アクセス制御のための最弱前処理を用いたAgdaにおけるビットコインスクリプトの検証【JST・京大機械翻訳】

Alhabardi Fahad F.; Beckmann Arnold; Lazar Bogdan; Setzer Anton

プレプリント

J-GLOBAL ID：202202220975225105 整理番号：22P0299704

アクセス制御のための最弱前処理を用いたAgdaにおけるビットコインスクリプトの検証【JST・京大機械翻訳】

Verification of Bitcoin Script in Agda using Weakest Preconditions for Access Control

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (4件)： , , ,
資料名：
発行年： 2022年03月06日プレプリントサーバーでの情報更新日： 2022年06月11日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

※このプレプリント論文は学術誌に掲載済みです。なお、学術誌掲載の際には一部内容が変更されている可能性があります。

本論文は,双方向定理証明器AgdaにおけるBitcoinのスマート契約言語SCRIPTで書かれたプログラムの検証に貢献する。それは,Bitcoinsの分布を支配するSCRIPTプログラムのためのアクセス制御のセキュリティ特性に焦点を合わせる。それは,Hoareトリプルの文脈における最も弱い前提条件が,アクセス制御を検証する適切な概念であると主張する。それは,ユーザ要求とスマート契約の形式的仕様の間の検証ギャップを閉じるために,最も弱い前提条件の人間可読記述を得ることを目指している。提案方法の例として,本論文は,Bitcoinsの分布を支配する2つの標準SCRIPTプログラム,Payから公開鍵ハッシュ(P2PKH)とPay(P2MS)に焦点を当てた。本論文では,P2PKHとP2MSで用いられるSCRIPTコマンドの運用意味論を導入し,それはAgda証明支援で定式化され,Hoare3重項を用いて推論された。最も弱い前提条件の人間可読記述を得るための2つの方法論を議論した。(1)ステップバイステップアプローチ,それはスクリプトを通して命令によって後方命令を作って,時々いくつかの命令を一緒にグループ分けする;(2)コードの記号的実行と入れ子ケース識別への翻訳,それは受容経路に沿った条件の結合の混乱として最弱な前提条件を読むことを可能にする。Hoare Triplesによる方程式推論のための構文を,Agdaにおけるこれらのアプローチを定式化するために定義した。キーワードとフレーズ:ブロックチェーン;暗号性;ビトコイン;Agda;検証;Hoare論理;ビトコインスクリプト;P2PKH;P2MS;アクセス制御;最も弱い前提条件;先行変圧器意味論;証明可能な正当性;記号実行;スマート契約。【JST・京大機械翻訳】

, , , , , , , ,
, , , , , , , 【Automatic Indexing@JST】

符号理論 , データ保護

, ,

前のページに戻る