Formal verification of security model using SPR tool

Il Gon Kim, Miyoung Kang, Jin Young Choi, Peter D. Zegzhda, Maxim O. Kalinin, Dmitry P. Zegzhda, Inhye Kang

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

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 on 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.

Original languageEnglish
Pages (from-to)353-368
Number of pages16
JournalComputing and Informatics
Volume25
Issue number5
Publication statusPublished - 2006 Dec 8

Fingerprint

Access control
Model checking
Security systems
Formal verification

Keywords

  • SEW (security evaluation workshop)
  • SPR (safety problem resolver)
  • SPSL (safety problem specification language)

ASJC Scopus subject areas

  • Artificial Intelligence

Cite this

Kim, I. G., Kang, M., Choi, J. Y., Zegzhda, P. D., Kalinin, M. O., Zegzhda, D. P., & Kang, I. (2006). Formal verification of security model using SPR tool. Computing and Informatics, 25(5), 353-368.

Formal verification of security model using SPR tool. / Kim, Il Gon; Kang, Miyoung; Choi, Jin Young; Zegzhda, Peter D.; Kalinin, Maxim O.; Zegzhda, Dmitry P.; Kang, Inhye.

In: Computing and Informatics, Vol. 25, No. 5, 08.12.2006, p. 353-368.

Research output: Contribution to journalArticle

Kim, IG, Kang, M, Choi, JY, Zegzhda, PD, Kalinin, MO, Zegzhda, DP & Kang, I 2006, 'Formal verification of security model using SPR tool', Computing and Informatics, vol. 25, no. 5, pp. 353-368.
Kim IG, Kang M, Choi JY, Zegzhda PD, Kalinin MO, Zegzhda DP et al. Formal verification of security model using SPR tool. Computing and Informatics. 2006 Dec 8;25(5):353-368.
Kim, Il Gon ; Kang, Miyoung ; Choi, Jin Young ; Zegzhda, Peter D. ; Kalinin, Maxim O. ; Zegzhda, Dmitry P. ; Kang, Inhye. / Formal verification of security model using SPR tool. In: Computing and Informatics. 2006 ; Vol. 25, No. 5. pp. 353-368.
@article{a1d6ba31963045ac95201cac02f20a1c,
title = "Formal verification of security model using SPR tool",
abstract = "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 on 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.",
keywords = "SEW (security evaluation workshop), SPR (safety problem resolver), SPSL (safety problem specification language)",
author = "Kim, {Il Gon} and Miyoung Kang and Choi, {Jin Young} and Zegzhda, {Peter D.} and Kalinin, {Maxim O.} and Zegzhda, {Dmitry P.} and Inhye Kang",
year = "2006",
month = "12",
day = "8",
language = "English",
volume = "25",
pages = "353--368",
journal = "Computing and Informatics",
issn = "1335-9150",
publisher = "Slovak Academy of Sciences",
number = "5",

}

TY - JOUR

T1 - Formal verification of security model using SPR tool

AU - Kim, Il Gon

AU - Kang, Miyoung

AU - Choi, Jin Young

AU - Zegzhda, Peter D.

AU - Kalinin, Maxim O.

AU - Zegzhda, Dmitry P.

AU - Kang, Inhye

PY - 2006/12/8

Y1 - 2006/12/8

N2 - 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 on 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.

AB - 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 on 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.

KW - SEW (security evaluation workshop)

KW - SPR (safety problem resolver)

KW - SPSL (safety problem specification language)

UR - http://www.scopus.com/inward/record.url?scp=33845228619&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845228619&partnerID=8YFLogxK

M3 - Article

VL - 25

SP - 353

EP - 368

JO - Computing and Informatics

JF - Computing and Informatics

SN - 1335-9150

IS - 5

ER -