Automated security proofs of secret shared protocols

The data, which contain the personal, medical and financial information of the data donors, are classified as sensitive. It is required that only the authorized organizations have the right to process the sensitive data. However, nowadays, the extensive implementation of online information systems not only makes the use of data more convenient, but also provides an easier way to abuse the data. Hence, a lot of research organizations have proposed their methods for processing the sensitive data without compromising the privacy of individuals. In our thesis, we address the proof method on a specific infrastructure proposed by Dan Bogdanov. In his thesis, he considers protecting the sensitive data as a multiparty computation task. He also proposes several secret shared protocols for computing the data without leaking the privacy of any person under the assumption that only few participants can be corrupt. Our goal is to devise a method, which can automatically prove that in all secret shared protocols no party can figure out more information than he should. In this thesis, we present a framework for analyzing the security of secret shared protocols. The result of our solution is the implementation software called AutoProver, which can automatically prove the security of the secret shared protocols. Our solution is based on the theory that a real world protocol securely emulates an ideal functionality if for any real world adversary there exists a simulator in the ideal world that the real world adversary can not distinguish if it is communicating with the protocol or the simulator