Formal verification of security model using SPR tool

被引：0
|
作者：
Kim, Il-Gon [1 ]
Kang, Miyoung
Choi, Jin-Young
Zegzhda, Peter D.
Kalinin, Maxim O.
Zegzhda, Dmitry P.
Kang, Inhye
机构：
[1] Korea Univ, Seoul 136701, South Korea
[2] St Petersburgh Polytech Univ, St Petersburg, Russia
[3] Univ Seoul, Seoul, South Korea
来源：
COMPUTING AND INFORMATICS | 2006年 / 25卷 / 05期
关键词：
SPR (Safety Problem Resolver); SEW (Security Evaluation Workshop); SPSL (Safety Problem Specification Language);
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In this paper, formal verification methodologies and the SPR (Safety Problem Resolver) model checking tool are used for verifying a security model's safety. The SPR tool makes it possible to analyze security issues oil security systems based on the access control model. To illustrate this approach, a case study of the Simple Access Control Model (SACM) is used and specific safety problems of the security model are analyzed using the SPR tool.
引用
收藏
页码：353 / 368
页数：16
相关论文
共 50 条
  • [1] Formal Verification of IEEE 802.16 Security Sublayer Using Scyther Tool
    Taha, Ahmed M.
    Abdel-Hamid, Amr T.
    Tahar, Sofiene
    [J]. 2009 INTERNATIONAL CONFERENCE ON NETWORK AND SERVICE SECURITY, 2009, : 172 - +
  • [2] Educating Cryptography using Formal Security Verification tool for Cryptographic Protocols.
    Okazaki H.
    Shimura S.
    Miyamoto T.
    Watanabe T.
    Murakami Y.
    Futa Y.
    [J]. Computer Software, 2020, 37 (01) : 99 - 113
  • [3] Formal Verification of Security Protocols Using Spin
    Chen, Shengbo
    Fu, Hao
    Miao, Huaikou
    [J]. 2016 IEEE/ACIS 15TH INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE (ICIS), 2016, : 637 - 642
  • [4] Formal specification and security verification of the IDKE protocol using FDR model checking
    Soltwisch, R
    Tegeler, F
    Hogrefe, D
    [J]. 2005 13TH IEEE INTERNATIONAL CONFERENCE ON NETWORKS JOINTLY HELD WITH THE 2005 7TH IEEE MALAYSIA INTERNATIONAL CONFERENCE ON COMMUNICATIONS, PROCEEDINGS 1 AND 2, 2005, : 329 - 334
  • [5] Hierarchical formal verification using a hybrid tool
    Kort, Skander
    Tahar, Sofiène
    Curzon, Paul
    [J]. International Journal on Software Tools for Technology Transfer, 2003, 4 (03) : 313 - 322
  • [6] Verification of a formal security model for multiapplicative smart cards
    Schellhorn, G
    Reif, W
    Schairer, A
    Karger, P
    Austel, V
    Toll, D
    [J]. COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, 2000, 1895 : 17 - 36
  • [7] Formal verification of ASM designs using the MDG tool
    Gawanmeh, A
    Tahar, S
    Winter, K
    [J]. FIRST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2003, : 210 - 219
  • [8] FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408
    Yajima, Kenichi
    Morimoto, Shoichi
    Horie, Daisuke
    Azreen, Noor Sheila
    Goto, Yuichi
    Cheng, Jingde
    [J]. 2009 INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY, AND SECURITY (ARES), VOLS 1 AND 2, 2009, : 624 - +
  • [9] Formal specification and verification of resource bound security using PVS
    Yu, WJ
    Mok, AK
    [J]. SOFTWARE SECURITY - THEORIES AND SYSTEMS, 2004, 3233 : 113 - 133
  • [10] Using temporal logics of knowledge in the formal verification of security protocols
    Dixon, C
    Gago, MCF
    Fisher, M
    van der Hoek, W
    [J]. 11TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2004, : 148 - 151
12345