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 条
  • [41] Method of formal design and verification of OS on assembly layer
    Qian Z.-J.
    Huang H.
    Song F.-M.
    Qian, Zhen-Jiang (tony_h@sina.com), 1600, Chinese Academy of Sciences (27): : 3143 - 3157
  • [42] Formal Verification for Embedded Systems Design Based on MDE
    Moreira do Nascimento, Francisco Assis
    da Silva Oliveira, Marcio Ferreira
    Wagner, Flavio Rech
    ANALYSIS, ARCHITECTURES AND MODELLING OF EMBEDDED SYSTEMS, 2009, 310 : 159 - +
  • [43] FORMAL VERIFICATION RAPIDLY CHEEKS ASIC DESIGN REVISIONS
    ONEILL, B
    COMPUTER DESIGN, 1995, 34 (08): : 104 - 105
  • [44] Formal for Everyone - Challenges in Achievable Multicore Design and Verification
    Stewart, Daryl
    Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012), 2012, : 186 - 186
  • [45] Integration of formal verification with real-time design
    Krasovec, G
    Shankar, N
    Ward, P
    SECOND WORKSHOP ON OBJECT-ORIENTED REAL-TIME DEPENDABLE SYSTEMS, PROCEEDINGS OF WORDS '96, 1996, : 128 - 136
  • [46] A formal verification environment for railway signaling system design
    Bernardeschi, C
    Fantechi, A
    Gnesi, S
    Larosa, S
    Mongardi, G
    Romano, D
    FORMAL METHODS IN SYSTEM DESIGN, 1998, 12 (02) : 139 - 161
  • [47] Design and Formal Verification of a VANET Lightweight Authentication Protocol
    Zhao, Guolei
    Wang, Ruinyun
    Wang, Xuejian
    Zhu, Xianwei
    2018 IEEE 18TH INTERNATIONAL CONFERENCE ON COMMUNICATION TECHNOLOGY (ICCT), 2018, : 513 - 517
  • [48] Introducing digital circuits design and formal verification concurrently
    Amblard, P
    Lagnier, F
    Levy, M
    MICROELECTRONICS EDUCATION, 2000, : 261 - 264
  • [49] Semi-formal specifications and formal verification improving the digital design: some statistics
    Torres, D.
    Cortez, J.
    Gonzalez, R. E.
    JOURNAL OF APPLIED RESEARCH AND TECHNOLOGY, 2009, 7 (01) : 15 - 40
  • [50] Formal Verification
    Meenakshi, B.
    RESONANCE-JOURNAL OF SCIENCE EDUCATION, 2005, 10 (05): : 26 - 38