Geopriv协议形式化分析与模型检测
开篇：润墨网以专业的文秘视角，为您筛选了一篇Geopriv协议形式化分析与模型检测范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘 要：在协议的形式化检测中，欧共体支助的基于TLA的大型项目AVISPA，其以HLPSL为描述语言，本文实现了基于TLA的geopriv协议的形式化分析与检测，通过检测，发现Geopriv协议在一定条件下，是可以攻破的，并发现该协议的攻击，给出了攻击路径。
中图分类号：TP301
模型检测是一种用于有限状态并发系统自动验证技术。模型检测未来的研究方向：研究利用抽象技术，组合推理，和对称性来减少状态爆炸的问题。对验证参数化设计方法进行研究。开发实时和混合系统实用工具。结合演绎验证。为系统设计适合于开发的工具界面。
1 行为时序逻辑概述
行为时序逻辑（TemporalLogicofActions，简称TLA）[2]由美国学者LesilieLamport提出。行为时序逻辑TLA是一种对并发系统进行描述与验证的逻辑。
2 AVISPA概述
AVISPA工具提供了一套建立和分析协议安全的应用软件[3]。协议用高级协议说明语言HLPSL来建模，以描述协议和协议的的安全性质。
AVISPA工具有四个后台：OFMC，CL-AtSe，SATMC和TA4SP；IF就是被设计来方便这些后台分析这些输入的语言。而且，这些分析方法是部分互补的而不是等价的，所以，不同的分析方法可能产生不同的分析结果。
3 Geopriv协议的形式化与AVISPA检测
Geopriv协议有目标（T）、位置信息（LI）、位置服务器（LS）、位置接收端（LR）。他们之间的信息交换如图1所示。
图1 Geopriv协议结构图
因篇幅原因，下面仅给出部分基本角色的定义，具体用HLPSL建模该协议的描述语言如下：
roletarget（
T，LS，LR：agent，
K_T，K_LS，K_LR：public_key，
H：hash_func，
Snd_LR，Snd_LS，Rcv：channel（dy））played_byTdef=
local
State：nat，
N1：text，
P_T：public_key，
Psi_LR：hash（public_key），
LI，TS：text，
GR：hash_func
initState：=1
transition
1.State=1/＼Rcv（{LR}_K_T.{{T.N1'}_K_T.Psi_LR'}_inv（K_LR））
=|>State'：=3/＼P_T'：=new（）
/＼Snd_LR（{{N1'}_K_LR.H（P_T'）}_inv（K_T））
/＼witness（T，LR，lr_T_N1，N1'）
/＼wrequest（T，LR，t_LR_Psi_LR，Psi_LR'）
/＼GR'：=new（）
/＼Snd_LS（{GR'.Psi_LR'.H（P_T'）}_inv（P_T'）.P_T'）
/＼witness（T，LS，ls_T_GR，GR'）
/＼LI'：=new（）
/＼secret（LI'，li，{T，LS，LR}）
/＼secret（（GR'（LI'）），filtered_LI，{T，LS，LR}）
/＼TS'：=new（）
/＼Snd_LS（{TS'.{LI'.H（P_T'）}_K_LS}_inv（P_T'）.P_T'）
/＼witness（T，LR，lr_T_filtered_LI，（GR'（LI'）））
/＼witness（LS，LR，ls_LR_P_LR，LS）
endrole
rolelocationServer（
T，LS，LR：agent，%butLSdoesnotactuallyuseidentityofTandLR
Psi_Table：（hash（public_key）.hash（public_key）.hash_func）set，
K_LS：public_key，
H：hash_func，
Snd，Rcv：channel（dy））played_byLSdef=
localState：nat，
P_T，P_LR：public_key，
N2：text，
Psi_LR：hash（public_key），
LI，TS：text，
GR：hash_func
initState：=5
transition
5.State=5/＼Rcv（{GR'.Psi_LR'.H（P_T'）}_inv（P_T'）.P_T'）
=|>State'：=7/＼Psi_Table'：=cons（Psi_LR'.H（P_T'）.GR'，Psi_Table）
7.State=7/＼Rcv（{TS'.{LI'.H（P_T）}_K_LS}_inv（P_T）.P_T）
=|>State'：=9
9.State=9/＼Rcv（{H（P_LR'）.H（P_T）.N2'}_inv（P_LR'）.P_LR'）