WEKO3
アイテム
A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System
http://hdl.handle.net/10173/1457
http://hdl.handle.net/10173/14578c916410-f48b-420f-9b5f-52f94951d482
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
28-50.pdf (908.5 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2017-03-24 | |||||||||
| タイトル | ||||||||||
| タイトル | A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | weighted pushdown systems | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | access control | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | model checking | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者 |
LAMILLA, ALVAREZ Pablo
× LAMILLA, ALVAREZ Pablo
× TAKATA, Yoshiaki
|
|||||||||
| 抄録 | ||||||||||
| 内容記述タイプ | Abstract | |||||||||
| 内容記述 | Information-Based Access Control (IBAC) has been proposed as an improvement to History-Based Access Control (HBAC) model. In modern component-based systems, these access control models verify that all the code responsible for a security-sensitive operation is sufficiently authorized to execute that operation. The HBAC model, although safe, may incorrectly prevent the execution of operations that should be executed. The IBAC has been shown to be more precise than HBAC maintaining its safety level while allowing sufficiently authorized operations to be executed. However the verification problem of IBAC program has not been discussed. This paper presents a formal model for IBAC programs based on extended weighted pushdown systems (EWPDS). The mapping process between the IBAC original semantics and the EWPDS structure is described. Moreover, the verification problem for IBAC programs is discussed and several typical IBAC program examples using our model are implemented. | |||||||||
| 書誌情報 |
IEICE Transactions on Information and Systems 巻 E97-D, 号 5, p. 1149-1159, 発行日 2014-05 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 0916-8532 | |||||||||
| DOI | ||||||||||
| 関連タイプ | isIdenticalTo | |||||||||
| 識別子タイプ | DOI | |||||||||
| 関連識別子 | 10.1587/transinf.E97.D.1149 | |||||||||
| 権利 | ||||||||||
| 権利情報 | © 2014 The Institute of Electronics, Information and Communication Engineers | |||||||||
| 権利 | ||||||||||
| 権利情報 | LAMILLA ALVAREZ, Pablo TAKATA, Yoshiaki, A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System, IEICE Transactions on Information and Systems, E97.D(5), 1149-1159, 2014-05 | |||||||||
| 権利（URI） | ||||||||||
| 権利情報 | https://search.ieice.org/ | https://search.ieice.org/ | |||||||||
| 著者版フラグ | ||||||||||
| 出版タイプ | VoR | |||||||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||||||
| 出版者 | ||||||||||
| 出版者 | 一般社団法人電子情報通信学会 | |||||||||
