Formal Verification of Authorization Policies for Enterprise Social Networks Using PlusCal-2

被引:1
|
作者
Akhtar, Sabina [1 ]
Zahoor, Ehtesham [2 ]
Perrin, Olivier [3 ]
机构
[1] Bahria Univ, Islamabad, Pakistan
[2] Natl Univ Comp & Emerging Sci, Secure Networks & Distributed Syst Lab SENDS, Islamabad, Pakistan
[3] Univ Lorraine, LORIA, BP 239, F-54506 Vandoeuvre Les Nancy, France
关键词
Enterprise social network; Formal verification; Model checking; PLUSCAL-2; TLA(+); TLC; MODEL;
D O I
10.1007/978-3-030-00916-8_49
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Information security research has been a highly active and widely studied research direction. In the domain of Enterprise Social Networks (ESNs), the security challenges are amplified as they aim to incorporate the social technologies in an enterprise setup and thus asserting greater control on information security. Further, the security challenges may not be limited to the boundaries of a single enterprise and need to be catered for a federated environment where users from different ESNs can collaborate. In this paper, we address the problem of federated authorization for the ESNs and present an approach for combining user level policies with the enterprise policies. We present the formal verification technique for ESNs and how it can be used to identify the conflicts in the policies. It allows us to bridge the gap between user-centric or enterprise-centric approaches as required by the domain of ESN. We apply our specification of ESNs on a scenario and discuss the model checking results.
引用
收藏
页码:530 / 540
页数:11
相关论文
共 50 条
  • [1] Formal Specification and Verification of MQTT Protocol in PlusCal-2
    Sabina Akhtar
    Ehtesham Zahoor
    [J]. Wireless Personal Communications, 2021, 119 : 1589 - 1606
  • [2] Formal Specification and Verification of MQTT Protocol in PlusCal-2
    Akhtar, Sabina
    Zahoor, Ehtesham
    [J]. WIRELESS PERSONAL COMMUNICATIONS, 2021, 119 (02) : 1589 - 1606
  • [3] Formal Verification of Security Policy Implementations in Enterprise Networks
    Bera, P.
    Ghosh, S. K.
    Dasgupta, Pallab
    [J]. INFORMATION SYSTEMS SECURITY, PROCEEDINGS, 2009, 5905 : 117 - +
  • [4] Improving the Formal Verification of Reachability Policies in Virtualized Networks
    Bringhenti, Daniele
    Marchetto, Guido
    Sisto, Riccardo
    Spinoso, Serena
    Valenza, Fulvio
    Yusupov, Jalolliddin
    [J]. IEEE TRANSACTIONS ON NETWORK AND SERVICE MANAGEMENT, 2021, 18 (01): : 713 - 728
  • [5] Simplifying Neural Networks Using Formal Verification
    Gokulanathan, Sumathi
    Feldsher, Alexander
    Malca, Adi
    Barrett, Clark
    Katz, Guy
    [J]. NASA FORMAL METHODS (NFM 2020), 2020, 12229 : 85 - 93
  • [6] Formal Analysis of Smart Home Policies using Compositional Verification
    Khakpour, Narges
    Sirjani, Marjan
    Jalilia, Saeed
    [J]. FEATURE INTERACTIONS IN SOFTWARE AND COMMUNICATION SYSTEMS X, 2009, : 220 - 233
  • [7] Towards formal specification and verification of a role-based authorization engine using JML
    Mustafa, Tanveer
    Drouineaud, Michael
    Sohr, Karsten
    [J]. Proceedings - International Conference on Software Engineering, 2010, : 50 - 57
  • [8] Using weak bisimulation for enterprise integration architecture formal verification - I
    Cachia, Ernest
    Vella, Mark
    [J]. ECBS 2007: 14TH ANNUAL IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS: RAISING EXPECTATIONS OF COMPUTER-BASES SYSTEMS, 2007, : 63 - +
  • [9] Trust-based formal delegation framework for Enterprise Social Networks
    Bouchami, Ahmed
    Perrin, Olivier
    Zahoor, Ehtesham
    [J]. 2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 1, 2015, : 127 - 134
  • [10] A Flexible Authorization Mechanism for Enterprise Networks Using Smart-phone Devices
    Chifor, Bogdan-Cosmin
    Teican, Sorin
    Togan, Mihai
    Gugulea, George
    [J]. 2018 12TH INTERNATIONAL CONFERENCE ON COMMUNICATIONS (COMM), 2018, : 437 - 440