Bisimulation and unwinding for verifying possibilistic security properties

被引:0
|
作者
Bossi, A [1 ]
Focardi, R [1 ]
Piazza, C [1 ]
Rossi, S [1 ]
机构
[1] Univ Ca Foscari, Dipartimento Informat, Venice, Italy
关键词
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
We study bisimulation-based information flow security properties which are persistent, in the sense that if a system is secure, then all states reachable from it are secure too. We show that such properties can be characterized in terms of bisimulation-like equivalence relations between the system and the system itself prevented from performing confidential actions. Moreover, we provide a characterization of such properties in terms of unwinding conditions which-demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. We also prove several compositionality results and discuss a sufficient condition to define refinement operators preserving security.
引用
收藏
页码:223 / 237
页数:15
相关论文
共 50 条
  • [1] Unwinding possibilistic security properties
    Mantel, H
    [J]. COMPUTER SECURITY - ESORICS 2000, PROCEEDINGS, 2000, 1895 : 238 - 254
  • [2] Verifying persistent security properties
    Bossi, A
    Focardi, R
    Piazza, C
    Rossi, S
    [J]. COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2004, 30 (3-4) : 231 - 258
  • [3] Verifying Opacity Properties in Security Systems
    Mu, Chunyan
    Clark, David
    [J]. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, 2023, 20 (02) : 1450 - 1460
  • [4] An environment for specifying and verifying security properties
    Renaud, A
    Krishnan, P
    [J]. 2001 AUSTRALIAN SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2001, : 203 - 212
  • [5] Verifying Quantum Communication Protocols with Ground Bisimulation
    Qin, Xudong
    Deng, Yuxin
    Du, Wenjie
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 21 - 38
  • [6] Verifying polymer reaction networks using bisimulation
    Johnson, Robert F.
    Winfree, Erik
    [J]. THEORETICAL COMPUTER SCIENCE, 2020, 843 : 84 - 114
  • [7] Verifying Security Properties in Unbounded Multiagent Systems
    Boureanu, Ioana
    Kouvaros, Panagiotis
    Lomuscio, Alessio
    [J]. AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2016, : 1209 - 1217
  • [8] Verifying security properties of cryptoprotocols: A novel approach
    Saleh, Mohamed
    Debbabi, Mourad
    [J]. SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 349 - +
  • [9] Verifying chemical reaction network implementations: A bisimulation approach
    Johnson, Robert
    Dong, Qing
    Winfree, Erik
    [J]. THEORETICAL COMPUTER SCIENCE, 2019, 765 : 3 - 46
  • [10] ALGORITHM FOR VERIFYING STRONG OPEN BISIMULATION IN FULL Π-CALCULUS
    邓玉欣
    傅育熙
    [J]. Journal of Shanghai Jiaotong University(Science), 2001, (02) : 147 - 152