金融信息安全(9)-形式化方法

1、 安全保障是对实体满足安全需求的信心。信心是建立在安安全保障是对实体满足安全需求的信心。信心是建立在安全保障工具所提供的事实基础上。全保障工具所提供的事实基础上。 安全保障技术可以分为形式化方法、非形式化方法和半形安全保障技术可以分为形式化方法、非形式化方法和半形式化方法。式化方法。 非形式化方法使用非形式化方法使用 自然语言来描述规范以及对断言的证明。自然语言来描述规范以及对断言的证明。 半形式化方法在非形式化方法的基础上使用了某些严密性控制方半形式化方法在非形式化方法的基础上使用了某些严密性控制方法。法。 形式化方法使用了数学和带分析工具的、机器能够解释的语言，形式化方法使用了数学和带分析

2、工具的、机器能够解释的语言，这种语言具有严格的语法和明确的语义。这种语言具有严格的语法和明确的语义。 为建立为建立“强壮强壮”的安全系统，需要使用形式化方法，建立的安全系统，需要使用形式化方法，建立系统的一个数学或逻辑模型及其需求，分析任何一种可能系统的一个数学或逻辑模型及其需求，分析任何一种可能模式的失败并计算出失败的可能性，确定系统是否满足需模式的失败并计算出失败的可能性，确定系统是否满足需求。求。 尽管理论上形式化方法可以用在系统开发的各个阶段，但是，从目前的技术水平来看，由于系统本身的复杂度，完全形式化地证明一个系统实现是安全的，是不可行的。需求需求分析和接收需分析和接收需求求模型模型

3、外 部 接 口外 部 接 口 AM1 抽象机抽象机AM2 原语级原语级AMn 可证明是内部一可证明是内部一致的致的称为高级规范称为高级规范该抽象机代表该抽象机代表了底层的系统了底层的系统规范规范最低层规范，最低层规范，是硬件和软件是硬件和软件的结合的结合 SPECIAL是是SRI International 开发的一阶逻辑语开发的一阶逻辑语言，是一种非过程性的、强类型的规范语言，可言，是一种非过程性的、强类型的规范语言，可在不知道实现细节的情况下描述输入、约束、错在不知道实现细节的情况下描述输入、约束、错误和输出。误和输出。 语言包括大量的内置操作符、比如语言包括大量的内置操作符、比如UNIO

4、N和和DIFF等；逻辑操作符，等；逻辑操作符，如与、或、蕴含等、全称量词和存在量词；如与、或、蕴含等、全称量词和存在量词；IF/THEN/ELSE结构、结构、算术标识符，并可区分变量的算术标识符，并可区分变量的 新旧值。新旧值。 规范可表示为一个模块，多个模块组合在一起，用以描述一个系规范可表示为一个模块，多个模块组合在一起，用以描述一个系统。一个模块规范分为几个部分，分别描述类型、参数、断言和统。一个模块规范分为几个部分，分别描述类型、参数、断言和函数。其中函数定义状态和变量，可以是模块私有的，也可以定函数。其中函数定义状态和变量，可以是模块私有的，也可以定义为可见的。义为可见的。 原型验证

5、系统原型验证系统 为关键系统创建良好的规范，并证明相关的属性。为关键系统创建良好的规范，并证明相关的属性。 不存在中的那些连续的抽象层和抽象层之间的映射关系。不存在中的那些连续的抽象层和抽象层之间的映射关系。 符号模型检查器符号模型检查器 基于控制树逻辑（），在谓词演算的基础上添加了基于控制树逻辑（），在谓词演算的基础上添加了个时态连接词。个时态连接词。 将系统描述为有向图，图中的所有节点代表系统状态，并标出所将系统描述为有向图，图中的所有节点代表系统状态，并标出所满足的命题，使用箭头连接节点表示系统转换。满足的命题，使用箭头连接节点表示系统转换。 密码协议分析器密码协议分析器 采用采用pro

6、log编写，验证方法建立在一组状态机相互交换的基础上，编写，验证方法建立在一组状态机相互交换的基础上，用户指定非安全的状态，并且证明这些状态是不可达的。用户指定非安全的状态，并且证明这些状态是不可达的。 时态需求语言（），可用来描述密钥分配或时态需求语言（），可用来描述密钥分配或密钥管理协议的一般需求。密钥管理协议的一般需求。 Z 规范语言规范语言 是一种在牛津大学编程研究组中发展起来的形式规范是一种在牛津大学编程研究组中发展起来的形式规范语言语言 基于谓词逻辑和集合论基于谓词逻辑和集合论 提供了丰富的语法元素提供了丰富的语法元素(construct), 比如比如, 基本类型基本类型(give

7、ntype), 公理公理(axiomatic)定义定义, 状态和操作模式状态和操作模式(schema)定义等等。定义等等。 Z 强调强调“描述性描述性”思维而非思维而非“过程性过程性”思维，其语义思维，其语义是数学的而非计算的，所以它不依赖于任何特定的规是数学的而非计算的，所以它不依赖于任何特定的规范开发方法，这一点使得范开发方法，这一点使得Z 成为了一种强有力的，灵成为了一种强有力的，灵活且扩展性良好的规范语言。自然，它也可以是一种活且扩展性良好的规范语言。自然，它也可以是一种用于规范安全系统的重要规范语言。用于规范安全系统的重要规范语言。 经过多年的发展，经过多年的发展，Z 规范语言的国际

8、标准已于规范语言的国际标准已于2002 年年正式通过实施。正式通过实施。 在一个规范中，首先出现的组件应该是给定的集合，这些集合常被用在一个规范中，首先出现的组件应该是给定的集合，这些集合常被用作类型和全局变量，此外还有一些有关它们语义的解释，确保它们的作类型和全局变量，此外还有一些有关它们语义的解释，确保它们的正确性是在适当抽象层次上进行建模的一个重要环节。正确性是在适当抽象层次上进行建模的一个重要环节。首先确定问题的重要部分，这些方面使用集合和约束来刻画。应该注首先确定问题的重要部分，这些方面使用集合和约束来刻画。应该注意到，有些集合之间是相互关联的，并且具有一定的结构，比如有序意到，有些

9、集合之间是相互关联的，并且具有一定的结构，比如有序列表等。列表等。定义系统基本数据的几种方法：定义系统基本数据的几种方法： 声明 最简单的定义方法是声明；例如，最简单的定义方法是声明；例如，Clark-wilson 模型中的模型中的DATA, OPERATION, USER, USERID, R_CDI，这里，这里DATA、OPERATION、USER、USERID、R_CDI 分别为系统数据、操作、用户、用户身份和受控数据之间分别为系统数据、操作、用户、用户身份和受控数据之间的约束关系。的约束关系。 x: A是一个声明，代表变量是一个声明，代表变量x从集合从集合A中取值。中取值。 x: t|

10、xs,对对x做了进一步限定做了进一步限定 简写 令定义的数据与现有的某一数据对象相等，例如，令定义的数据与现有的某一数据对象相等，例如，CDI = DATA;UDI = DATA，其中，其中CDI 和和UDI 分别为分别为DATA 类型的受控数据类型的受控数据项和非受控数据项。项和非受控数据项。 公理 定义时，要求不仅具有声明，还要列出其应满足的谓词，表明系统存定义时，要求不仅具有声明，还要列出其应满足的谓词，表明系统存在的约束关系在的约束关系 接下来，使用一个或者多个模式来描述抽象状态，状态模接下来，使用一个或者多个模式来描述抽象状态，状态模式应该保持简洁，并且仅只包括构造模型规范所必须的那

11、式应该保持简洁，并且仅只包括构造模型规范所必须的那些声明。些声明。 确定策略本质上就是对以状态机模型为计算模型的系统进行规范。确定策略本质上就是对以状态机模型为计算模型的系统进行规范。 用确定策略规范系统时，定义一个或者多个状态模式用确定策略规范系统时，定义一个或者多个状态模式(state schema)来描述系统状态，定义多个操作模式来描述系统状态，定义多个操作模式(operation schemas)来描述状态之间的转换。来描述状态之间的转换。 对于安全模型而言，只包括与安全有关的变量。对于安全模型而言，只包括与安全有关的变量。 Z语言中一个系统的规范主要由两部分构成：语言中一个系统的规范

12、主要由两部分构成： 状态描述部分：状态描述部分：Z 使用一个状态模式来描述状态，模式中所声使用一个状态模式来描述状态，模式中所声明的变量就是状态变量，每个状态变量都有一个类型和其相关明的变量就是状态变量，每个状态变量都有一个类型和其相关联，这个类型可以是一个诸如整型类型，或者更加复杂的诸如联，这个类型可以是一个诸如整型类型，或者更加复杂的诸如关系或者函数的类型。状态变量的值描述了系统在任意实例中关系或者函数的类型。状态变量的值描述了系统在任意实例中的状态。的状态。 在最初的层次上，钱包包括一个余额（在最初的层次上，钱包包括一个余额（balance）和一个损失）和一个损失（lost ）组件，代表

13、未成功支付时的损失总数，抽象状态空间含）组件，代表未成功支付时的损失总数，抽象状态空间含有一个从名字到钱包的映射，代表了已被认证的钱包。有一个从名字到钱包的映射，代表了已被认证的钱包。 商务系统状态由状态变量来构成，这些变量的值在安全操作的作用下可商务系统状态由状态变量来构成，这些变量的值在安全操作的作用下可以发生变化，而其它的虽然在策略模型中用到，但其值并不受安全操作以发生变化，而其它的虽然在策略模型中用到，但其值并不受安全操作的影响的变量，则被定义为安全策略模型的边界，对其值的约束也就是的影响的变量，则被定义为安全策略模型的边界，对其值的约束也就是安全边界条件。安全边界条件。 依据依据Si

14、moneSIMO01的看法，安全系统的安全特性根据安全特性的约的看法，安全系统的安全特性根据安全特性的约束对象，分为用于约束状态组件的安全不变量，以及用于约束状态迁移束对象，分为用于约束状态组件的安全不变量，以及用于约束状态迁移规则的安全约束，因此，系统状态和安全不变量相结合来确定安全状态。规则的安全约束，因此，系统状态和安全不变量相结合来确定安全状态。 安全不变量使用状态变量来定义，如果系统的每个状态都满足某一特定安全不变量使用状态变量来定义，如果系统的每个状态都满足某一特定状态不变量，也即构成状态的所有状态变量值都满足这个状态不变量的状态不变量，也即构成状态的所有状态变量值都满足这个状态不

15、变量的约束条件时，则称系统满足这个不变量。约束条件时，则称系统满足这个不变量。 Z 使用操作模式来描述操作。操作模式用于描述操作使用操作模式来描述操作。操作模式用于描述操作对系统状态变量的影响，以及该操作可以发生的条件对系统状态变量的影响，以及该操作可以发生的条件（也称作为前置条件）。（也称作为前置条件）。 操作模式具体由两部分构成：操作模式具体由两部分构成： (1)用于声明状态变量的声明部分。用于声明状态变量的声明部分。 (2)用于列举前置条件和操作影响的主体部分。用于列举前置条件和操作影响的主体部分。 在描述操作的模式中，约定带修饰符在描述操作的模式中，约定带修饰符“ ”的元素及其谓词的元

16、素及其谓词描述的是操作后系统该部分的状态，而不带该修饰符的元素描述的是操作后系统该部分的状态，而不带该修饰符的元素及其谓词描述的是操作前系统该部分的状态。因此，在模式及其谓词描述的是操作前系统该部分的状态。因此，在模式中不包括任何修饰符变量的条件就是前置条件，反之则为后中不包括任何修饰符变量的条件就是前置条件，反之则为后置条件。置条件。 在某些模型中的安全策略中，并不存在对操作应用序在某些模型中的安全策略中，并不存在对操作应用序列进行约束的条目。于是，在变换关系之上的约束可列进行约束的条目。于是，在变换关系之上的约束可以直接简化为作用在单个操作应用上的约束，也即形以直接简化为作用在单个操作应用

17、上的约束，也即形成各种安全操作。定义成各种安全操作。定义OPERATION 类型：类型： OPERATION 每一个操作执行都需要一些输入，同时也可能产生一每一个操作执行都需要一些输入，同时也可能产生一些输出些输出 例如，电子钱包系统的抽象操作规范如下：例如，电子钱包系统的抽象操作规范如下：其中，输出为其中，输出为 aNullOut 代表不关注输出。如果所有操作都代表不关注输出。如果所有操作都有输入输出，并且其类型相同，则容易完成，使用自由类型有输入输出，并且其类型相同，则容易完成，使用自由类型结构定义抽象安全操作的输入和输出，即结构定义抽象安全操作的输入和输出，即 AIN := aNullI

18、n| transferTransferDetails AOUT := aNullOut 定义系统定义系统 系统由一个可能的状态集、一个可能的初始化状态集、一个可能系统由一个可能的状态集、一个可能的初始化状态集、一个可能的操作集和一个可能的操作执行集合所组成：的操作集和一个可能的操作执行集合所组成： 这里应该注意的是在系统中这些操作都是真正可能的，不这里应该注意的是在系统中这些操作都是真正可能的，不允许系统包含从任何可达状态出发，决不会被执行的操作，允许系统包含从任何可达状态出发，决不会被执行的操作，虽然这是一个相当弱的活性条件，但是其对应于系统中必虽然这是一个相当弱的活性条件，但是其对应于系统

19、中必须有某些操作的要求。须有某些操作的要求。 所谓部分操作所谓部分操作(partial operation)是指该操作定义是指该操作定义仅仅只考虑一个成功执行情况的操作，并不进一仅仅只考虑一个成功执行情况的操作，并不进一步处理各种例外情况。步处理各种例外情况。 部分操作使用如下形式的模式来描述：部分操作使用如下形式的模式来描述： 这里通过谓词把输入和输出变量以及初始状态和这里通过谓词把输入和输出变量以及初始状态和终了状态关联起来。终了状态关联起来。 通常情况下我们希望建立一个完整的接口，目的是使系统通常情况下我们希望建立一个完整的接口，目的是使系统可以处理任何输入并且提供可见的结果。可以处理任

20、何输入并且提供可见的结果。 值得提及的是，应该和用户相互讨论以确保错误以适当的值得提及的是，应该和用户相互讨论以确保错误以适当的方式得到处理，使得对于错误情况的分析和处理必须和用方式得到处理，使得对于错误情况的分析和处理必须和用户的实际需求相适应。户的实际需求相适应。 例如，如果一个操作的前置条件是两个谓词的合取：例如，如果一个操作的前置条件是两个谓词的合取：pq，就有以下，就有以下3 种可能的错误条件：种可能的错误条件： p q p q p q 尽管尽管(pq)的情况是充分的，但是这或许并不足以保证的情况是充分的，但是这或许并不足以保证当系统出现错误情况时，可对系统行为进行有效描述，有当系统

21、出现错误情况时，可对系统行为进行有效描述，有时不可避免地出现未决情况时不可避免地出现未决情况(non-determinism)。 根据前置条件，给出完整的操作接口，使之能包含错误根据前置条件，给出完整的操作接口，使之能包含错误处理情况。处理情况。 全操作全操作(totaloperation) 它由描述操作成功情形的部分操作和各种错误组合而成，通常它由描述操作成功情形的部分操作和各种错误组合而成，通常使用模式析取方式来达到目的使用模式析取方式来达到目的 例如，安全支付（例如，安全支付（transfer）操作只更新源端）操作只更新源端from 和接收端和接收端to的状态，其他钱包状态保持不变。一个

22、转移只有在两个独立、的状态，其他钱包状态保持不变。一个转移只有在两个独立、已被认证并且支付端已被认证并且支付端from 具有足够额度时才能成功。具有足够额度时才能成功。AbTransfer安全在钱包之间进行支付或安全安全在钱包之间进行支付或安全“损失损失“某些余额。某些余额。 Z 语言中的计算模型是非确定性的，也即任何前置条件语言中的计算模型是非确定性的，也即任何前置条件满足的操作都可以被执行。这里应该注意的是，一个计满足的操作都可以被执行。这里应该注意的是，一个计算非确定模型并不意味着一个给定操作的影响是非确定算非确定模型并不意味着一个给定操作的影响是非确定的。的。系统的安全约束主要是用于约

23、束相邻两个安全状态对之间所必须满足系统的安全约束主要是用于约束相邻两个安全状态对之间所必须满足的关系，由于操作是引起安全状态发生迁移的唯一原因，所以可以把的关系，由于操作是引起安全状态发生迁移的唯一原因，所以可以把这种对于安全状态对之间的约束视作为对于操作的约束，也就通过使这种对于安全状态对之间的约束视作为对于操作的约束，也就通过使用安全约束来对操作进行约束，从而形成安全操作。用安全约束来对操作进行约束，从而形成安全操作。只有系统状态中的各个变量同时满足所有安全系统状态不变量的约束只有系统状态中的各个变量同时满足所有安全系统状态不变量的约束时，才可以成为安全系统状态。为了便于使用起见，可以把各

24、条安全时，才可以成为安全系统状态。为了便于使用起见，可以把各条安全约束组合在一起构成一个总的安全约束模式。约束组合在一起构成一个总的安全约束模式。 基本要求是要求状态和操作中的约束都是可以满足的。基本要求是要求状态和操作中的约束都是可以满足的。 对操作模式效果进行证明：对操作模式效果进行证明： 比如证明操作模式是否是安全状态保比如证明操作模式是否是安全状态保持的。持的。 由于每个安全操作对系统状态的作用都是通过系统中的操作函数由于每个安全操作对系统状态的作用都是通过系统中的操作函数来体现的，所以一个操作的安全定理应该包括系统前后状态、操来体现的，所以一个操作的安全定理应该包括系统前后状态、操作

25、和系统本身。作和系统本身。 具体内容包括语法、类型检查和域检查、前置条件计算和具体内容包括语法、类型检查和域检查、前置条件计算和通用定理证明等等通用定理证明等等 语法、类型和域检查 域检查分析用于确保在该规范中所包含的表达式和类型都是有意域检查分析用于确保在该规范中所包含的表达式和类型都是有意义的。如果无法从安全策略规范导出一个内在一致的、自容模型，义的。如果无法从安全策略规范导出一个内在一致的、自容模型，则其中就存在着非一致错误。则其中就存在着非一致错误。 从非一致错误机制来看可以分为两种类型从非一致错误机制来看可以分为两种类型全局非一致和局部全局非一致和局部非一致。当在一个规范中出现语义条

26、件过强的公理框、通用框或非一致。当在一个规范中出现语义条件过强的公理框、通用框或者谓词时，则整个规范将是不一致的，即全局不一致者谓词时，则整个规范将是不一致的，即全局不一致(global inconsistency)。全局非一致所造成的后果显然更严重些。全局非一致所造成的后果显然更严重些。 前置条件前置条件 如果操作的前置条件不能被满足，则该操作可能会彻如果操作的前置条件不能被满足，则该操作可能会彻底失败、或者不能终止、或者产生一些异常结果（例底失败、或者不能终止、或者产生一些异常结果（例如所产生的终了状态无法满足状态模式谓词部分的约如所产生的终了状态无法满足状态模式谓词部分的约束）。束）。

27、前置条件通常和错误情况以及部分操作一起来辅助理前置条件通常和错误情况以及部分操作一起来辅助理解规范。解规范。 在在Z 中，操作作为关系来看待，也即描述为初始状态中，操作作为关系来看待，也即描述为初始状态和终了状态之间的一个关系，这种对于操作的处理方和终了状态之间的一个关系，这种对于操作的处理方式具有很多优点，但是没有显式给出一个操作的前置式具有很多优点，但是没有显式给出一个操作的前置条件条件(precondition)则是这种方式的最大缺陷。则是这种方式的最大缺陷。前置条件的证明要求前置条件的证明要求 证明每个操作的前置状态不为空，即操作定义没有矛盾。证明每个操作的前置状态不为空，即操作定义没

28、有矛盾。 State; Input pre Op 实际上，对完全操作，它要求的条件要强的多：实际上，对完全操作，它要求的条件要强的多：State; Input pre Op在计算操作的前置条件时，通常是首先屏蔽所有输出和终了状态变量，在计算操作的前置条件时，通常是首先屏蔽所有输出和终了状态变量，然后使用存在量词对后状态和输出变量进行量化来生成前置条件。然后使用存在量词对后状态和输出变量进行量化来生成前置条件。应该仔细检查操作的描述，以确保它的前置条件在操作谓词中被显式应该仔细检查操作的描述，以确保它的前置条件在操作谓词中被显式的包括。的包括。由于安全约束只是作为一种安全特性而存在，本意是对由该

29、操作所引由于安全约束只是作为一种安全特性而存在，本意是对由该操作所引起的状态迁移动作的结果进行约束，并不影响该操作的执行以及执行起的状态迁移动作的结果进行约束，并不影响该操作的执行以及执行效果，所以在计算一个操作的前置条件时应该将其略去。效果，所以在计算一个操作的前置条件时应该将其略去。 一个操作的前置条件应该明确反映下列内容：一个操作的前置条件应该明确反映下列内容： 操作的有效输入。操作的有效输入。 操作模式中的谓词部分。操作模式中的谓词部分。 操作执行结果。操作执行结果。 在安全协议中在安全协议中 有效输入是消息本身有效输入是消息本身 操作模式的谓词部分是消息是否是合法有效的操作模式的谓词

30、部分是消息是否是合法有效的 操作执行结果是接受者所获得的知识增加了。操作执行结果是接受者所获得的知识增加了。 通用定理证明工具通用定理证明工具 在在Z/EVES 中，一个证明就是一个谓词演算序列，其中中，一个证明就是一个谓词演算序列，其中每一步都把当前目标谓词转变为一个逻辑上等价的谓每一步都把当前目标谓词转变为一个逻辑上等价的谓词，只有当能把目标谓词转化为谓词词，只有当能把目标谓词转化为谓词true 时，则意味时，则意味着完成了该证明过程。着完成了该证明过程。 简化公式简化公式 运用公理、引理以及函数定义简化公式运用公理、引理以及函数定义简化公式 重组公式重组公式 使用更加容易处理的等价项来替

31、换公式中的某些项，使用更加容易处理的等价项来替换公式中的某些项，例如，如果定理中例如，如果定理中x-1(x不等于不等于0），那么定理证明器将采用），那么定理证明器将采用y+1来代替来代替x. 等式替换等式替换 例如，如果公式中出现了例如，如果公式中出现了s=t，那么在公式的其他，那么在公式的其他地方将采用地方将采用s替代替代t，并消除该等式。，并消除该等式。 对于不再起作用的表达式，采用变量来替换，从而推广公式对于不再起作用的表达式，采用变量来替换，从而推广公式 消除公式中的不相关项消除公式中的不相关项 在需要的时候，归纳证明定理在需要的时候，归纳证明定理 为了完成证明过程，为了完成证明过程，

32、Z/EVES 提供了一系列的指令提供了一系列的指令 这些指令既包括对于公式的很小操作指令，也包括强有力的穷举证明这些指令既包括对于公式的很小操作指令，也包括强有力的穷举证明指令。指令。 在这些过程中，常常使用到各种类型的辅助定理在这些过程中，常常使用到各种类型的辅助定理 如用于重写的规则、用于前向证明链引用的前向规则及用于触发假设如用于重写的规则、用于前向证明链引用的前向规则及用于触发假设的假设规则等。的假设规则等。 同时，同时， Z/EVES支持数学工具包支持数学工具包(mathematical toolkit)，工具包中，工具包中包括了许多定理，它们具有在定理证明中可以为定理证明器自动引用

33、包括了许多定理，它们具有在定理证明中可以为定理证明器自动引用的形式。的形式。 用户控制推理过程用户控制推理过程 用户和证明系统之间的交互目的在于由用户来提供一个证明路线用户和证明系统之间的交互目的在于由用户来提供一个证明路线 使用把一个定理分割为一系列子定理，然后由证明系统来分别自动证使用把一个定理分割为一系列子定理，然后由证明系统来分别自动证明这些子定理。明这些子定理。 例如，可以对例如，可以对Clark-Wilson 模型的安全状态不变量证明目标进行分割证模型的安全状态不变量证明目标进行分割证明：每个状态不变量只是部分地约束了系统状态，如果在当前规则的作明：每个状态不变量只是部分地约束了系

34、统状态，如果在当前规则的作用下状态发生迁移后，为该不变量所约束的部分状态变量的值如果不发用下状态发生迁移后，为该不变量所约束的部分状态变量的值如果不发生变化，则意味着该不变量与引发此次状态迁移的规则无关，于是可以生变化，则意味着该不变量与引发此次状态迁移的规则无关，于是可以只针对集合的改变继续证明。只针对集合的改变继续证明。 尽量推迟归约证明尽量推迟归约证明(prove by reduce)等大运算量命令的执行；等大运算量命令的执行； 有针对性地运用实例化和等价替换命令有针对性地运用实例化和等价替换命令1将名字包括进来的一个目的是为了使该钱包自己可以验证它是否将名字包括进来的一个目的是为了使该

35、钱包自己可以验证它是否是这个交易所使用的钱包。是这个交易所使用的钱包。2 一个钱包具有状态（一个钱包具有状态（status），以记录交易进程：），以记录交易进程： 如果钱包在某一个可能造成价值（如果钱包在某一个可能造成价值（value） 损失的操作点取消了一个转损失的操作点取消了一个转帐操作，则钱包记录操作细节。帐操作，则钱包记录操作细节。 例如，当钱包处于例如，当钱包处于epv（已发送（已发送req消息）或消息）或epa（已发送（已发送val但未接收到但未接收到ack)状态时才需要更新日志。在其他情况下，由于支付尚未真正开始或状态时才需要更新日志。在其他情况下，由于支付尚未真正开始或已经成功

36、完成，无需进行记录。已经成功完成，无需进行记录。3例外日志例外日志 钱包保存支付信息，例外日志记录失败或有问题的交钱包保存支付信息，例外日志记录失败或有问题的交易以便重构所损失的价值，即进行冲正。易以便重构所损失的价值，即进行冲正。 CLEAR 是钱包例外日志的清除码集合，清除码由外部源确定用于清除是钱包例外日志的清除码集合，清除码由外部源确定用于清除钱包的例外日志。钱包的例外日志。 image 是用于计算一个非空例外记录集合清除码的函数。是用于计算一个非空例外记录集合清除码的函数。image 接收例接收例外日志的一个集合，计算一个用于认证日志清除命令合法性的一个数值。外日志的一个集合，计算一

37、个用于认证日志清除命令合法性的一个数值。 所包括的谓词反映论如下的约束：所包括的谓词反映论如下的约束： 1） pd : exLog name pd.from, pd.to 例外日志中的所有记录都与这个钱包有关，它可以作为发送方例外日志中的所有记录都与这个钱包有关，它可以作为发送方from 或者接收方或者接收方to 。 2）. status = epr = name = pdAuth.from pdAuth.value balance pdAuth.fromSeqNo pdAuth.toSeqNo nextSeqNo 如果钱包正在等待支付指令（如果钱包正在等待支付指令（payment value

38、），则其下一序列号大），则其下一序列号大于当前交易的系列号，这里钱包处于作为接收方的状态。于当前交易的系列号，这里钱包处于作为接收方的状态。 4）status = epa pdAuth.fromSeqNo nextSeqNo 如果钱包在等待支付确认，则其下一序列号大于当前交易的系列号。如果钱包在等待支付确认，则其下一序列号大于当前交易的系列号。在更加具体的层次上，一个完整的支付交易由在更加具体的层次上，一个完整的支付交易由startFrom, startTo, req,val, 和和 ack操作组成操作组成操作的输入就是协议中的消息。操作的输入就是协议中的消息。MESSAGE := start

39、FromCounterPartyDetails| startToCounterPartyDetails| readExceptionLog| reqPayDetails| valPayDetails| ackPayDetails| exceptionLogResultNAME PayDetails| exceptionLogClearNAME CLEAR| 第一组消息可能是不受保护的。通过将它们放入初始消息第一组消息可能是不受保护的。通过将它们放入初始消息ether 中，可中，可以对其可伪造这一性质进行描述。其中支付信息以对其可伪造这一性质进行描述。其中支付信息(counterparty )是

40、一个是一个短消息，指出对方身份、要支付的数目和对方的交易序列号。短消息，指出对方身份、要支付的数目和对方的交易序列号。第二组消息需要进行密码学保护，其不可伪造性要求第二组消息需要进行密码学保护，其不可伪造性要求: 只有使用特殊的只有使用特殊的操作才能将它们放入消息操作才能将它们放入消息ether 中。中。, 伪造消息伪造消息 是非认证过的钱包发送的，或是忽略（非相关）消息是非认证过的钱包发送的，或是忽略（非相关）消息的操作发送的，也可作为操作的操作发送的，也可作为操作Ignore, Increase 和和 Abort的输入。的输入。 实现为一个不受保护的状态消息、错误消息、实现为一个不受保护的

41、状态消息、错误消息、“伪造伪造”消息或消息或“沉沉默默”。支付日志记录支付日志记录Paydetails（支付信息），支付信息包括（支付信息），支付信息包括TransferDetails所具有的交易两方（所具有的交易两方（from,to） 的名字及资金转移的的名字及资金转移的数目信息，同时也记录序列号。钱包名字和交易序列号进行组合可以数目信息，同时也记录序列号。钱包名字和交易序列号进行组合可以唯一地标识一个交易。唯一地标识一个交易。协议可由协议可由StartFrom ； StartTo ；Req ； Val ； Ack操作序列组成操作序列组成。相应地，可定义钱包的操作状态：相应地，可定义钱包的操

42、作状态： STATUS := eaFrom | eaTo | epr | epv | epa无形操作无形操作 除了支付操作，在抽象模型中，还存在忽略操作除了支付操作，在抽象模型中，还存在忽略操作AbIgnore，在具体模型，在具体模型中，它被具体化为以下的无形操作：中，它被具体化为以下的无形操作：IncreasePurse、 AbortPurse这些操作对可见组件状态没有任何影响，只是增加序列号。例如，这些操作对可见组件状态没有任何影响，只是增加序列号。例如，AbortPurseOkay 操作只是中止（操作只是中止（ abort）和记录（）和记录（log）不完全的交易，）不完全的交易，只有钱包

43、的序列号、例外日志只有钱包的序列号、例外日志pdAuth 和状态和状态status 会发生改变。会发生改变。例外日志操作例外日志操作 ReadExceptionLogPurse 钱包必须接收到钱包必须接收到readExceptionLog消息。消息。 首先要记录所有未完成的支付，并转移到首先要记录所有未完成的支付，并转移到eaFrom状态，然后再执行操作状态，然后再执行操作。 操作回送一个未受保护的状态消息（如无此记录）或返回一个受保护的操作回送一个未受保护的状态消息（如无此记录）或返回一个受保护的exceptionLogResult 消息，含有一条例外记录。消息，含有一条例外记录。 Clea

44、rExceptionLogPurse 在清除日志交易时，在清除日志交易时， 钱包必须接收到非空的例外日志和一个合法的钱包必须接收到非空的例外日志和一个合法的exceptionLogClear 消息。消息。 只改变钱包日志，其他组件不变，如果当前交易和例外日志不存在，则忽略只改变钱包日志，其他组件不变，如果当前交易和例外日志不存在，则忽略这个消息。这个消息。 钱包空间代表了系统的体系结构，其组织形式是全局化（钱包空间代表了系统的体系结构，其组织形式是全局化（promoted）的状）的状态态-操作模型。操作模型。该空间包括钱包集合、公共空间该空间包括钱包集合、公共空间ether 用于存储所有以前发

45、送的消息只改变钱包日用于存储所有以前发送的消息只改变钱包日志，其他组件不变，和一个私有志，其他组件不变，和一个私有archive用于安全存储例外日志，每条记录都标有用于安全存储例外日志，每条记录都标有保存这一记录的钱包名字。保存这一记录的钱包名字。在在ether 中，有些类型的消息是可以伪造的。中，有些类型的消息是可以伪造的。在具体层次，对钱包行为的描述必须能真实反映实际设计的内容。这样就可在具体层次，对钱包行为的描述必须能真实反映实际设计的内容。这样就可以首先建立单独的钱包的模型，然后将它阶跃（以首先建立单独的钱包的模型，然后将它阶跃（promoting ）为具有多个钱）为具有多个钱包的空间模型。包的空间模型。阶跃技术阶跃技术 如果局部类型被一个全局类型完全封装，则称阶跃是自由的，否则，称如果局部类型被一个全局类型完全封装，则称阶跃是自由的，否则，称为受限的阶跃，这里我们主要使用自由阶跃。为受限的阶跃，这里我们主要使用自由阶跃。 为反映不能对钱包和通信介质进行全局控制这一事实，需要证明一些谓为反映不能对钱包和通信介质进行全局控制这一事实，需要证明一些谓词成立，消除关于传送不确定性的约束词成立，消除关于传送不确定性的约束 ，然后才可使用自由阶跃。，然后才可使用自由