基于行为时序逻辑TLA的安全协议形式化分析与检测

Formal Analysis and Check of Security Protocol Based on Temporal Logic of Actions TLA

随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。

with the insecurity of network protocol,formal analysis and check of the security protocol is very important.And model checking based on Temporal Logic of Actions TLA is one of important form validation method.This paper mainly analyses and checks H.530 protocol with HLPSL based on TLA language.