Swift语言子集SubSwift的定义主要考虑2个因素。1) Swift 语言是一种复杂的编程语言。若在定义SubSwift时，考虑Swift语言的所有语句，则太过复杂。另外，由于Blanchet演算是一种安全协议建模语言，其语言简单且功能不够强大，故不能建立从Swift到Blanchet的演算映射。2) 对已有的安全协议实施 Swift 进行分析，找出开发安全协议Swift实施所需要的核心语句。综合考虑这2个因素来定义 SubSwift 语言，并定义 SubSwift 语言的巴科斯范式，如图1所示。

SubSwift语言主要包含的语句有：表达式语句（expression）、声明语句（declaration）、分支语句（branch_statement）、控制转移语句（control_transfer_statement）。表达式语句主要包含常量（value）、变量（variable）、赋值表达式（assignment）、算术运算表达式、逻辑运算表达式（logical_statement）等。由于Blanchet演算没有涉及算术运算，故没有考虑SubSwift语言的算术运算部分。SubSwift语言表达式语句主要包含表达式的值、赋值表达式、逻辑运算表达式等。声明语句是对要进行安全协议实施中所需的常量、变量、函数、类、库等进行定义。SubSwift 语言声明语句主要包含导入声明（import_declaration）、常量声明（constant_ declaration）、变量声明（variable_ declaration）、函数声明（functions_declaration）和类声明（class_ declaration）。导入声明语句是指定Swift库文件数据分组名，该分组定义多种元素。控制转移语句用于控制代码的执行顺序，从而实现代码的跳转。SubSwift语言控制转移语句包括 return 语句、throw 语句。return 语句用于从当前执行的函数返回到主调用函数，同时传回返回值。throw 语句用于创建异常和返回代码错误信息。分支语句用于某种特定条件下执行相应代码的情形。SubSwift语言分支语句主要包括if语句和guard语句。if语句如 ：当且仅当if后的<condition>值为 true 时，执行{statements1}；当<condition>值为 false 时，并且 if 语句中有 else语句，就执行{statements2}，否则直接执行下一条语句。guard语句如：与If语句实现相同的功能，当且仅当guard后的{statement}值为true时直接跳过else语句执行下一条语句。当条件表达式为false时，就执行else语句，并跳出guard语句代码段。

2008 年，Blanchet^[27]提出一种概率进程演算——Blanchet演算，它基于PI演算和其他几种演算的思想。在Blanchet演算中，消息是位串，密码原语可看作位串到位串的函数的序列。这种演算具有概率学语义，并且所有进程的运行是多项式时间。观察等价^[10]是证明安全属性过程中使用到的主要技术之一，其基本思想是：若攻击者能够区分进程Q 和进程Q′的可能性是可忽略的，则进程 Q 观察等价于进程Q′。Blanchet演算增加一种新功能，进程执行过程中所有变量的值都存储在数组中，这是协议分析过程实现自动化的关键，比如，表示进程索引编号i中的x的变量值。数组代替链表，而链表经常用在安全协议的手工证明方面。例如，考虑（MAC,message authentication code）安全性的定义。通常，MAC安全性定义攻击者伪造MAC成功概率是可忽略的，因此，在安全性证明过程中，有个链表保存MAC算法中处理过的参数，当要证明消息m 的 MAC 时可以检查消息 m 是否在链表中。在Blanchet演算中，MAC生成算法，使用过的参数都保存在数组中，通过遍历该数组来寻找消息m。相对于人工论证的链表，数组不需要对其中插入的值进行附加说明。这样消除了许多细微且难以自动化的语法转换，便于通过等式来表示数组元素之间的关系。Blanchet 演算是一种建立安全协议抽象模型的建模语言。图2给出了Blanchet演算的巴科斯范式。

在3.1节中定义的SubSwift语言主要包含表达式语句、声明语句、分支语句、控制转移语句等。

表达式语句主要定义常量、变量、赋值表达式和逻辑表达式。表达式语句到Blanchet演算的BNF映射规则如图4所示。常量a∈value映射为Blanchet演算中的a[:T]，变量x∈variable映射为 Blanchet演算中的项x[:T]。赋值表达式assignment：x=a映射为let…in语句let y：T=simp leterm in；逻辑表达式映射为 Blanchet 演算中的（cond），逻辑与表达式logicaland:e₁＆＆e₂ 映射为 $\langle simpleterm\rangle$ ＆＆$\langle simpleterm\rangle$，逻辑或 logicalor:e ₁||e₂ 映射为$\langle simpleterm\rangle \Vert \langle simpleterm\rangle$ ，逻辑等于 Logical equan:e₁==e₂映射为 $\langle simpleterm\rangle =\langle simpleterm\rangle$，逻辑不等于logicalunequal:e !₁=e₂映射为 $\langle simpleterm\rangle <>\langle simpleterm\rangle$< 。

SubSwift语言声明语句到Blanchet演算的BNF映射关系如图5所示。SubSwift语言的声明语句主要包含导入声明、常量声明、变量声明、函数声明、类声明等。在Blanchet演算中，不存在与SubSwift中 import 语句对应的语句，因此，若安全协议SubSwift语言实施转换为Blanchet演算模型的过程中遇到import语句，则直接跳过。

Swift语言基本语句到Blanchet演算的BNF映射关系如图6所示。SubSwift语句映射为Blanchet演算语句时，任意一条SubSwift语句statement:S映射为 Blanchet 演算中输入或输出进程中的$\langle outprocess/inprocess\rangle$，每个 SubSwift 语句块code_block:{S*}映射为 Blanchet 演算中输入或输出进程中的多条语句 $\langle outprocess/inprocess\rangle *$ *，if语句if_statement:if e {P} else{Q}映射为 if $\langle cond\rangle$then $\langle outprocess\rangle$ else $\langle outprocess\rangle$，guard 语句guard_statement:guard e else {P}映射为if $\langle !cond\rangle$then $\langle outprocess\rangle$，guard语句映射为Blanchet演算中的if语句时，其条件表达式要进行取非操作。因为else后的语句块在guard语句条件不成立时执行，反之，else 后的语句块不会执行。创建类的实例new_class:let x =class(e₁,e₂,")，映射为 Blanchet演算中的 new 语句 new x :T，调用类方法class_method:class.method(e₁,e₂,")，映射为Blanchet演算中的函数fun ident $\left(seq\langle T\rangle \right)$ :T[compos]。SubSwift 语言用套接字等方法发送与接收消息，对应于Blanchet演算中out和in语句。Socket中的Send方法socket_send:socket.send(x₁,x₂,...)发送消息，映射为 out 语句 $out\left(\langle \text{channel}\rangle ,\langle term\rangle \right)$ $[;\langle inprocess\rangle$；socket 中的 Receive 方法 socket_receive:socket.receive(x₁,x₂,")接收消息，映射为in语句$(\langle channel\rangle ,\langle term\rangle )[;\langle outprocess\rangle$。

SubSwift语言和Blanchet演算是强类型语言，两者的主要区别在于，SubSwift语言中的基本类型如整型 int、单精度浮点型 float、双精度浮点型double 等都是 SubSwift 语言预先定义的；而在Blanchet 演算中，除与密码体制、签名机制相关的部分数据类型是由Blanchet演算预先定义的之外，其他类型是先声明后使用的。因此，在定义SubSwift语言到Blanchet演算的类型映射关系时，主要考虑以下2个方面：1) 对SubSwift语言中的基本数据类型，在Blanchet演算中声明一个同名的数据类型，直接进行调用；2) SubSwift语言中与密码体制、签名机制相关的数据类型需映射到Blanchet演算中对应的密码体制、签名机制中的数据类型。

应用Antrl4工具对安全协议SubSwift语言实施进行语法分析，并获取安全协议SubSwift语言实施语法分析树。首先根据SubSwift语言的词法规则开发SubSwift语言词法分析器并对安全协议SubSwift 语言实施进行词法分析，进而得到安全协议SubSwift语言实施的词法元素序列。然后根据SubSwift语言的语法规则开发SubSwift语言语法分析器，对获得的安全协议SubSwift语言实施词法元素序列进行语法分析，判断安全协议SubSwift语言实施是否符合SubSwift语言语法规则，若符合，则生成安全协议SubSwift语言实施的语法分析树。SubSwift 语言词法分析器和语法分析器开发原理如图9所示。

为开发 SubSwift 语言词法分析器和语法分析器，创建SubSwift.g4文件并存入 SubSwift语言的词法规则和语法规则。执行 SubSwift.g4 文件生成的语法分析相关文件。SubSwiftLexer.java是 SubSwift 词法分析器，将 SubSwift 代码转换为单词元素序列。SubSwiftParser.java是SubSwift语法分析器，对单词元素序列进行语法分析。SubSwift BaseListener.java 由监听器 Listener 默认实现。

5.1.1 SubSwift语言词法分析器

词法分析从左到右读入实施中的字符，并根据定义的词法规则识别并确定单词元素及其属性，从而将输入流中的字符串序列分割为单词元素序列，将其作为语法分析器的输入。每个单词元素序列是一个独立的序列 1，包括常量、关键字、标识符、运算符、分界符等。Antrl4 工具可以根据定义的SubSwift语言词法规则自动化生成SubSwift语言词法分析器SubSwiftLexer.java，在SubSwift.g4 文件中定义词法规则。在 SubSwift语言中，常量包括布尔型、数值型等，在词法规则定义中，布尔型取值为 true 或 false，即为：boolean_literal :'true' | 'false' 。整型可分为二进制数（binary_literal）、八进制数（octal_literal）等，其词法规则如图10所示。

关键字是程序语言中具有固定意义的标识符，这些标识符只能作为保留字，不能被重新定义为一般标识符。在SubSwift语言中，定义的关键字如图11所示。

安全协议 SubSwift 实施中标识符是程序语言中用来表示安全协议实体的字符串，如变量名、函数名、类名等。标识符通常由字母、数字和下划线组成，且不能以数字开头，SubSwift语言中标识符的词法规则如下。

identifier :identifier_head identifier_character? ;

identifier_head :[a-zA-Z]| '_' ;

identifier_character :[0-9]| identifier_head ;

identifier_characters :identifier_character+

运算符一般分为算术运算符、逻辑运算符、赋值运算符、关系运算符及连接运算符。在 Blanchet演算中，只有赋值运算和逻辑运算，因此主要考虑SubSwift 语言运算符中的赋值运算符和逻辑运算符。SubSwift语言中运算符的定义如图12所示。

分界符是程序语言中一个重要组成部分，通常包括括号、分号、冒号、下划线等。SubSwift语言的分界符定义如图13所示。

在SubSwift语言代码中，有些代码如空格、换行符、注释等在词法分析中可忽略，其具体词法规则定义如下。

WS :[ \n\r\t]+-> channel(HIDDEN) ;

block_comment :'/*' (block_comment|.)*? '*/'->channel(HIDDEN) ;

line_comment :'//'.*? ('\n'|EOF)->channel(HIDDEN)

其中，WS 的作用是忽略换行符、空格、制表符， Block_comment中定义的是多行注释，line_comment中定义的是单行注释，channel(HIDDEN)的作用是跳过这些字符。

5.1.2 SubSwift语言语法分析器

SubSwift语言语法分析器的输入是经词法分析器后所得到的单词元素序列。根据给定的形式文法分析并确定单词元素序列的语法组织结构，判断源程序代码语法的正确性，若源程序在语法组织结构上正确，则生成语法分析树。

根据 Antrl4 工具的文法定义规则，在SubSwift.g4 文件中添加定义的 SubSwift 语言的语法规则，编译执行之后生成的SwiftParser.java文件，即为SubSwift语言语法分析器。SubSwift的BNF，主要包括表达式语句、声明语句、分支语句和控制转换语句，根据 SubSwift 中语句的语法规范，

SubSwift.g4文件的文法规则定义如下。

statement :

expression ';' //表达式语句

| declaration ';' //声明语句

| branch_statement ';' //分支语句

| control_transfer_statement ';' //控制转换语句

SubSwift的表达式语句主要包含赋值语句和逻辑运算表达式语句。赋值语句如 variable[:Type]= identifier，逻辑运算表达式包含逻辑等于、逻辑不等于、逻辑与、逻辑或，它们分别对应于< iden tifier > == <identifier>、<identifier> != < identifier >、<identifier> ＆＆ <identifier> 及 <identifier >|| <identifier>，根据其 BNF，可以在 SubSwift.g4文件中将表达式的文法规则定义如下。

expression :

identifier[:type]

| assignment_expression

| logical_expression

SubSwift语言主要关注的声明语句有导入声明、常量声明、变量声明、函数声明及类声明。Sub Swift.g4文件中声明语句的文法规则定义如图14所示。

在SubSwift语言中，除表达式语句、声明语句之外，其他语句还包括分支语句和控制转换语句，其中，分支语句主要包括if语句和guard语句，控制转换语句主要包括return语句和throw语句，在SubSwift.g4文件中，文法规则定义如下。

branch_statement :

if_statement

| guard_statement ;

if_statement :'if ' condition_clause code_block

else_clause ;

else_clause :'else' code_block | 'else' if_statement;

guard_statement :'guard' condition_

clause 'else' code_block ;

condition_clause :expression ;

control_transfer_statement :

return_statement

| throw_statement ;

return_statement :'return' expression ;

throw_statement :'throw' expression

5.2.1 遍历安全协议SubSwift语言实施语法分析树

用 ParseTreeWalker 类遍历安全协议 SubSwift语言实施语法分析树。Antrl4工具的语法分析器编译SubSwift.g4文件时，会根据定义的SubSwift语言语法规则自动化生成语法树监听器 ParseTree Listener 接口的子接口 SwiftListener 及其默认实现SwiftBaseListener，其中包含 SubSwift 语言语法中每个规则对应的Enter方法和Exit方法。采用深度优先遍历SubSwift语言语法分析树。当树遍历器遇到SubSwift语言某个语法规则节点时，就会调用该规则所对应的 Enter 方法，并将该语法树节点的上下文传递给该规则对应的上下文对象；当树遍历器遍历完这个节点下所有的子节点之后，就会调用该规则对应的Exit方法。

5.2.2 生成Blanchet演算实施

用Antrl4工具对SubSwift语句进行分析得到的语法分析树无法按照传统的方法通过对语法分析树的节点进行移动、删除或添加等操作来获得与之对应的Blanchet演算语法树，进而获得Blanchet演算语句。故采用Antrl4工具中特有的方式——注解语法树来获取Blanchet演算语句。

注解 SubSwift 语法分析树是为了将 SubSwift语句对应的 Blanchet 演算语句存储在该 SubSwift语句语法分析树的根节点中，只要访问根节点对应的映射值即可获得某条 SubSwift 语句所对应的Blanchet演算语句。

注解 SubSwift 语法分析树的具体方法是：通过使用ParseTreeProperty类型的字段cv及帮助方法getCV()、setCV()，得到SubSwift语言输入短语所对应的Blanchet演算语句。在SubSwift语法分析树中，首先，将每棵子树转换为 Blanchet 演算语句，然后，把相关字符串关联在该子树的根节点上，在更高节点上捕获这些关联的字符串来获取更大的字符串，并关联在该节点上，最后，整个语句的根节点所关联的字符串即为整个语句转换为Blanchet演算后的结果。在SubSwift2CV.java文件中，定义转换器类 CVEmitter、字段 cv 和帮助方法getCV()、setCV()，getCV()用于获取与当前根节点所关联的字符串值，setCV()用于注解当前根节点，其代码如下。

public static class CVEmitter extends SwiftBaseListener {

ParseTreeProperty<String> cv =

new ParseTreeProperty<String>();

String getCV(ParseTree ctx) { return cv.get (ctx); }

void setCV(ParseTree ctx,String s) { cv.put (ctx,s); }

以变量声明及初始化语句为例，说明注解语法分析树的过程。根据SubSwift语言到Blanchet演算的映射模型可知：变量声明未初始化语句var x[:T]对应的 Blanchet 演算语句的 BNF 为new x :T；而变量声明与初始化语句 var x[:T]=a 对应的Blanchet演算语句的BNF为let y :T = simpleterm in。在变量声明语句语法分析树中，变量声明时是否初始化具体表现为 initializer 根节点的子树结构是否存在。此外，SubSwift 语法分析树结构中的pattern_initializer节点对应的BNF结构x[:T]=a与Blanchet演算中的y:T =simpleterm结构是对应的，通过在 pattern_initializer 节点对应的映射值中添加关键字new或let"in即可实现SubSwift变量声明语句到Blanchet演算语句的转换。

SubSwift2CV 的主要功能包括：首先接收SubSwift语言实施并进行词法分析、语法分析，进而输出该SubSwift语言实施的语法分析树，最后遍历SubSwift语言实施的语法分析树，根据所建立的安全协议 SubSwift 语言到 Blanchet 演算的转换模型，生成并输出该SubSwift语言实施所对应的Blanchet演算实施。SubSwift2CV界面主要包括 3 个区域，分别是显示输入的 SubSwift语言实施、SubSwift语言实施的语法分析树结构及对应的 Blanchet 演算实施。其界面设计如图15所示。

OpenID Connect安全协议包含客户端（client）、终端用户（end-user）和 OpenID 供应商（OpenID provider）3个主体。 OpenID Connect协议可通过隐式流（implicit flow）、授权码流（authorization code flow）和混合流（hybrid flow）3种方式进行身份认证，不同的方式决定ID Token和Access Token返回到客户端的方式不同，其消息流程也会有所区别。本文选择授权码流的方式进行身份认证，ID Token和Access Token从令牌终端中返回，客户端可以利用授权服务器发送的授权码向令牌终端请求ID Token和Access Token，这种方式可有效防止令牌泄露。OpenID Connect 协议的消息结构如图17所示。

授权码流进行身份验证的客户端首先将用户名、密码和重定向URL发送给OpenID供应商，然后接收 OpenID 供应商的公钥，最后收到来自OpenID供应商的令牌响应。因为令牌响应中的ID Token 经过数字签名，客户端收到令牌响应之后，需要验证该数字签名，若验证结果为真，则表明客户端能认证 OpenID 供应商若验证为所示时。其中OpenID 供应商首先要生成公钥和私钥，并在客户端发送令牌响应时使用生成的私钥对 ID Token 进行数字签名。当 OpenID 供应商收到客户端发送的身份信息时，将产生的公钥发送给客户端。当OpenID 供应商收到发自客户端的令牌请求时，对客户端的身份信息进行验证，验证成功后生成 ID Token和Access Token及相关参数，并向客户端发送令牌响应，执行OpenID Connect安全协议OpenID供应商、客户端 SubSwift 语言实施。结果如图18所示。结果表明客户端能够认证OpenID供应商。

首先，将获取的安全协议SubSwift语言实施输入SubSwift2CV。然后，经过词法分析及语法分析，进而生成安全协议SubSwift实施语法分析树，遍历语法分析树，从而生成安全协议Blanchet演算实施。最后，将生成的安全协议Blanchet演算实施转换为CryptoVerif工具的输入进而分析其安全性，同时获得其安全性分析结果。

实验采用的OpenID Connect源码^[38]是由Aero Gear项目提供的，该项目致力于将企业与移动端结合起来使跨平台企业移动开发变得容易，目前，该项目获得Twitter、Facebook 、Google等公司支持，分析该项目的 OpenID Connect 实施对网络空间安全具有重要意义。

OpenID Connect安全协议将OpenID供应商、客户端 SubSwift 语言实施分别导入 SubSwift2CV 工具中，输出结果如图19和图20所示。整理SubSwift2CV工具生成的OpenID Connect安全协议Blanchet演算实施，并将其转化为CryptoVerif语句后输入Crypto Verif工具中，进而得到的安全性分析结果如图21所示。结果表明客户端能够认证OpenID供应商。

用同样的方法，对Oauth2.0安全协议SubSwift语言实施和生成的Blanchet演算实施的安全性分别进行分析，结果如图22和图23所示。

由图22和图23可知，Oauth2.0协议SubSwift语言实施和Blanchet演算实施的安全性分析结果是一致的，这表明客户端无法认证授权服务器，即当客户端收到授权码时不能够确定该授权码是否来自授权服务器。因为授权服务器向客户端发送授权码的过程中，没有采用数字签名机制，所以攻击者能获得其授权码，并对其进行篡改。

同样地，对 TLS 安全协议 SubSwift 语言实施和生成的 Blanchet 演算实施的安全性分别进行分析，结果如图24和图25所示。

由图24和图25可知，TLS安全协议SubSwift语言实施和Blanchet演算实施的安全性分析结果是一致的，这表明在客户端与服务器通信的过程中，能够保证预主密钥的保密性，且客户端能够认证服务器。