Design and Formal Verification of DZMBE

被引:0
|
作者
Mohammadi, Mahdi Soodkhah [1 ]
Bafghi, Abbas Ghaemi [1 ]
机构
[1] Ferdowsi Univ Mashhad, Engn Fac, Comp Dept, Data & Commun Secur Lab, Mashhad, Iran
关键词
Broadcast Encryption; Secure Multiparty Computation; Threshold Secret Sharing; Formal Methods; Applied pi Calculus;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
In this paper, a new broadcast encryption scheme is presented based on threshold secret sharing and secure multiparty computation. This scheme is maintained to be dynamic in that a broadcaster can broadcast a message to any of the dynamic groups of users in the system and it is also fair in the sense that no cheater is able to gain an unfair advantage over other users. Another important feature of our scheme is collusion resistance. Using secure multiparty computation, a traitor needs k cooperators in order to create a decryption machine. The broadcaster can choose the value of k as he decides to make a trade-off between communication complexity and collusion resistance. Comparison with other Broadcast Encryption schemes indicates enhanced performance and complexity on the part of the proposed scheme (in terms of message encryption and decryption, key storage requirements, and ciphertext size) relative to similar schemes. In addition, the scheme is modeled using applied pi calculus and its security is verified by means of an automated verification tool, i.e., ProVerif. (C) 2013 ISC. All rights reserved.
引用
收藏
页码:37 / 53
页数:17
相关论文
共 50 条
  • [21] Review on Spacecraft Formal System Design Verification
    Wang, Huamao
    Wang, Yan
    SEC 2008: PROCEEDINGS OF THE FIFTH IEEE INTERNATIONAL SYMPOSIUM ON EMBEDDED COMPUTING, 2008, : 388 - 393
  • [22] Formal framework for design and verification or robotic agents
    Periyasamy, K.
    Alagar, V.S.
    Bui, T.D.
    Journal of Intelligent and Robotic Systems: Theory and Applications, 1993, 8 (02): : 173 - 200
  • [23] Formal verification of structured analysis and design in HOS
    Chiang, CC
    Lee, R
    Third ACIS International Conference on Software Engineering Research, Managment and Applications, Proceedings, 2005, : 282 - 287
  • [24] Towards Formal Evaluation and Verification of Probabilistic Design
    Lee, Nian-Ze
    Jiang, Jie-Hong R.
    2014 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2014, : 340 - 347
  • [25] A FORMAL FRAMEWORK FOR DESIGN AND VERIFICATION OF ROBOTIC AGENTS
    PERIYASAMY, K
    ALAGAR, VS
    BUI, TD
    JOURNAL OF INTELLIGENT & ROBOTIC SYSTEMS, 1993, 8 (02) : 173 - 200
  • [26] Testing and Formal Verification of Logarithmic Function Design
    Agarwal, Sanjeev
    Bhuria, Indu
    INTERNATIONAL CONFERENCE ON METHODS AND MODELS IN SCIENCE AND TECHNOLOGY (ICM2ST-10), 2010, 1324 : 57 - +
  • [27] Research on Formal Design and Verification of Operating Systems
    Qian, Zhenjiang
    Liu, Yongjun
    Jin, Yong
    Xing, Xiaoshuang
    Zhang, Mingxin
    Gong, Shengrong
    Liu, Wei
    Yang, Weiyong
    Tan, Jack
    Zhang, Lifeng
    EMBEDDED SYSTEMS TECHNOLOGY, ESTC 2017, 2018, 857 : 81 - 88
  • [28] Formal Verification of Cloud Orchestration Design with TOSCA and BPEL
    Chareonsuk, Warun
    Vatanawood, Wiwat
    2016 13TH INTERNATIONAL CONFERENCE ON ELECTRICAL ENGINEERING/ELECTRONICS, COMPUTER, TELECOMMUNICATIONS AND INFORMATION TECHNOLOGY (ECTI-CON), 2016,
  • [29] COMPASTA: Extending TASTE with Formal Design and Verification Functionality
    Bombardelli, Alberto
    Bozzano, Marco
    Cavada, Roberto
    Cimatti, Alessandro
    Griggio, Alberto
    Nazaria, Massimo
    Nicolodi, Edoardo
    Tonetta, Stefano
    MODEL-BASED SAFETY AND ASSESSMENT, IMBSA 2022, 2022, 13525 : 21 - 27
  • [30] Improving a Design Methodology of Synthesizable VHDL With Formal Verification
    Perpetuo Costa Marques, Luis Gustavo
    de Queiroz, Max Hering
    Farines, Jean-Marie
    2016 IEEE 7TH LATIN AMERICAN SYMPOSIUM ON CIRCUITS & SYSTEMS (LASCAS), 2016, : 51 - 54