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

Abstract

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.