このリポジトリには、LLM支援によるセキュリティプロトコルモデリングのためのローカルなhuman-in-the-loop UIが含まれています。これは我々の研究で説明されているワークフローをサポートします：
LLM支援セキュリティプロトコルモデリングのための信頼度誘導型プロトコルIR
このシステムは、自然言語によるプロトコル記述とSapic+/Tamarin生成の間のセマンティックチェックポイントとしてプロトコル中間表現（IR）を導入し、レビュー担当者が形式的検証の前にLLM生成のプロトコルモデルのセマンティックな正確性を監査できるようにします。
以下のスクリーンショットは、レビューUIに読み込まれたSigfox準備済みワークフローを示しています。
run_contract_review_ui.py: ローカルHTTPサーバーとワークフローAPI。contract_review_ui/: ブラウザUI。protocol_ir_pipeline/: IR処理、モデリングコントラクト生成、Sapic+生成、修復、証明リント、およびTamarinヘルパー。protocol_ir_pipeline/c_to_ir.py: 埋め込みプロンプトを用いた段階的なC/C++ソースからProtocolIRへの抽出。scripts/c_to_protocol_ir.py: C/C++抽出フローのコマンドラインエントリポイント。config/: デフォルトのローカルリント/検索設定。examples/ui_input_cases.json: 実験に使用されるUI対応のベンチマーク入力。examples/ui_inputs.md: UIに手動で入力するためのコピーしやすいベンチマーク入力。難易度別にグループ化されています。examples/protocol-abstraction-cases.json: バンドルされた抽象化ヒントライブラリ。UIで有効にした場合にのみ使用されます。examples/prepared_workflows/gpt55/: ベンチマークケースの生IRおよび人間がレビューしたIRスナップショット。examples/user_tested_workflows/deepseek_ui_20260615/: 著者がUIを通じて手動でテストしたToyおよびSigfoxワークフロー。NOTICE.md: 帰属および成果物範囲に関する注記。LICENSE: GPLv3ライセンステキスト。PATH上にtamarin-prover。お使いのプラットフォームの公式手順に従ってTamarin Proverをインストールしてください：https://tamarin-prover.com/manual/master/book/002_installation.html。Python依存関係をインストールします：
pip install -r requirements.txt
認証情報を設定します：
cp .env.example .env
# edit .env and set the provider API key
空のワークフローディレクトリで開始します：
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--provider deepseek \
--host 127.0.0.1 \
--port 8765
開きます：
http://127.0.0.1:8765/
典型的なワークフロー：
Save Reviewedをクリックしてmodeling_contract.reviewed.jsonを書き込みます。Generate Sapic+をクリックします。tamarin-proverがインストールされている場合は、Tamarinでコンパイルおよび証明します。Save Reviewedは、すべてのレビューバッジが確認されることを要求しません。フィールドの確認は、レビューの進捗追跡や証明に重要な生成ヒントに役立ちますが、保存された編集は生成に引き続き使用されます。
抽出ステージ、JSON出力コントラクト、およびプロンプトはprotocol_ir_pipeline/c_to_ir.pyにあります。
LLMを使用して段階的抽出を実行します：
python3 scripts/c_to_protocol_ir.py \
--source path/to/protocol.c \
--output-dir runs/c_to_ir_demo \
--name MyProtocol \
--provider deepseek
このリポジトリには、tpm2-sessions.cのサニタイズされたC-to-IRデモ成果物が含まれています。以下のコマンドでUIを起動し、デモを開きます：
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--provider deepseek \
--host 127.0.0.1 \
--port 8765
http://127.0.0.1:8765/c-code-demo
プロトコルIRは、最終的な形式モデルが意味を持つために正しくある必要があるセマンティックな決定を記録します。これには以下が含まれます：
UIは起動後にバンドルされた抽象化ヒントライブラリを見つけることができますが、Sapic+を生成する前にユーザーがUse abstraction hintsをチェックしない限り、それを使用しません。このチェックボックスが有効な場合、バックエンドは以下から証明エンジニアリングのヒントを取得します：
examples/protocol-abstraction-cases.json
このライブラリを置き換えたり、別のものを使用したりできます：
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--abstraction-hints-path /path/to/protocol-abstraction-cases.json
examples/prepared_workflows/gpt55/には、ベンチマークケースの生IRおよび人間がレビューしたIRスナップショットが含まれています。各ケースには以下のみが含まれます：
ir/protocol_ir.json
ir/protocol_ir.reviewed.json
これらのファイルは、人間のレビュー前後のIRのコンパクトな例です。
examples/user_tested_workflows/deepseek_ui_20260615/には、手動テスト中に実際にUIを通じて実行された2つのワークフローが含まれています：
Toy
Sigfox
これらには、それらのUI実行からの軽量な成果物が含まれます：入力/レビュー成果物、プロンプト、LLM呼び出しメタデータ、生成されたTamarinモデル、コンパイル/修復出力、および証明ログ。API認証情報は含まれていません。
UIでそれらを検査するには、このワークフローライブラリでサーバーを起動します：
python3 run_contract_review_ui.py \
--run-dir runs/tmp_user_tested_review \
--workflow-library-dir examples/user_tested_workflows/deepseek_ui_20260615 \
--provider deepseek \
--host 127.0.0.1 \
--port 8765
次にUIを開き、Select prepared workflow...を使用して、easy / Toyまたはeasy / Sigfoxを選択します。
オプションで、UIからインポートする準備済みワークフローのディレクトリを公開できます：
python3 run_contract_review_ui.py \
--run-dir runs/local_demo \
--workflow-library-dir /path/to/prepared/workflows \
--provider deepseek
examples/ui_input_cases.jsonには、このレビューUI用に準備された18のプロトコル入力が含まれています。それらは、UIにコピーできる自然言語の記述、仮定、目標、および期待される結果として表現されています。
手動テスト用に、examples/ui_inputs.mdには同じケースが1つのコピーしやすいMarkdownファイルに含まれており、Easy、Medium、Hardのセクションにグループ化されています。
含まれるケース：
Example, NSPK, Naxos, Toy, Woo_Lam, sigfox, EDHOC, KEMTLS, LAK06, SPLICE,
SSH, CCITT_X509, Denning_Sacco, Kao_Chow, NSSK, Neuman_Stubblebine,
Otway_Rees, Yahalom
examples/ui_input_cases.jsonのベンチマーク入力は、AutoSMの18ケースベンチマーク入力から整理されました。完全なAutoSMベンチマーク参照Sapic+/Tamarinファイルは、このパッケージには含まれていません。
Ziyu Mao, Jingyi Wang, Jun Sun, Shengchao Qin, and Jiawen Xiong. "LLM-Aided Automatic Modeling for Security Protocol Verification." ICSE 2025. DOI: 10.1109/ICSE55347.2025.00197.
AutoSM成果物リポジトリ：https://github.com/zerrymore/AutoSM
このパッケージは、LICENSEにGPLv3ライセンステキストとともに配布されています。成果物範囲の帰属に関する注記についてはNOTICE.mdを参照してください。