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 条
  • [1] Incremental formal design verification
    Swamy, Gitanjali M.
    Brayton, Robert K.
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994, : 458 - 465
  • [2] Design and formal verification of an intelligent alarm
    Li, Xin Ben
    Sun, De Chao
    WSEAS Transactions on Systems, 2007, 6 (03): : 576 - 581
  • [3] FORMAL DESIGN VERIFICATION OF DIGITAL CIRCUITRY
    BUTLER, RW
    SJOGREN, JA
    RELIABILITY ENGINEERING & SYSTEM SAFETY, 1991, 32 (1-2) : 67 - 93
  • [4] Formal System Design and Verification: A Perspective
    Rajamani, Sriram
    ISOFT: PROCEEDINGS OF THE 13TH INNOVATIONS IN SOFTWARE ENGINEERING CONFERENCE, 2020,
  • [5] Getting formal verification into design flow
    Arvind, S.
    Dave, Nirav
    Katelman, Michael
    FM 2008: FORMAL METHODS, PROCEEDINGS, 2008, 5014 : 12 - +
  • [6] Practical formal verification in microprocessor design
    Jones, RB
    O'Leary, JW
    Seger, CJH
    Aagaard, MD
    Melham, TF
    IEEE DESIGN & TEST OF COMPUTERS, 2001, 18 (04): : 16 - 25
  • [7] Formal verification in intel CPU design
    O'Leary, J
    Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2004, : 152 - 152
  • [8] DESIGN OF A FORMAL ESTELLE SEMANTICS FOR VERIFICATION
    BREDEREKE, J
    GOTZHEIN, R
    VOGT, FH
    IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS, 1993, 10 : 153 - 168
  • [9] Assured VLSI design with formal verification
    Kim, JD
    Chin, SK
    COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 13 - 22
  • [10] Formal verification and hardware design with statecharts
    Philipps, J
    Scholz, P
    PROSPECTS FOR HARDWARE FOUNDATIONS: ESPRIT WORKING GROUP 8533 NADA - NEW HARDWARE DESIGN METHODS SURVEY CHAPTERS, 1998, 1546 : 356 - 389