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
关键词
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 条
  • [41] UML Automatic Verification Tool with Formal Methods
    Beato, Ma Encarnacion
    Barrio-Solorzano, Manuel
    Cuesta, Carlos E.
    de la Fuente, Pablo
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 127 (04) : 3 - 16
  • [42] Formal verification of digital circuits using symbolic model checking
    Casar, A
    Brezocnik, Z
    Kapus, T
    INFORMACIJE MIDEM-JOURNAL OF MICROELECTRONICS ELECTRONIC COMPONENTS AND MATERIALS, 2000, 30 (03): : 153 - 160
  • [43] A Security Assurance Framework Combining Formal Verification and Security Functional Testing
    Wang, Weiguang
    Zeng, Qingkai
    Mathur, Aditya P.
    2012 12TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2012, : 136 - 139
  • [44] Formal verification of a group membership protocol using model checking
    Rosset, Valerio
    Souto, Pedro F.
    Vasques, Francisco
    ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS 2007: COOPLS, DOA, ODBASE, GADA, AND IS, PT 1, PROCEEDINGS, 2007, 4803 : 471 - 488
  • [45] Constructing Security Cases Based on Formal Verification of Security Requirements in Alloy
    Zeroual, Marwa
    Hamid, Brahim
    Adedjouma, Morayo
    Jaskolka, Jason
    COMPUTER SAFETY, RELIABILITY, AND SECURITY, SAFECOMP 2023 WORKSHOPS, 2023, 14182 : 15 - 25
  • [46] Automated Formal Verification of Model Transformations Using the Invariants Mechanism
    Ulitin, Boris
    Babkin, Eduard
    Babkina, Tatiana
    Vizgunov, Arsenii
    PERSPECTIVES IN BUSINESS INFORMATICS RESEARCH, BIR 2019, 2019, 365 : 59 - 73
  • [47] Formal Verification of Application-Specific Security Properties in a Model-Driven Approach
    Moebius, Nina
    Stenzel, Kurt
    Reif, Wolfgang
    ENGINEERING SECURE SOFTWARE AND SYSTEMS, PROCEEDINGS, 2010, 5965 : 166 - 181
  • [48] Formal Verification of Distributed System Using an Executable C Model
    Cifuentes, F.
    Bustos, J.
    Simmonds, J.
    IEEE LATIN AMERICA TRANSACTIONS, 2016, 14 (06) : 2874 - 2878
  • [49] A tool for lazy verification of security protocols
    Chevalier, Y
    Vigneron, L
    16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 373 - 376
  • [50] Verification of Operation Sequences in Process Simulate by Connecting a Formal Verification Tool
    Falkman, Petter
    Westman, Fredrik
    Modig, Christoffer
    2009 IEEE INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1-3, 2009, : 1207 - +