AVISPA使用教程（一）

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

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

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
    %声明协议的安全目标
end goal

environment() %执行