The Description and Validation of EKE Protocol Based on TLA
Shigong Long · Journal of Guizhou University · 2012
The temporal logic of action(TLA) was a new logic put forward by Lesilie Lamport in 1990s,modeling the concurrent system to relieve the pressure caused by the state space explosion to some extent,and it can express model process and system attributes in a use language at the same time.This paper first introduces the syntax and semantics of the temporal logic of action,and then taking EKE protocol for example,specifies the EKE protocol with TLA+ based on the temporal logic of actions,uses TLA for modeling,and then describes the EKE protocol with the language TLA+ of the temporal logic of action,and finally uses the model checker TLC for analysis to get the result that there exists middle-man's reply attack.