Isabelleにおけるセキュリティ工学のための形式的開発サイクル【JST・京大機械翻訳】

Kammueller Florian

プレプリント

J-GLOBAL ID：202202220268035448 整理番号：22P0104220

Isabelleにおけるセキュリティ工学のための形式的開発サイクル【JST・京大機械翻訳】

A Formal Development Cycle for Security Engineering in Isabelle

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

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

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

本論文では,証明支援Isabelleにおいて完全に定式化された精密化の形式的概念に基づくセキュリティ工学プロセスを示した。この精密化-Riskサイクルは,対話型定理証明によってサポートされた攻撃解析とセキュリティ精密化に焦点を合わせる。アクターと政策を持つインフラストラクチャの完全形式化モデルを使用するので,システム仕様のための形式的セキュリティ精密化の新しい方法をサポートできる。この形式的プロセスは,攻撃ツリーによるIsabelleインフラストラクチャーフレームワークへの拡張として実際に構築される。インフラストラクチャモデルの精密化の形式的概念を定義した。IsabelleインフラストラクチャーフレームワークにおけるKripke構造と分岐時間論理の形式的基礎のおかげで,これらの段階的変換を攻撃木解析とインターリーブし,従って完全形式的セキュリティ工学フレームワークを提供した。プロセスは,GDPR要求とブロックチェーンを導入したIoTヘルスケア事例研究で例証した。【JST・京大機械翻訳】

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

データ保護

, ,

前のページに戻る