The DH exponentiation extension in a verification logic of local sessions

Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can verify many interesting properties for complex security protocols. However, It does not discuss the DH key exchange and the related properties. In this paper, we extend the original LLS with DH exponentiation. After revising some primary concepts and definitions, a new theorem called DH-Secrecy Properties is proposed and proved. Avoiding influencing the proof of the former axioms, our extension enlarges the range of applicability of LLS.