Object-Oriented Approach to Specify Secret Sharing Protocol in Security Critical System Using Formal Method

Malaysian Journal of Computer Science

Mohammad Zahidur Rahman¹  Yew Kok Meng¹  Sai Peck Lee¹ 

关键词: Formal method;    secret sharing;   

DOI  :  

学科分类：社会科学、人文和艺术（综合）

来源: University of Malaya * Faculty of Computer Science and Information Technology

【 摘 要 】

Computers are being used increasingly in different security critical systems like electronic commerce and health care systems. The formal analysis turns out to be very useful that its application should be routine for financial and security critical systems. To win the confidence of users of a secured system, like secure secret sharing protocol, there is no other alternative than the formal method. In this paper, we first briefly introduce the secret sharing system and Object-Z formal specification tool. Then we present our design of the secret sharing scheme. In our model, the participating user and the information sharing authority dealer are modeled. To exchange information securely between users and the dealer, private channels are used. Broadcast channel is used for open information exchange. Both types of channels have been modeled. The model is formally specified by introducing the concept of combine object for collecting secret shares and for checking whether they lie in the perfect secret sharing scheme. We finally conclude with our experience.

【 授权许可】

Unknown