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...

Full description

Saved in:
Bibliographic Details
Main Authors: Yinyin Xiao, Kaile Su
Format: Conference Proceeding
Language:English
Subjects:
Computational modeling
DH-HEMTs
Diffie-Hellman symmetric encryption
Encryption
formal verification
Logic of Local Sessions
Protocols
security protocol
Semantics
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/CSAE.2012.6272646