| Item type |
紀要論文(ELS) / Departmental Bulletin Paper(1) |
| 公開日 |
2007-03-31 |
| タイトル |
|
|
タイトル |
セキュリティプロトコルの簡易検証I : 具体意味論 |
| タイトル |
|
|
タイトル |
A Lightweight Verification Method : Concrete Semantics |
|
言語 |
en |
| 言語 |
|
|
言語 |
jpn |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
departmental bulletin paper |
| ページ属性 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
P(論文) |
| 記事種別(日) |
|
|
|
論説 |
| 記事種別(英) |
|
|
|
en |
|
|
Article |
| 著者名(日) |
大矢野, 潤
|
| 著者名よみ |
オオヤノ, ジュン
|
| 著者名(英) |
OYANO, Jun
|
| 著者所属(日) |
|
|
|
千葉商科大学計算機科学政策情報学部 |
| 抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
To represent secure systems over open networks, there exists cryptosystems and its application. Robustness of a cryptosystem is given by computational approaches and formal ones. The computational approach relies on issues of complexity and probability, on the other hand, the formal method omit discussions about complexity of systems using an idealized cryptography, which is called "Computational hardness assumptions". Even if we omit computational discussion, it is still hard to prove the safety properties of network protocols. To cope with undecidability and complexity of analyzing formal systems, the author introduces "Yield-Arrow Nonce Protocol Inspection Method (YANPI method)". Using this method, we expect to get lightweight and intuitive verification method. The YANPI Method's model is established on a concrete semantics using directed graphs, however, its analyzing algorithms use abstracted directed graphs and its refinement. In this paper, we introduce the formal concrete model of the YANPI method. In the next paper, we are planning to present YANPI method's abstraction and refinement algorithms. |
| 雑誌書誌ID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AN0014259X |
| 書誌情報 |
千葉商大論叢
巻 44,
号 4,
p. 27-52,
発行日 2007-03-31
|
KJ00004684526.pdf (1.4 MB)
