Design And Formal Analysis Of TPM-based Protocols For IaaS And SaaS

Cloud computing is the further development of distributed computing, parallel processingand grid computing. It is the undergoing profound change in the field of information technology.The U.S. National Institute of Standards Technology divided cloud computing services into threelayers: Infrastructure-as-a-Service (IaaS), Platform-as-a-Service (PaaS), Software-as-a-Service(SaaS). Cloud computing subverts the concept of a traditional computer, bringing greatadvancement of efficiency on accessing to and using of the computing resources. However, italso brings great challenges on the user’s privacy and the safety of data. In order to getbreakthrough on resolving the cloud computing security issues, a number of key technology hasbeen raised, Trusted Computing is one of these. Its very nature is adding the trusted computingtechnology into the cloud computing, using a reliable manner to provide the cloud computingservices. Currently, the research of trusted cloud computing is mainly around IaaS and SaaS.This paper bases on security needs of the trusted cloud computing, and makes furtherimprovement and optimization on the basis of existing research. And it ultimately gives thedesign of IaaS and SaaS protocols. The protocols define the interaction manner between thecloud function module, the service renting party and the trusted third party; and it establishes atrust relationship between the three. The main contents are:In IaaS, Eucalyptus is an open source IaaS framework implementation which is used forresearch. However, there is no paper describes how to use all the modules of Eucalyptus tosupply security infrastructure service. This paper divides infrastructure service into five steps,and designs protocols which based on Trusted Platform Module (TPM) to achieve these steps.In SaaS, when SaaS acquires computing and storage resources from underlying IaaS, Thesoftware service process can be divided into two phrases, and it is implemented under aTPM-based protocol.The design of IaaS and SaaS protocol follows from the cloud computing servicehierarchical ideas. IaaS and SaaS implement their duties, relying on each other. During thedesigning of protocols, the use of TPM is strictly standardized to avoid operation errors inreferences[41,42,44,46].Whether the IaaS and SaaS services can meet the security needs of trusted computing isinduced to whether the protocols can achieve the desired security goals and the confidentiality ofnegotiated secret key (if has). The protocols is tested by Scyther and proved in the model ofComputational Protocol Composition Logic (CPCL).There are nature advantages of simple processing and easy reasoning in proving traceproperties by the provement of CPCL. But not like authentication, confidentiality is not a traceproperty. Rreference[48] extended CPCL logic system to induce the confidentiality property intosome trace property which meets specific needs, but the conclusion is limited in symmetricencryption schemes. This paper extend the conclusion to both symmetric and asymmetricencryption schemes. All the protocols pass the examination of Scyther and are made securityproof by CPCL, so the security of IaaS and SaaS services is generalized.