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 条
  • [31] A Formal Verification Environment for Railway Signaling System Design
    Cinzia Bernardeschi
    Alessandro Fantechi
    Stefania Gnesi
    Salvatore Larosa
    Giorgio Mongardi
    Dario Romano
    Formal Methods in System Design, 1998, 12 : 139 - 161
  • [32] 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
  • [33] Design of Software Security Verification with Formal Method Tools
    Jang, Seung-Ju
    Ryoo, Jungwoo
    Lee, ChangYeol
    INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2006, 6 (9B): : 163 - 167
  • [34] Preserving Design Hierarchy Information for Polynomial Formal Verification
    Drechsler, Rolf
    Mahzoon, Alireza
    PROCEEDINGS OF THE 2022 IFIP/IEEE 30TH INTERNATIONAL CONFERENCE ON VERY LARGE SCALE INTEGRATION (VLSI-SOC), 2022,
  • [35] Formal verification helps stamp out design bugs
    Ajluni, C
    ELECTRONIC DESIGN, 1998, 46 (27) : 67 - +
  • [36] Formal Design and Verification of Memory Management Unit Microprocessor
    Yang, Hongwei
    Ma, Dianfu
    2019 IEEE 2ND INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATION ENGINEERING TECHNOLOGY (CCET), 2019, : 124 - 128
  • [37] FORMAL VERIFICATION - IS IT PRACTICAL FOR REAL-WORLD DESIGN
    CAMURATI, P
    CHIN, SK
    FOURMAN, M
    PRINETTO, P
    TAKAHARA, A
    IEEE DESIGN & TEST OF COMPUTERS, 1989, 6 (06): : 50 - 58
  • [38] Design and formal verification of a CEM protocol with transparent TTP
    Liu, Zhiyuan
    Pang, Jun
    Zhang, Chenyi
    FRONTIERS OF COMPUTER SCIENCE, 2013, 7 (02) : 279 - 297
  • [39] A Formal Verification Approach to the Design of Synthetic Gene Networks
    Yordanov, Boyan
    Belta, Calin
    2011 50TH IEEE CONFERENCE ON DECISION AND CONTROL AND EUROPEAN CONTROL CONFERENCE (CDC-ECC), 2011, : 4873 - 4878
  • [40] Design and formal verification of a CEM protocol with transparent TTP
    Zhiyuan Liu
    Jun Pang
    Chenyi Zhang
    Frontiers of Computer Science, 2013, 7 : 279 - 297