Cloud computing is technique that provides data privacy and reliability, access control, data forwarding(sharing) without using compute-intensive re-encryption, insider threat security, and forward and backward access control. The SeDaSC technique encrypts a file with a single encryption key. Two different key shares for each of the users are generated, with the user only receiving one share. The control of a single share of a key allows the SeDaSC attitude to counter the insider threats. The other key share is stored by a trusted third party, which is called the cryptographic server. This method is applicable to usual and mobile cloud computing environments. We implement a working prototype of the SeDaSC method and assess its performance based on the time consumed during a choice of operations. We officially confirm the working of SeDaSC by using high-level Petri nets, a Z3 solver.