Modeling and Reasoning about States in Late Launch Based on Horn Clauses

Late Launch, which is a kind of dynamic measurement technology proposed by both Intel and AMD, offers isolated execution environment for codes needed to be protected. However, since the specifications and documents of Late Launch have hundreds of pages, they are too long and complicated to be fully covered and analyzed. A model based on Horn clauses is presented to solve the problem that there is a lack of realistic models and of automated tools for the verification of security protocols based on Late Launch. A running example is taken to show the execution details of Late Launch. Based on the example, secrecy properties of Late Launch are verified. Whats more, the automatic theorem proving tool ProVerif is used to make the verification more fast and accurate.