UMLによるプロテクションプロファイルのモデル化とその形式的検証

摘要

プロテクションプロファイルは，様々な情報システムにおけるセキュリティ仕様書の雛形であり，ISO/IEC15408という国際基準によりセキュリティが保証されている．しかしながら，扱う分野についての明確な規定がないことや，文書構造に問題があるため，実際にはほとんど利用されていない．本論文ではプロテクションプロファイルを効果的に利用できるよう，UMLによるモデル化を提案する．このモデル化により，ISO/IEC15408のセキュリティ基準に準拠した仕様記述を容易にする．また，モデル化したプロテクションプロファイルを用いて記述した仕様がセキュリティ基準を満たすかどうかを，定理証明技法とモデル検査技法により検証する技法を示す．