AVISPA使用教程（一）

一、简介

AVISPA是一种用于自动证明网络安全协议与应用的工具集。

AVISPA的工具包集成在了一个叫SPAN的虚拟机上，而SPAN虚拟机需要下载虚拟机软件virtual box才能打开。

安装教程不在此赘述。

二、基础框架

• basic role

代码语言：javascript复制

role role_name(类型化参数) %参数变量首字母必须大写
played_by name def=   �f和=之间不能有空格
    local  %定义本地变量
    const  %常量
    init   %初始化变量
    transition %转变，记录事件的触发条件和触发后的动作
end role

• composed role 将多个basic role组合在一起，组成会话

代码语言：javascript复制

role session(类型化参数，应包含所有的basic role的类型参数）
def=
    local SA,RA,SB,RB : channel(dy)   %定义每个basic role的发送、接收信道
composition
    A(类型化参数) / B(类型化参数）
end role

• environment

代码语言：javascript复制

role environment()
def=
    const 
        a,b : agent
        aid,bid : text
        h1,h2 : hash_func
    intruder_knowedge = {a,b} %攻击者知道的知识
    composition 
        session(session的类型参数) [/ session(session的类型参数）] %将多个会话组合起来
end role

• goal

代码语言：javascript复制

goal
    %声明协议的安全目标
end goal

• environment()

代码语言：javascript复制

environment() %执行

网络安全 environment virtual 教程 虚拟机形式化分析 AVISPA 协议安全性分析

0 人点赞