Design and formal verification of DZMBE+

Document Type: ORIGINAL RESEARCH PAPER

Authors

Abstract

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.

Keywords


[1] Shimshon Berkovits. How to broadcast a secret. In DonaldW. Davies, editor, Advances in Cryptology EUROCRYPT 91, volume 547 of Lecture Notes in Computer Science, pages 535-541. Springer Berlin Heidelberg, 1991. ISBN 978-3-540-54620-7.

 

[2] Amos Fiat and Moni Naor. Broadcast encryption. In DouglasR. Stinson, editor, Advances in Cryptology CRYPTO 93, volume 773 of Lecture Notes in Computer Science, pages 480-491. Springer Berlin Heidelberg, 1994. ISBN 978-3-540 57766-9. doi: 10.1007/3-540-48329-2-40.

 

[3] Paolo DArco and DouglasR. Stinson. Fault tolerant and distributed broadcast encryption. In Marc Joye, editor, Topics in Cryptology CTRSA 2003, volume 2612 of Lecture Notes in Computer Science, pages 263-280. Springer Berlin Heidelberg, 2003. ISBN 978-3-540-00847-7. doi:10.1007/3-540-36563-X-18.

 

[4] Jung Hee Cheon, Nam-Su Jho, Myung-Hwan Kim, and Eun Sun Yoo. Skipping, cascade, and combined chain schemes for broadcast encryption. IEEE Transactions on Information Theory, 54(11):5155-5171, 2008.

 

[5] Yanli Chen and Geng Yang. An efficient broadcast encryption scheme for wireless sensor network. pages 3138-3141. IEEE Press, 2009.

 

[6] In Tae Kim and Seong Oun Hwang. An efficient identity-based broadcast signcryption scheme for wireless sensor networks. In Wireless and Pervasive Computing (ISWPC), 2011 6th International Symposium on, pages 1-6. 2011. doi:10.1109/ISWPC.2011.5751323.

 

[7] Jeffrey B. Lotspiech. Broadcast encryption versus public key cryptography in content protection systems. In Proceedings of the ninth ACM workshop on Digital rights management, DRM'09, pages 39-46. ACM, New York, NY, USA, 2009. ISBN 978-1-60558-779-0. doi:10.1145/1655048.1655055.

 

[8] Hongxia Jin and Jeffrey Lotspiech. Efficient traitor tracing for clone attack in content protection. In Proceedings of the 2011 ACM Symposium on Applied Computing, SAC '11, pages 1544-1549. ACM, New York, NY, USA, 2011. ISBN 978-1-4503-0113-8. doi: 10.1145/1982185.1982513.

 

[9] Ccile Delerable, Pascal Paillier, and David Pointcheval. Fully Collusion Secure Dynamic Broadcast Encryption with Constant-Size Cipher-texts or Decryption Keys, volume 4575 of Lecture Notes in Computer Science, pages 39-59. Springer Berlin Heidelberg, 2007. ISBN 978-3-540-73488-8.

 

[10] Dan Boneh and Brent Waters. A fully collusion resistant broadcast, trace, and revoke system. In Proceedings of the 13th ACM conference on Computer and communications security, CCS'06, pages 211-220. ACM, New York, NY, USA, 2006. ISBN 1-59593-518-5. doi: 10.1145/1180405.

1180432.

 

[11] Ik Rae Jeong. Efficient secret broadcast in the broadcasting networks. Communications Letters, IEEE, 13(12):1001-1003, 2009.

 

[12] Nelly Fazio and IrippugeMilinda Perera. Outsider-anonymous broadcast encryption with sub-linear ciphertexts. In Marc Fischlin, Johannes Buchmann, and Mark Manulis, editors, Public Key Cryptography PKC 2012, volume 7293 of Lecture Notes in Computer Science, pages 225-242. Springer Berlin Heidelberg, 2012. ISBN 978-3-642-30056-1. doi:10.1007/978-3-642-30057-8-14.

 

[13] Benot Libert, KennethG. Paterson, and Eliza bethA. Quaglia. Anonymous broadcast encryption: Adaptive security and efficient constructions in the standard model. In Marc Fischlin, Johannes Buchmann, and Mark Manulis, editors, Public Key Cryptography PKC 2012, volume 7293 of Lecture Notes in Computer Science, pages 206-224. Springer Berlin Heidelberg, 2012. ISBN 978-3-642-30056-1. doi: 10.1007/978-3-642-30057-8-13.

 

[14] Xinjun Du, Ying Wang, Jianhua Ge, and Yumin Wang. An id-based broadcast encryption scheme for key distribution. Broadcasting, IEEE Transactions on, 51(2):264-266, 2005.

 

[15] Wu Danfei and Zhang Weimin. Authenticated broadcast encryption with short ciphertexts and private keys. In Multimedia Technology (ICMT), 2011 International Conference on, pages 218-221. 2011. doi:10.1109/ICMT.2011.6001984.

 

[16] Dalit Naor, Moni Naor, and Jeff Lotspiech. Revocation and tracing schemes for stateless receivers. In Joe Kilian, editor, Advances in Cryptology CRYPTO 2001, volume 2139 of Lecture Notes in Computer Science, pages 41-62. Springer Berlin Heidelberg, 2001. ISBN 978-3-540-42456-7. doi:10.1007/3-540-44647-8-3.

 

[17] Xiaoming Wang and Zhiwei Liao. A secure encryption protocol for ad hoc networks. In Information Science and Engineering (ISISE), 2010 International Symposium on, pages 578-581. 2010. doi: 10.1109/ISISE.2010.144.

 

[18] Wenliang Du and Mikhail J. Atallah. Secure multi-party computation problems and their applications: a review and open problems. In Proceedings of the 2001 workshop on New security paradigms, NSPW '01, pages 13-22. ACM, New York, NY, USA, 2001. ISBN 1-58113-457-6. doi:10.1145/508171.508174.

 

[19] Andrew C. Yao, Andrew C. Yao, Andrew C. Yao, and Andrew C. Yao. Protocols for secure computations. In Foundations of Computer Science, 1982. SFCS '08. 23rd Annual Symposium on, pages 160-164. 1982. doi:10.1109/SFCS.1982.38.

 

[20] N. Maheshwari and K. Kiyawat. Structural framing of protocol for secure multiparty cloud computation. In Modeling Symposium (AMS), 2011 Fifth Asia, pages 187-192.

 

[21] Ueli Maurer. Secure multi-party computation made simple. In Stelvio Cimato, Giuseppe Persiano, and Clemente Galdi, editors, Security in Communication Networks, volume 2576 of Lecture Notes in Computer Science, pages 14-28. Springer Berlin Heidelberg, 2003. ISBN 978-3-540-00420-2. doi:10.1007/3-540-36413-7-2.

 

[22] Ronald Cramer, Ivan Damgrd, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient multiparty computations secure against an adaptive adversary. In Jacques Stern, editor, Advances in Cryptology EUROCRYPT 99, volume 1592 of Lecture Notes in Computer Science, pages 311-326. Springer Berlin Heidelberg, 1999. ISBN 978-3-540-65889-4. doi: 10.1007/3-540-48910-X 22.

 

[23] R. Canetti. Universally composable security: a new paradigm for cryptographic protocols. In Foundations of Computer Science, 2001. Proceedings. 42nd IEEE Symposium on, pages 136-145. 2001. doi:10.1109/SFCS.2001.959888.

 

[24] B. Pfitzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. In Security and Privacy, 2001. S P 2001. Proceedings. 2001 IEEE Symposium on, pages 184-200. 2001. doi:10. 1109/SECPRI.2001.924298.

 

[25] Ran Canetti. Security and composition of multiparty cryptographic protocols. Journal of Cryptology: the journal of the International Association for Cryptologic Research, 13(1):143-202, 2000.

 

[26] Mikhail J. Atallah and Keith B. Frikken. Securely outsourcing linear algebra computations. In Proceedings of the 5th ACM Symposium on

Information, Computer and Communications Security, ASIACCS '10, pages 48-59. ACM, New York, NY, USA, 2010. ISBN 978-1-60558-936-7. doi:10.1145/1755688.1755695.

 

[27] Adi Shamir. How to share a secret. Commun. ACM, 22(11):612-613, 1979.

 

[28] Ronald Cramer, Ivan Damgrd, and JesperB. Nielsen. Multiparty computation from threshold homomorphic encryption. In Birgit Pfitzmann, editor, Advances in Cryptology EUROCRYPT 2001, volume 2045 of Lecture Notes in Computer Science, pages 280-300. Springer Berlin Heidelberg, 2001. ISBN 978-3-540-42070-5. doi:10.1007/3-540-44987-6-18.

 

[29] Moni Naor and Benny Pinkas. Efficient oblivious transfer protocols. In Proceedings of the twelfth annual ACM-SIAM symposium on Discrete algorithms, SODA '01, pages 448-457. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 2001. ISBN 0-89871-490-7.

 

[30] Lin Keng-Pei and Chen Ming-Syan. On the design and analysis of the privacy-preserving svm classifier. Knowledge and Data Engineering, IEEE Transactions on, 23(11):1704-1717, 2011.

 

[31] Dung Luong The, Bao Ho Tu, Binh Nguyen The, and Hoang Tuan-Hao. Privacy preserving classification in two-dimension distributed data. In Knowledge and Systems Engineering (KSE), 2010 Second International Conference on, pages 96-103.

 

[32] Z. Yu and N. Zhang. Achieving privacy preserving computation on data grids. In Computers and Communications, 2007. ISCC 2007. 12th IEEE Symposium on, pages 763-768.

 

[33] Yang Piyi, Cao Zhenfu, Dong Xiaolei, and T. A. Zia. An efficient privacy preserving data aggregation scheme with constant communication overheads for wireless sensor networks. Communications Letters, IEEE, 15(11):1205-1207, 2011.

 

[34] D. K. Mishra and M. Chandwani. A zero-hacking protocol for secure multiparty computation using multiple ttp. In TENCON 2008 - 2008 IEEE Region 10 Conference, pages 1-6.

 

[35] Gavin Lowe. Breaking and fixing the Needham Schroeder Public-Key Protocol using FDR, volume 1055 of Lecture Notes in Computer Science, chapter 10, pages 147-166. Springer Berlin Heidelberg, 1996.

 

[36] Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: the spi calculus. In Proceedings of the 4th ACM conference on Computer and communications security, CCS '97, pages 36-47. ACM, New York, NY, USA, 1997. ISBN 0-89791-912-2. doi:10.1145/266420.266432.

 

[37] Martín Abadi and Bruno Blanchet. Computer Assisted Verification of a Protocol for Certified Email, volume 2694 of Lecture Notes in Computer Science, chapter 17, pages 316-335. Springer Berlin Heidelberg, 2003.

 

[38] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Computer Security Foundations Workshop, 2001. Proceedings. 14th IEEE, pages 82-96. 2001. doi:10.1109/CSFW.2001.930138.

 

[39] Steve Kremer and Mark Ryan. Analysis of an electronic voting protocol in the applied pi calculus. In Mooly Sagiv, editor, Programming Languages and Systems, volume 3444 of Lecture Notes in Computer Science, pages 186-200. Springer Berlin Heidelberg, 2005. ISBN 978-3-540-25435-5. doi:10.1007/978-3-540-31987-0-14.

 

[40] Atsushi Fujioka, Tatsuaki Okamoto, and Kazuo Ohta. A practical secret voting scheme for large scale elections. In Jennifer Seberry and Yu-liang Zheng, editors, Advances in Cryptology - AUSCRYPT '92, volume 718 of Lecture Notes in Computer Science, pages 244-251. Springer Berlin Heidelberg, 1993. ISBN 978-3-540-57220-6. doi:10.1007/3-540-57220-1-66.

 

[41] Stphanie Delaune, Steve Kremer, and Mark Ryan. Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster, volume 6000 of Lecture Notes in Computer Science, chapter 18, pages 289-309. Springer Berlin Heidelberg, 2010.

 

[42] R. Kusters and T. Truderung. An epistemic-approach to coercion resistance for electronic voting protocols. In Security and Privacy, 2009 30th IEEE Symposium on, pages 251-266. 2009. doi:10.1109/SP.2009.13.

 

[43] Steve Kremer, Mark Ryan, and Ben Smyth. Election verifiability in electronic voting protocols. In Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou, editors, Computer Security ESORICS 2010, volume 6345 of Lecture Notes in Computer Science, pages 389-404. Springer

Berlin Heidelberg, 2010. ISBN 978-3-642-15496-6. doi:10.1007/978-3-642-15497-3-24.

 

[44] Ben Adida. Helios: web-based open-audit voting. pages 335-348. USENIX Association, 2008.

 

[45] M.R. Clarkson, S. Chong, and A.C. Myers. Civitas: Toward a secure voting system. In Security and Privacy, 2008. SP 2008. IEEE Symposium on, pages 354-368. 2008. doi:10.1109/SP.2008.32.

 

[46] Ben Smyth, Mark Ryan, Steve Kremer, and Mounira Kourjieh. Towards automatic analysis of election verifiability properties. In Alessandro Armando and Gavin Lowe, editors, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, volume 6186 of Lecture Notes in Computer Science, pages 146-163. Springer Berlin Heidelberg, 2011. ISBN 978-3-642-16073-8. doi:10.1007/978-3-642-16074-5-11.

 

[47] Liqun Chen and Mark Ryan. Attack, solution and verification for shared authorisation data in tcg tpm. In Pierpaolo Degano and JoshuaD.

Guttman, editors, Formal Aspects in Security and Trust, volume 5983 of Lecture Notes in Computer Science, pages 201-216. Springer Berlin

Heidelberg, 2010. ISBN 978-3-642-12458-7. doi:10.1007/978-3-642-12459-4-15.

 

[48] M. Backes, M. Maffei, and D. Unruh. Zero-knowledge in the applied pi calculus and automated verification of the direct anonymous attestation protocol. In Security and Privacy, 2008. SP 2008. IEEE Symposium on, pages 202-215. 2008. doi:10.1109/SP.2008.23.

 

[49] Bruno Blanchet and Avik Chaudhuri. Automated formal analysis of a protocol for secure file sharing on untrusted storage. In Proceedings of the 29th IEEE Symposium on Security and Privacy (S&P'08), pages 417-431. IEEE, 2008.

 

[50] Martín Abadi, Bruno Blanchet, and Cedric Four-net. Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur., 10(3):9, 2007.

 

[51] Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, and Sergio Maffeis. Keys to the cloud: formal analysis and concrete attacks on encrypted web storage. In Proceedings of the Second international conference on Principles of Security and Trust, POST'13, pages 126-146. Springer-Verlag, Berlin, Heidelberg, 2013. ISBN 978-3-642-36829-5. doi:10.1007/978-3-642-36830-1-7.

 

[52] Jannik Dreier, Pascal Lafourcade, and Yassine Lakhnech. Formal Verification of e-Auction Protocols, volume 7796 of Lecture Notes in Computer Science, chapter 13, pages 247-266. Springer Berlin Heidelberg, 2013.

 

[53] Myrto Arapinis, Vronique Cortier, Steve Kremer, and Mark Ryan. Practical Everlasting Privacy, volume 7796 of Lecture Notes in Computer Science, chapter 2, pages 21-40. Springer Berlin Heidelberg, 2013.

 

[54] Denise Demirel, Jeroen Van De Graaf, and Roberto Arajo. Improving helios with everlasting privacy towards the public. In Proceedings of the 2012 international conference on Electronic Voting Technology/Workshop on Trustworthy Elections, EVT/WOTE'12, pages 8-8. USENIX Association, Berkeley, CA, USA, 2012.

 

[55] Tal Moran and Moni Naor. Receipt-Free Universally-Verifiable Voting with Everlasting Privacy, volume 4117 of Lecture Notes in Computer Science, chapter 22, pages 373-392. Springer Berlin Heidelberg, 2006.

 

[56] Martín Abadi and Cedric Fournet. Mobile values, new names, and secure communication. SIGPLAN Not., 36(3):104-115, 2001.

 

[57] Robin Milner. Communicating and mobile systems: the pi-calculus.

Cambridge University Press, 1999.

 

[58] Danny Dolev and Andrew C. Yao. On the security of public key protocols. Technical report, Stanford University, 1981.

 

[59] M. S. Mohammadi and A. G. Bafghi. A dynamic, zero-message broadcast encryption scheme based on secure multiparty computation. In Information Security and Cryptology (ISCISC), 2012 9th International ISC Conference on, pages 12-17.

 

[60] V. I. Nechaev. Complexity of a determinate algorithm for the discrete logarithm. Mathematical Notes, 55(2):165-172, 1994.

 

[61] Hung-Yu Lin and Lein Harn. Fair reconstruction of a secret. Inf. Process. Lett., 55(1):45-47, 1995.

 

[62] Dan Boneh, Craig Gentry, and Brent Waters. Collusion resistant broadcast encryption with short ciphertexts and private keys. In Victor Shoup, editor, Advances in Cryptology CRYPTO 2005, volume 3621 of Lecture Notes in Computer Science, pages 258-275. Springer Berlin Heidelberg, 2005. ISBN 978-3-540-28114-6.

 

[63] Adrian Perrig. Efficient collaborative key management protocols for secure autonomous group communication. In International Workshop on Cryptographic Techniques and E-Commerce CrypTEC '99, pages 192-202.