Title: The Description and Validation of EKE Protocol Based on TLA
Abstract: 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.
Publication Year: 2012
Publication Date: 2012-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot