2 papers
cs.PL2021
Reasoning about Iteration and Recursion Uniformly based on Big-step Semantics
Ximeng Li, Qianying Zhang, Guohui Wang +2
A reliable technique for deductive program verification should be proven sound with respect to the semantics of the programming language. For each different language, the construct…
cs.CR2019
A Comprehensive Formal Security Analysis and Revision of the Two-phase Key Exchange Primitive of TPM 2.0
Qianying Zhang, Shijun Zhao
The Trusted Platform Module (TPM) version 2.0 provides a two-phase key exchange primitive which can be used to implement three widely-standardized authenticated key exchange protoc…