223理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html17页一种基于Maude模型的迪利亚E. Rodr'ıguez1，2空军研究实验室信息处美国纽约州罗马市，邮编：13441-4505摘要元对象用于将第一个异步、主动、秘密共享协议的规范分解为秘密共享、复制和加密层。描述了一种搜索策略，该策略利用规范的结构来减少搜索空间。关键词：协议规范，元对象1介绍对软件系统的要求越来越高。它们应该是分布式的、可靠的、适应性强的、安全的等等。设计和推理这样的系统是非常困难的，而且可能会有很多风险。为了帮助管理这种复杂性，Maude [1]将面向对象、继承性、丰富的参数化模块和用户可定义的语法引入了形式化领域为了提供进一步的模块化、适应和重用形式规范的方法，元对象被赋予了重写语义[2]。个案研究可有助于在明智地结合这些手段方面取得经验这里所描述的工作是朝着这个方向的一种尝试COCA [7]是一个容错和安全的在线认证机构，具有非常弱的假设，从而降低了其脆弱性。为了维护用于签名证书和响应的私钥，开发了第一个异步主动秘密共享协议（APSS），这就是这里描述在[6]中，它被描述为一系列假设越来越弱的版本规范和本演示文稿的开发遵循这些步骤。第2节介绍秘密共享。Maude中的对象和元对象的概念第4节介绍了协议的第一版，介绍了规范的基本结构。第5及61由空军科学研究办公室支持2电子邮件：Dilia. rl.af.mil2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。罗德里格斯224n描述获得协议下一版本的修改方案的正确性标准定义见第7节。第8节描述了一种利用规范分层结构的搜索策略。下面是一个简短的结论2秘密共享秘密共享解决了秘密的可用性和秘密性之间的紧张关系，通过将秘密分发给多个服务器，只有当其中一些服务器受到损害时才公开秘密。 一个特殊的方案是（n，t + 1）秘密共享，由分裂和重建操作定义。Split从一个秘密中生成一个随机的n个共享的集合，称为共享，而reconstruct从具有超过阈值t个共享的共享的任何子集中获得秘密。如果秘密共享是单个值，则称为标准秘密共享。在[6]中，Zhou描述了一个（n，t+1）余项的构造. 秘密分享从（l，l）标准秘密共享，其中l=t。集P1，…，Pl的t服务器代表最坏情况的故障场景。给定共享s1，...，s1，每个份额s1与失败场景P1相关联。服务器p的（n，t+1）个秘密共享的相同秘密的份额，称为fp的份额集，记为Sp，定义为dysi∈Sp惠p∈/Pi。更抽象地说，对于每一个服务器p，对应于一个索引集合Ip，使得i∈Ip惠p∈/Pi。[6]中提出的秘密共享协议采用组合（n，t+1）秘密共享来维护秘密。下一节将非常简要地介绍Maude中对象和元对象的概念，它们将用于表示服务器和分离协议的不同方面3对象和元对象一个分布式的面向对象系统在Maude [4]中被表示为一个排序的术语Configuration，它有子排序Object和Msg。配置是由一个多集联合算子建立的，分布式系统的状态由一个术语描述：M1... M m< O1：C1|attts1>.
.M是消息，其他项给出名为Oi的对象的状态类C i的，其属性值在atts i中给出，i = 1，.，n.罗德里格斯225--系统的动态由重写规则指定，其最常见的形式是r：M1. M m< O1：C1|attts1>. . . 。 < Q1：D1|attsJ1J>. M1J. MQJ如果条件。这个规则，用r表示，表示如果条件Cond成立，消息M被消耗;一些原始对象O以新的状态和可能的新类CJ保持，并且出现新的对象Q和消息MJMaude支持这样一种约定，即规则不需要提及与该规则无关的对象属性为了表示更复杂的实体，有元对象的概念，在[2]中给出了重写语义。不同的通信服务可以由不同的元对象表示，并且可以通过堆叠相应的元对象来组合，可能会受到一些接口约束。这些可堆叠的对象必须在MetaObject的子类中定义，MetaObject是一个允许消息向下移动和配置请求向上移动的类，配置请求是消息传输或对象创建的多组请求元对象有五个属性：base，标识堆栈底部的元对象;和四个数据列表，允许与相邻元对象和环境通信 来自上层或外部的消息被导入到in中; down保存要导出的消息; up保存从下层导入的配置请求; out保存要导出的配置请求。在这里介绍的规范中，MetaObject与上面的描述不同，导入列表被multisets取代。一个元堆栈是一个元对象的列表，所有这些元对象都有相同的基，并且其最后一个元对象是被标识为基的元对象。MetaTower的一个术语是MS ， 其 中 MS 是 一 个 元 堆 栈 。 MetaStack 和 MetaTower 是Configuration的子类。下一节介绍了APSS的第一个模型。元塔、对象和消息的配置描述了系统的状态。。4APSS与单一协调员这第一个协议假设一个良性的环境。它是一种异步协议，对服务器速度、消息延迟或本地时钟漂移没有限制它的目标是主动地用相同秘密的另一个共享替换由n个服务器集体持有的秘密的一个共享在协议的一次运行或实例期间产生，并在下一次运行期间销毁为了知道秘密，对手必须获得足够的共享份额来重建它。因此，脆弱性窗口期是罗德里格斯226≥n✛构建体sJls1l...。。sJjs1j...的伊尔。西伊季。......sll。slj。s11sl✻分裂。。SJ1S11S1............Fig. 1. 共享刷新连续两次跑步。该协议假设在此期间不超过t台服务器受到危害。它还需要n3t + 1。第一个版本假设对手是被动的。一个被入侵的服务器可能只会遇到崩溃故障，将本地存储的信息泄露给对手。链路被假定为是可靠的，将每一条消息传递给其预期的接收者;对手只能窃听链路。4.1共享刷新一个（n，t +1）组合算子. l s加密共享建立在（l，l）标准之上秘密共享，其中l=t。 每台服务器都为每个索引在其索引集中。若要替换共享s1，...，s 1，分割每个份额，并且如图1所示重构所得到的子份额，以获得nsJ1， . . . ，SJL.协议要求每台未被入侵的服务器都要分配份额。由于每个标准共享由多个服务器持有，并且拆分操作是不确定的，因此需要协调器为下一次共享选择子共享。此版本假定协调器对攻击免疫。基本秘密共享操作的语法如下所示：op split：MachineInt Label SplitId Secret ->NeSetOfShares。操作构造：MachineInt LabelNeListOfShares -> Share？ 。两者都需要共享的长度，并且都标记了它们的结果。由于split是不确定的，所以split id可以区分不同的应用。 该协议永远不会重建所维护的秘密。构造从必须具有共享长度的共享列表中获得一个共享，这是一个Secret;否则，它返回errorShare。罗德里格斯227◦ ◦索引的共享集表示服务器的共享集以及它们获得的子共享的集合基本操作被重载以对其进行操作opsplit： MachineInt Label MachineInt Oid NeISetOfShares->SubsharesLabels.索引集合中具有给定标签L的每个份额si被分割成长度由第一个参数给定并由L i O标记的（子）份额，其中O是第四个参数，执行分割的服务器的名称每个共享结果都由一个由服务器名称和拆分计数组成的拆分ID进一步标识，拆分计数从第三个参数开始op构造：MachineInt Label NeListOfLabels NeISetOfShares->NeISetOfShares。一个新的共享集由构造产生，其前提条件要求，对于给定索引集中的每个索引，与列表中的每个标签共享，其长度必须在第一个参数中给定所得到的份额被标记有给定的标签。介绍了收集共享和删除所有共享或除具有某个给定标签的共享之外的所有共享的操作op _+>_：NeISetOfShares NeISetOfShares ->NeISetOfShares。op_>-： NeISetOfShares ->NeISetOfShares。op_>- ' [ _ ' ] ： N e I S e t O f S h a r e s 标 签 - > N e I S e t O f S h a r e s 。4.2APSS和MetaObjects异步、主动的秘密共享协议主要是分割和构建共享，但需要复制和加密，这使得协议复杂这种指定将这些方面分解为不同的元对象。4.2.1秘密共享层基础层捕获协议的正确秘密共享部分服务器是秘密共享的持有者，协调器在它们替换秘密时指导它们。消息被保持在最小和简单的范围内。本节描述异步对象重写理论，其规则在左侧有一个对象和最多一个消息，然后可以转换为[2]中描述的元对象理论。运行的每个参与者或主体都知道共享的长度它的状态可能是向上或向下。主类|共享长度：MachineInt，status：状态，当前版本号：MachineInt。级服务器|split-count： MachineInt，runs： SetOfTime，共享：ISetOfShares，子共享：ISetOfShares。子类服务器<主体。罗德里格斯228班级协调员|正在运行：Bool，chose：Bool，propagated-subsharings：propagatedSubsharings. Subclass Coordinator Conf]=>[短信。操作_<|_：Id消息->消息包op ：ConfReq ConfReq->ConfReq[配置文件id：none]。为了从协议的秘密共享部分抽象出复制，AId排序项被用来表示一个或多个具体对象，这些对象由Oid排序项标识。在上面，all用于表示所有服务器。抽象消息将通过复制元对象转换为发送给具体对象的当每个服务器从协调器接收到指令时，它将其份额与指定的标签分开，并将子份额发送给应该拥有它们的持有者（参见图1），并将产生的共享的标签发送给协调器。crl [contribute]：[<服务器：ActiveServer|状态：up，运行：Rs，当前版本号：V，拆分计数：Cnt，共享长度：Len，份额：Ss>（Srv<|C|< init（L））Conf]=>[<服务器：ActiveServer|运行：Rs U（L，仅旧），拆分计数：Cnt+size（labels（split（Len，L，Cnt，Srv，Ss）>{#（持有人<|SRV| ConfReq用于将必须作为一个单元转换的消息括起来一系列的复制、简化和联合将发给持有者的一条消息转换为发给持有者的一条消息-（I），其中I = 1，...， Len，其中只有索引集中包含I的服务器应该拥有的子共享。（一）有“德”者，必有“德”者。当协调器收到足够的标签时，每个索引至少有一个标签，它选择其中的l（指定的共享长度Len）来指定用于构建新共享的子共享，并将它们发送到所有服务器。当一个服务器拥有了它所需要的所有子共享时，它构造它的新共享集，并向协调器发送一个计算（L）消息，其中L是带有新版本号的标签。协调器必须等待来自不同服务器的2t+1个计算消息的法定数量，然后才能得出新共享已安装的结论。协调器的复制元对象收集这些消息，当达到仲裁时，向下发送（对应于的消息C <|comp-quorum|<计算 （L），其中comp-quorum的排序为AId。 在更新当前版本号并重置其他属性之后，协调器发送所有<|C|<完成（L），其指示服务器更新当前版本号并删除旧共享和所有子共享。4.2.2复制层如上所述，某些消息具有抽象的接收者或发送者，表示一组实际的主体。复制元对象的任务是在抽象和具体消息之间进行转换。受此示例的启发，可以定义一个有点通用的参数化复制元对象当配置请求向上移动时，它们可能会被复制，而当消息向下移动时，如果被识别为对仲裁有贡献，则它们可能会被过滤（其他REPL包括META-STACK。排序ReplicatorMap QuorumMap Filter。类Replicator |replicator-map：ReplicatorMap，filter：Filter，quorum-map：QuorumMap。子类Replicator=>如果不是（待U-过滤（F，CR））。crl [多对一自上而下]：<复制者R|过滤器：F，在：M MConf， 向下：Ml，法定人数映射：QM>=>< RO：Replicator.R|过滤器：d过滤器（F，M）in：MConf，down：Ml.*.d-filtered（QM，F，M）>if to-be-d-filtered（F，M）.* morerulesendom）当消息通过复制层向下移动时，过滤器F识别任何作为要计入法定数量的响应的消息只有当达到法定人数时，才传递消息以报告该事实。要定义要堆叠在服务器和协调器元对象上的复制元对象，对象模块(omod请求-N-响应是* 模块导入类|a2c-map：A2C-Map， responses-quorums：QuorumMap，response-recognizer：RespRecognizer。子类（C<|C|<完成（L））]=>[会议]-[L]，subshares：SSs >->]。6防御活动链接攻击该协议的下一个版本将防御主动链路攻击者。它们可以插入、修改、删除、重新排序或重放消息。最难防御的是删除消息。本节非常简要地概述了该版本规格的要素这个版本假设公平的链接。不一定所有的信息都能被传递，但如果有无限多的信息被传递，那么就有无限多的信息被正确地传递。为了近似多播的可靠链路[6]，引入了group-send原语。由p进行的群发送（p，m，ack，d）定义如下。对于任何服务器q，p为q构造一个消息m，并重复发送给q。当q接收到消息时，它将ack（m）发送回p。当p接收到数据，或者当它从另一个运行中接收到一个完成的消息时，这个组发送终止例如，协调器发送给所有服务器的init消息（参见第6页）由contribute消息确认。在这里，相同的消息被发送到所有服务器。当为每个接收者定制相同类型的消息时，也会使用此原语，因为发送到所有服务器的建立消息需要t+1个分段（参见第6页）此协议的规范要求对上一版本的基础层和复制层进行新的协议消息被引入以充当副本，并且复制层必须允许消息的重新发送。复制层中的过滤器不仅必须识别数据包，而且每个消息组都有一个计时器，并存储消息，以便在必要时重新发送可以使用[5]中面向对象系统的时间处理思想和[3]中计时器的使用7正确性准则异步主动秘密共享协议具有三个正确性要求：保密性，秘密对对手保持未知;可用性，正确的服务器共同具有足够的份额来重建秘密;以及进展，每次运行最终终止，这意味着正确的服务器最终删除前一次运行的份额可用性和保密性的谓词定义如下：秘密：秘密。ops is-available is-secret：Configuration -> Bool。罗德里格斯233opall-secrets：SetOfShares->SetOfSecrets。eq可用（Conf）=所有秘密中的秘密（服务器共享（Conf））。eq is-secret（Conf）=not（the-secret in all-secrets（adversaries-shares（Conf）.servers-shares （Conf ）是活动服务器拥有的所有共享和子共享的集合;adversaries-shares是对手的类似集合共享有三种表示形式，具体取决于共享是从拆分中获得的、从刷新过程中获得的，还是在运行结束时安装的。所有秘密通过从共享递归地恢复秘密来变换一组秘密。8分层规格说明的搜索策略如果存在协议的某些运行，其中在某些点服务器不能恢复秘密或对手可以恢复秘密，则违反了APSS协议的可用性和保密正确性标准。Maude是一种响应式语言，支持任意数量的元层。任何规范都可以在下一个元级别上进行元表示，从而从中进行操纵。特别是，Maude可以用来指定策略，规范来控制重写过程。本节考虑APSS协议规范的一些属性。它激发并描述了一种策略，该策略穷尽地生成具有此类属性的规范的所有计算这些计算可用于通过搜索违反可用性或保密性的运行来正式分析协议8.1穷举搜索协议的完整规范包括协议本身的规范、预期参与者的动作和消息，以及它必须运行的环境的规范和它保证的属性。所有这三个组成部分都可以通过重写理论来具体化，其中一个属性通过检测并以某种方式捕获违反它的状态的规则来负具体化。然后，可以通过从给定的初始状态生成所有计算，并搜索以应用指定违反保证属性的某些规则结束的那些计算来形式化地分析协议8.2简化工作，创造良好环境APSS由服务器数量n和妥协阈值t一个特定的（n，t）实例化的APSS正式分析的计算树的穷举搜索植根于初始状态的实例化。在这种状态下，每个服务器都拥有一个标准共享si，罗德里格斯234→对于其索引集中的每个i，所维护的秘密的一些初始共享。对于协议的第一个版本，有n个服务器和一个协调器。对于第二种情况，有n个主体，其中至少t+ 1个是充当协调器的服务器。初始状态既没有对手，也没有消息。因此，对于这两个版本，初始状态都是三个元对象塔的配置这两个协议都假设一个良性的环境，在这个环境中，对手只能从崩溃的服务器访问本地信息。在这种假设下，加密是不必要的。因此，搜索空间可以通过使初始状态具有两个元对象塔而没有加密元对象来稍微减小8.3计算的标准形式计算是一系列转换，对于Maude中指定的系统来说，这些转换是重写规则应用程序。在并发系统中，一些转换是不可比较的，导致一些虚假的区别计算。穷举搜索的问题是组合爆炸的问题。因此，尽量减少这些人为的区别是很重要的。如果当s→τ时，t和s→τJ存在一个状态sJ使得tτJSsJ和tJ→τsJ。τ/ τJt//❅τJ❅❅❘❅❅❘tJ//τSJ因此，改变不相交子状态的跃迁是不可比较的。一个元对象有四个通信属性in、out、up和down，可能还有其他属性。元对象的内部转换只改变该元对象的状态对于秘密共享和复制元对象，内部转换要么消耗一个导入属性的单个元素（in、up），要么产生其导出属性的新元素（down、out）。通信转换是规则in、out、up和down的应用（参见[2]），在通信属性方面与内部Meta对象转换是互补的：一个在另一个消费的地方产生，反之亦然。规则向上和向下的应用程序在元堆栈中的相邻元对象之间传输数据;向上，从属性输出到属性向上;向下，从属性向下到属性输入。规则in和out的应用程序依次在元对象塔的顶部元对象和周围的配置之间传输数据;in，从配置到in属性;out，从out属性到配置。命题1设i，i o，i oJ是秘密共享或复制元对象的内部转移，其中下标标识元对象并且oJ/= o。罗德里格斯235τk→ ···→设c、cJ为通信转换。然后i/cc/伊欧联系我们/联系我们联合国J/联系我们/c/c//cioJ//io为了减少搜索空间，对一些不可比的转换施加规范顺序。让ss和r表示内部秘密共享和复制转换，并且in、out、up和down表示规则in、out、up和down的应用。然后内、外、上、下初始状态被假定为所有Meta对象的所有通信属性都为空.因此，这份订单相当于立即交货的政策。8.4APSS复制层是Church-Rosser复制层的行为由四个条件规则描述。两个消费向上移动的消息;两个，向下移动的消息;在每一对中，一个规则的条件是另一个规则的条件的否定因此，由复制元对象消耗的任何消息确定唯一的转换。复制规则的应用可以产生零个或多个要向上、向下或在两个方向上导出的消息，从而实现输出和向下转换，其中输出转换实现由其他复制元对象进行的输入转换在参数化复制层的APSS实例化中，只有Filter属性的值可以更改。它被实现为一组元组。向上移动的消息可以向过滤器添加新的向下移动的消息可以替换元组，只是为了改变作为向下移动的消息的计数的组件由于导入属性（in和up）是多重集，并且向下移动的消息可能只会更改计数值，因此元对象的内部转换是不可比较的。Proposition2LetroandroJ元对象然后是APSS复制的内部转换ro/JR/联系我们❅鲁杰罗阿托洛❅❘//ro联系我们从命题1和命题2，通过归纳得出APSS复制层是Church-Rosser。τJτJProposition3Lets→τ1·· ·→tands1l tJbes equen cesoftransitions更改APSS复制元对象的状态存在状态sJ和sequencestτk+1τnsJ和tJτlJ+1τmJsJ。→···→ → ···→罗德里格斯2368.5隐藏图层可用性和保密性属性取决于秘密共享层的状态因此，需要探索的计算树是其节点是秘密共享层的状态的计算树复制层的转换应隐藏。给定秘密共享层的状态，计算树中的子节点通过应用内部秘密共享规则或立即递送所发送的消息来获得，这隐藏了复制转换。由于复制层是Church-Rosser，因此可以方便地使用预定义模块META-LEVEL的函数元重写。这个函数接受一个模M，一个项T和一个整数n，并使用一个默认的公平策略来求出一个TJ项。对于n= 0，所得到的TJ不能被进一步重写。在为了向元重写提供用于此目的的适当模块该规范修改如下。8.6配置层如所指定的，APSS实例化的状态是具有两个元对象塔的配置由于在穷举搜索过程中，将消息上下移动以及进出配置的转换应该被隐藏，因此元对象塔被分解。 对于搜索，状态由复制配置和秘密共享配置表示。复制配置具有复制元对象。秘密共享配置具有敌手对象和用于服务器和协调器的秘密共享元对象计算树中的节点是TssTr形式的项，其中Tss和Tr是秘密共享和复制配置的元表示。TR通过内部秘密共享转换保持不变隐藏的转换在发送消息时触发 规则up被一对规则up>取代，它通过将配置请求从元对象导出到配置中来启动来自秘密共享配置的配置请求的传输。复制配置的对应规则<将其从配置导入元对象。为配置间传输引入了新的语法，它将配置请求与对象ID配对，以识别两种配置中匹配的元对象。这些匹配规则的应用由元级操作介导，该元级操作从秘密共享配置中提取该消息并将其插入复制配置中。类似地，rule down被复制层rule 所取代，它们通过元级操作来传递从复制配置发送到secret-sharing配置的任何消息。匹配应用out和in被替换为应用新的rule，下>），Mr=Mr+（<上，<下，<出）-（<上，<下，<进，<出）。有关详情载于附录。9结论已经描述了异步主动秘密共享协议的一些版本。该规范被分为三层：秘密共享、复制和加密。针对APSS协议的（n，t）实例化，实例化了用于消息复制和应答定额收集开发了一种利用规范的结构来减少搜索空间的策略发现了数千个长度为40的完整序列，没有一个更短。由于脆弱性周期是两次连续运行的持续时间，因此搜索树的深度至少应为80。因此，将寻求减少空间搜索的进一步方法这个工作是使用Maude 1.0.5完成的。继续的工作将利用更强大的功能，新版本的Maude在更好的分析技术和更完整的规范的协议。A附录用于互配置消息的op up'（_'）>_：ConfReq Oid -> ConfReq. opdown '（_'）>_：Msg Oid -> Msg.秘密共享配置的通信规则：rl[up>]：[配置]=>[Conf（上（CR）> B）]。rl[down>]：[配置（down（M）> B）]=>[Conf]中。复制配置的通信规则：rl[down]：[配置]=>[Conf（向下（M）>B）]。rl[up]：[配置（上（CR）>B）]=>[Conf].rl[out in]：[配置罗德里格斯238< O'：元对象|输出：（B <|M）。CRl >]=>[Conf< O'：元对象t|输出：CR1>]。把状态的元表示作为一对配置。保护TUPLE（2）[Term，Term]* （sortTuple[Term，Term]to Layered-Term，opop p1_toss._ ，opp2_to r._）的。subsort分层<术语。给定一个状态T，该状态由应用内部秘密共享转换产生，该转换由标记为L的规则指定：extTerm（meta-apply（Mss，ss. T，L，none，0））#r. T .从配置中提取对象、向上和向下消息的操作操作o^_u^_d^_：期限->期限。用于组合配置的操作：op^：-> Term.op_&_：Term Term-> Term [ascurrentid：^].立即交付的实施：等式deliver（Mss，Mr，T）= r>ss（Mss，r（Mr，ss>r（Mss，Mr，T）。等式ss>r（Mss，Mr，T）= 0 ^（extTerm（meta_apply（Mss，ss. T，'up>，none，0）#（r.不&u ^（extTerm（meta_apply（Mss，ss. T，'up>，无，0）。等式r（Mr，T）= ss。 T #元重写（Mr.T，0）。等式r>ss（Mss，T） =d>>（Mss，（ss. T）&（d^r. T））#o^r. T.等式d>>（Mss，T）=if extTerm（meta-apply（Mss，T，else d>>（Mss，extTerm（meta-apply（Mss，T，菲引用[1] M. Cl avel，F. 你好，S。 E ker，P. Lincoln，N. Mart'oliet，J. 梅塞格尔，以及J. Quesada. Maude：Specification and Programming in Rewriting Logic. ，SRIInternational，1999.可在www.example.com上获得http://maude.csl.sri.com/。[2] G. Denker，J. Meseguer和C. 塔尔科特 重写元对象和可组合分布式服务罗德里格斯239的 语 义 ， 理 论 计 算 机 科 学 电 子 笔 记 ， 36 （ 2000 ） 。 可 查 阅http://www.elsevier.nl/locate/entcs/volume36.html。罗德里格斯240[3] I. Mason和C. 塔尔科特Maude中的简单网络协议模拟，理论计算机科学电子笔记，36（2000）。可在http://www.elsevier.nl/locate/entcs/volume36.html上获得。[4] J. Meseguer。“并发对象的逻辑理论及其在Maude中的实现。”In G.Agha，P.Wegner和A.Yonezawa，编辑，MIT Press，1993.[5] P. Oülveczky和J. 梅瑟格尔 Real-TimeMaude：一种用于模拟的工具和分析实时和混合系统，电子笔记理论计算机科学，36（2000）。见http://www.elsevier.nl/locate/entcs/volume36.html。[6] L. 舟“走向容错和安全的在线服务”，博士。论文，康奈尔大学，2001年。见http://www.cs.cornell.edu/Info/People/ldzhou/coca.htm。[7] L. Zhou，F.B. Schneider和R.范·雷内斯。COCA：一个安全的分布式在线 认 证 机 构 ， ACM 计 算 机 系 统 交 易 。 出 现 。 可 查 阅http://www.cs.cornell.edu/Info/People/ldzhou/coca.htm。
