2008 Fiscal Year Annual Research Report
暗号アルゴリズムのハードウェア実装およびプロトコルの形式検証の研究
Project/Area Number |
08F08742
|
Research Institution | University of Tsukuba |
Principal Investigator |
岡本 栄司 University of Tsukuba, 大学院・システム情報工学研究科, 教授
|
Co-Investigator(Kenkyū-buntansha) |
SIMON Kramer 筑波大学, 大学院・システム情報工学研究科, 外国人特別研究員
|
Keywords | 暗号 / セキュリティ / FPGA / プロトコル / 形式検証 |
Research Abstract |
論理学、特にModal Logicを用いたモデルリングを行う。Modal Logicは攻撃を定式化する際に役立つもので、コンピュータウィルスをはじめ多くのアタックの解析、防御に適用していく。 課題の解決のために、アルゴリズムと実装に対してはCPL(Cryptographic Protocol Logic),プロトコルに対してはC3(Calculus of Cryptographic Communication)、応用に対してはMM(Malware Modeling)に分けて実施する。 今回、完全性と健全性を定式化した。完全性の方は正しくないエージェントの振る舞いを記述しており、健全性の方は正しいエージェントの振る舞いを記述している。これを利用して、システムの動作保証を別の簡単なシステムへ帰着することができた。 この結果を論文誌に投稿したところである。 Simon Kramer,Andrey Rybalchenko:A Multi-Modal Framework for Achieving Accountability in Multi-Agent Systems,Journal of Applied Non-Classical Logics
|