模型检验俄罗斯卡"：密码协议无条件安全模型检验及认知逻辑分析

理论计算机科学电子笔记149（2006）105-123www.elsevier.com/locate/entcs模型检查俄罗斯卡H.P. van Ditmarsch1，2新西兰达尼丁奥塔哥大学计算机科学W. van der Hoek3联合王国利物浦大学计算机科学R. van der Meyden4澳大利亚悉尼新南威尔士大学计算机科学与工程学院J. 阮5新西兰达尼丁奥塔哥大学计算机科学摘要我们在三个不同的最先进的认知模型检查器中实现了一个特定的纸牌代理之间的比特交换协议，并比较了结果。关键词：密码学，无条件安全，模型检验，基于信息的协议，认知逻辑。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.07.029106惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）1051介绍密码协议的安全性通常取决于几个假设的真实性：代理是计算有限的，并且某些计算问题在给定这些计算限制的情况下是棘手的例如，在基于公钥加密方案（如RSA）的协议中，消息的解密对于预期的接收者来说是易处理的，但对于窃听者来说是不可能的，因为它需要分解一个大的素数乘积，这是一个被认为是棘手的问题然而，确实存在无条件安全的协议，其安全性不依赖于这样的假设。这些协议可以被证明是安全的，即使对对手具有无限的计算能力，因为他们确保对手不能学习秘密的信息理论，而不是计算的原因。验证密码协议的一种流行方法是根据使用知识和信念逻辑表示的信息流来分析它们[3，12]。一般来说，这些逻辑的语义并没有捕捉到协议的安全性所依赖的计算复杂性的维度：相反，它们将代理视为纯粹的信息理论推理机，其计算能力甚至超出了递归可验证性。然而，这个特性使得这些逻辑成为分析无条件安全协议的非常合适的工具。在本文中，我们考虑的应用程序的知识逻辑无条件安全协议的基础上的信息交换接地的相关性所产生的一副牌已被处理的代理。一个玩家可以将诸如卡片所有权之类的秘密比特传达给另一个玩家1本研究是在AOARD（亚洲空军研究与发展组织）研究基金AOARD-05-4017的支持下进行的澳大利亚国家信息和通信技术项目由澳大利亚政府的“支持澳大利亚能力”倡议资助汉斯·范·迪特马施和冀鲁安密切合作，而冀鲁安在奥塔哥拜访汉斯Hans感谢Jan van Eijck在DEMO开发过程中提供的令人兴奋的互动Wiebe van der Hoek自2002年作为WilliamEvans Fellow访问奥塔哥以来，一直参与Ron van der Meyden在2003年Hans访问悉尼期间编写了最终成为MCK计划的第一个版本，以及第一次尝试MCK计划的基础，用于任意初始状态的汉斯和纪后来完成了这些。罗恩后来开发了两个MCK程序的更快版本。我们衷心感谢Franco Raimondi在完成MCMAS计划时提供的非常有用的帮助。我们也感谢MoChArt 05组织提供的匿名推荐人的评论。2电子邮件地址：hans@cs.otago.ac.nz3电子邮件地址：wiebe@csc.liv.ac.uk4电子邮件地址：meyden@cse.unsw.edu.au5电子邮件地址：jruan@cs.otago.ac.nz惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105107而不向第三玩家（窃听者）泄露这些秘密。这已经在[6，16，10，1，17]中进行了研究。一个典型的例子是“问题”在于找到一种协议，允许发送者和接收者了解对方的牌，而在[16]中，给出了长度为2的原型，解决了这个问题.长度大于2的协议在[17]中进行了研究在这样的卡协议，所需的后置条件并不总是明确或不容易验证，公开已知的协议功能可能涉及相当复杂的嵌套动态认知公式，枚举所有可能的协议是一个问题。模型检查器是解决这些复杂性的有前途的工具在[20]中，对俄罗斯纸牌问题进行了部分模型检查分析：将场景的认知属性转换为（线性时间）LTL，然后使用模型检查器SPIN进行验证一张牌加上一些公告对应于一个时间线。代理人的不确定性通过利用[4]中提出的局部命题来表示，也参见[13]。这种模型检查认知逻辑的方法有一些缺点：需要翻译意味着认知方面只是隐含在分析中，它需要用户明确提供适当的局部命题-可能很难识别-并且在知识运算符出现否定的情况下，需要多次运行模型检查器来进行验证在这方面的贡献，我们采取了一种更直接的方法，验证协议属性的模型检查器的工作与认知逻辑明确。我们对一些系统进行了比较研究，基于各种方法来表示知识的进化：知识逻辑与线性和/或分支时间的组合[5，9，14]，以及动态认知逻辑[8，2，15]。具体来说，我们考虑模型检查器MCK[7]使用基于BDD的算法处理知识逻辑以及线性和分支时间，MCMAS [11]使用基于BDD的算法处理知识和分支时间，DEMO [18]是基于动态认知逻辑的显式状态模型检查器。我们选择了一个特定的俄罗斯纸牌协议，即“五手协议”，在这些非常不同的这涉及到用时间认知术语重新解释动态认知概念;这一理论练习成功地进行了，并增加了我们对动态认知特征的理解所有三个实施都是在一个区域内进行的108惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105--关于我们开发时间短，一切顺利。一些额外的俄罗斯卡协议功能，特别是长度大于2的协议此外，不正确的协议（如俄罗斯卡问题的非解决方案）可以很容易地证明是这样的，通过建立（众所周知的或其他）认识条件的失败这只需要对下面提供的脚本进行（几乎）微小的更改即可获得正确的协议。在第二节中，我们提出了俄罗斯卡问题。第3节至第5节分别讨论了在模型检查器MCK、DEMO和MCMAS中实现俄罗斯纸牌问题的第6节比较了结果。MCK、DEMO和MCMAS输入脚本可以在www.example.com上找到http://www.cs.otago.ac.nz/staffpriv/hans/aoard/。2俄罗斯纸牌从一副七张已知的牌中，两个玩家每人抽三张牌，第三个玩家得到剩下的牌。 有三张牌的玩家怎么能公开地互相告知他们的牌，而第三个玩家不从他们的任何一张牌中知道谁持有它？这个“俄罗斯卡”问题起源于2000年莫斯科数学奥林匹克。 叫玩家安妮，比尔和凯斯，牌0，...，6，假设安妮持有0，1，2，比尔3，4，5，和导管卡6。为了手中的牌0， 1， 2，写012，对于发牌，写012.345.6，等等。从现在开始假设012.345.6是实际发牌。所有公告必须公开和真实。安妮能说的话不多。但是，她不能说“我有0或6”，因为这样凯西就知道安妮有0。但是安妮也不能说但安妮也不能说“我有0或1”。即使安妮同时持有0和1，这样她就不会冒着被凯斯消除任何一张牌的风险，从而获得关于单张牌所有权的知识因此，凯斯可以得出结论，安妮只会说就这样，凯丝一次学会了两张牌！Cath不知道和Cath知道之间的表面矛盾并不真正存在，因为这些观察是关于不同的信息状态的：只是公告可能会引起包含其他信息的进一步更新在《易经》中，“知”字不一定是“知”字惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105109Vp. 对于（n∈G<$n）<$，写作<$G：这是解释常识的途径虽然这对安妮、比尔和凯斯来说是一个很大的优势，但凯斯仍然不知道安妮或比尔的任何一张卡片，这对凯斯来说可能是有意义的。一个典型的例子是，当安妮说她持有012或没有任何这些卡，之后比尔说，凯斯持有卡6。详情参见[16]。事实上，一个解决方案的要求是，凯斯这样的公告被称为安全。俄罗斯牌问题的解决方案是一系列安全的公告，之后安妮和比尔（不一定包括凯斯）通常都知道安妮知道比尔这个（五手协议的实例）是一个解决方案：安妮说：“ 我 手 上 的 牌 是 0 1 2 、 0 3 4 、 0 5 6 、 1 3 5 、 2 4 6 中 的 一张 ” ， 比 尔 接 着 说 ： “ 凯 斯 有 6 张 牌 ” 。请注意，比尔在这个序列之后，甚至公开知道安妮知道比尔如果我们用一只手来扩展安妮的公告，即245，如果公众知道安妮和比尔使用的pro-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to-to这对安妮和比尔来说是一个有用的安全功能，因为凯斯扮演了屋檐下的角色另一个后置条件是Anne的所有安全公告都确保Bill至少有一个安全响应，反之亦然。这种递归要求导致了更复杂的情况。参见[17]。公共宣告逻辑俄罗斯纸牌问题可以用公共宣告逻辑来我们给出了一个简洁的概述语言及其语义。给定一组代理N和一组原子P。一个认知模型M=域S，域S，域V，域S由（事实）状态（或“世界”）组成n：N→ P（S×S），V：P→ P（S）. 对于s∈S，（M，s）是一个认知状态对于n（n），我们记为n，对于V（p），我们记为Vp。所以，可以将V看作是一组等价关系，V可以看作是一组赋值G组。公告的语言可以归纳为：：= p| ¬ϕ|（李伟杰）|Kn|CG|[]其中p∈P，n∈N，G∈N是任意的。 将“Kn"改为110惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105|知道公式"将“CG"改为将[]改为公开宣布“知识”的结果是将认识状态限制在“知识”所处的所有世界。因此，语义如下。 给出了一个认识模型M=S，V，V。M，s|= pi ∈ VpM，s|=<$i M，s|=M，s| =100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 = m和M，s=||M，s |= Kn<$i <$，对所有t ∈ S：s <$nt蕴涵M，t|= M，s |= CG<$i <$for all t ∈ S：s <$Gt impliesM，t |= M，s |=[] i M，s |=隐含M|，s |=模型M|=SJ<${sJ∈S| M，S，J|=}JnVpJ Vp换句话说：模型M是限制在所有状态的模型M，其中包括状态之间的访问公式1适用于模型M，符号M| = 0，当且仅当对于M的定义域中的所有状态s：M，s| = 0。公式有效，符号|= m，当且仅当对于所有模型M：M| = 0。我们现在在这个逻辑中模拟俄罗斯纸牌问题。给定一堆已知的牌和一些玩家，玩家从牌堆中盲目地抽取一些牌在这样发牌的状态下，但没有进行任何种类的游戏动作，通常知道牌是什么，它们都是不同的，每个玩家有多少张牌，玩家只知道自己的牌。从最后一点可以得出，如果一个代理人在两张牌中持有相同的牌，并且如果所有玩家在两张牌中持有相同数量的牌，那么对于她来说，两张牌是相同的。这导致了交易的等价关系。一个认知模型（罗斯，012。三百四十五012.第012章交易三百四十五6，我们投资，编码的知识的球员安妮，比尔和凯斯（a，b，c），惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105111∧331∼这张牌 它包括。七尺。4英里。1个月= 140笔交易。对于每个玩家，访问状态之间的关系是由上面的等价性引起的，例如，012。三百四十五6a012. 346. 5说安妮不能区分这两张牌（因为她的手两者都是012）。关于卡所有权的事实写为qn，表示“卡q由y pla y er n持有”。事实0a（安妮持有牌0）的价值V0a由安妮手中出现0的所有 60笔交易组成在一系列的公告，这是一个俄罗斯卡问题的解决方案，它应该举行安妮知道比尔aknowowsbsq=0..6（Kaqb<$Ka<$qb）b已知为q=0.. 6（Kbqa<$Kb<$qa ）c ignorant<$q=0.. 6（<$Kcqa<$Kcqb）我们在前一节中指出，这些条件太弱。这可以通过观察得到例证，例如，罗斯012三百四十五6|=[Ka（012 a<$（<$0 a <$$>1a<$$> 2a））][cignorant]<$c ignorant在安妮说她的手牌是012或她没有持有任何这些牌之后，c ignorant是真的，但进一步更新（换句话说：当Cath可以假设这是真的时）使Cath学习安妮的一些 避免这种复杂性的实际所需的后置条件是：在每次宣布执行的协议之后，公众都知道Cath是无知的，并且在整个协议执行之后，Anne和Bill通常都知道：Anne知道Bill知道她的牌，并且Bill知道Anne知道他的牌。同样使用Cab（Kba knows bs<$Kab knows as）等价于Cab（a knows bs<$b knowsas），这被形式化为Cab（a knowsbsb knows as）CABCC无知关于协议：当安妮宣布然后可以证明，罗斯012三百四十五6|=[Ka[Ka] Cabcc ignorant] Cabcc ignorant112惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105我我我∈ R因此，在这种情况下，意图确实实现了，与上面不同：公告是安全的。我们忽略了进一步的复杂性，即安全公告需要安全响应。第2节中给出的解决方案由连续的公告组成一个宣布一个宣布b宣布2006年c时间认知逻辑我们提出的两个模型检查器需要解释系统表示和/或时间认知逻辑公式的验证因此，有些话是为了如何将这些与动态认知环境进行比较。一个解释系统I是由一组全局状态G和一组与这些状态相关的游程R组成的对（G，R）一个全局状态g∈ G是一个元组，由每个代理的局部状态gn和环境的状态gnA runr是一系列全局状态。 发生的第m个全局状态在运行中，r被称为r（m），并且在全局状态r（m）中的代理n的局部状态被写为rn（m）。一个点（r，m）是由一个游程和一个时间点m组成的对在一个解释系统中，代理可以区分全局状态，如果他们在两者中具有相同的局部状态，这导致（r，m）<$n（rJ，mJ）i <$r（m）<$nrJ（mJ）i <$rn（m）=rnJ（mJ）由于对当地和环境状态价值的明显估值，这就定义了一个认识模型。为了方便起见，我们一直在为此写作给定一个实际点（rJ，mJ），我们就得到一个认知状态（，（rJ，mJ））。认知和（LTL）时态（下一个）运算符具有以下解释：I，（r，m）|= X i I，（r，m + 1）|=I，（r，m）|= Kn 我的 对于所有（rJ，mJ）：（r，m）<$n（rJ，mJ）蕴涵I，（rJ，mJ）|=现在我们来概述一下“next”和announcement运算符之间的关系 公告被视为一个完全可观察的时钟滴答声，使系统同步。 当从点（r，m）过渡到点（r，m +1）时，通过改变某些环境变量p的值来模拟在时间m宣布不确定性，并将该信息传递给代理的局部状态。在时间m可用的静态信息包含在限制I中|m的解释系统I的所有点，惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105113∗我|我|时间m.这就决定了纯认识公式的意义。但是对于包含认知算子和假设对于每个时间m，都有一个公式m，使得m处允许的唯一转换是由m的声明引起的转换。我们可以定义一个翻译，在这里，给定一个认知状态和一个公式，该公式中的每个X-算子都被一个相应的动态算子所取代。以下内容现在都是等价的如果I，（r，m）|= π，则I，（r，m）|= X如果I，（r，m）|= m，则I，（r，m + 1）|=如果我|m，（r，m）|那我|M|（r，m）|=我|m，（r，m）|=[]如果和都是纯认识的，那么=，=，我们有I，（r，m + 1）|=对应于I|M|（r，m）|=有趣的是，观察到在前者中的检查“0”涉及（给定同步完美回忆）（m+ 1）的整个域，而在后者中的检查“0”仅涉及其前趋者m的“0”状态，对应于从m到m+ 1的转变中重置的环境变量的仅一个值对于3型号CNOMCKMCK，即整体设置假设一些代理人在一个环境中，通过时间的发展。这是由一个解释的系统，代理根据协议执行操作建模动作和环境可能在每个时刻都只能部分地被观察到。不同的方法来实现时间和认知的相互作用和定义。知识可以仅基于当前观测、基于当前观测和时钟值以及基于所有观测和时钟值的历史。最后一个对应于同步完美回忆。我们采用了这种方法。在时间维度上，具体化公式可以描述系统沿着114惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105单个计算，即， 使用线性时间时态逻辑（LTL），或者它们可以描述所有可能的计算的分支结构，即使用分支时间或计算树逻辑（CTL）。我们使用 LTL 。 如 http://www.cse.unsw.edu.au/~mck/ 需 详 细 信 息 ， 请 参 阅www.example.com。在MCK中，我们必须重新解释第2节中的动态认识论。 在一个程序rus.mck中，我们依次引入环境变量并初始化它们;我们创建了三个代理A、B和C，并使用相应的协议“anne”、“bill”和“cath”;程序的主要部分指定了由发牌和公告引起的（时间）转换，这些转换将这些玩家的不同信息状态联系起来;最后，rus.mck包含了一个部分，其中包含了所创建的时间线的各种待验证属性。代理人的一手牌由七个布尔值的列表编码，例如一手牌：布尔[7]指定所有牌0，...，6它们是否由Anne持有，使得当Anne持有卡0时，annecards[0]为真，等等。代理A，对于安妮来说，是由agentA“anne”（a_hand，a_announce，b_announce，stage）代理人的名字是A。它使用协议“安妮”。 它可以与括号之间的变量交互，并可能观察括号之间的变量其中第一个显然只能由安妮观察到，其他的将在其他代理定义中重新出现，因为它们是公开可观察的。可变阶段是rus.mck的transitions部分指定在协议执行的不同阶段会发生什么。我们区分阶段（时钟滴答声）0，1，2和3。在第0阶段，牌被分发给玩家，顺序为0，...，6.我们把它显示到牌0的发牌stage== 0->beginif钠3-> begin a_hand[0]：=True; na：= na+1 end []nb< 3 -> begin b_hand[0]：=True; nb：= nb+1 end []nc == 0-> begin c_hand[0]：=True; nc：= 1 endfi;变量na、nb和nc是用来记录代理人有多少张牌的计数器，[]表示不确定性选择。在过渡的这一部分中，创建了140个不同的交易，表示为140个不同的时间线。在第一阶段，安妮宣布她的手是012、034、056、135和135中的一个。246.这是通过执行协议“anne”间接完成的，该协议包含一个惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105115与这五笔交易相对应的条件，这会导致宣布行动被处决这就导致了原子a声明成为真。stage == 1/\ A.Announce -> a_announce：= True在第二阶段，比尔宣布凯斯持有第6张牌。或者，我们可以模拟比尔宣布凯茜的卡片- Bill的公告是通过操作B.Announce进行的，并导致变量bannounce变成现实这是过渡到第三阶段，最后阶段。我们可以想象整个系统由140个不同的运行组成变量a announce和b announce在阶段2和阶段3中是否分别为真，取决于该运行中的交易安妮的治疗方案是协议“anne”（卡片：observable Bool[7]，a_announce：observable Bool，b_announce：observableBool，stage：observable Counter）开始跳过;如果（（cards[0]/\cards[1]/\cards[2]）\/（cards[0]/\cards[3]/\cards[4]）\/（cards[0]/\cards[5]/\cards[6]）\/（cards[1]/\cards[3]/\cards[5]）\/（cards[2]/\cards[4]/\cards[6]）->公告>>新闻中心端该协议的在第0阶段，什么也没发生：跳过。 在阶段1中，操作Announce<<被处决了 实际上，卡片的价值或实例对于安妮来说是一张卡片;见上，安妮是在哪里创建的。或者五个实际的手，一个多更长的协议根据安妮的实际手牌创建五张任意的手牌。 没有为阶段2指定任何内容：因此，默认情况下再次跳过此阶段。Bill有一个类似的协议，但他的协议以skip开始;skip，因为他的声明是在第2阶段。 而Cath根本不采取行动，这携带了协议skip;skip; skip。代理人的知识随着每个阶段的发展而发展，通过代理人最初，他们只观察自己的牌，安妮安妮不能区分两个州，因为她的观察结果在这两个州是一样的例如，在第1阶段，Anne无法区分交易的时间表116惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105012. 三百四十五6和012。346. 5、因为：两者都有相同的a hand值（对于所有七个变量），a announce在两种情况下都是true，b announce在两种情况下都是false。 但在第三阶段，安妮可以区分这些时间线，因为b announce对前者是真的，对后者是假的rus.mck的最后一部分列出了要检查的各种时间认知属性。例如，我们想验证Rus，012。三百四十五6 |[a announce] [b announce] Caba knows bs.MCK的当前版本（0.2.0）不支持在完美召回模块中指定公共知识运算符因此，我们验证在第3阶段，a知道bs在模型中是有效的。这与罗斯相对应|一个通告|B宣布|= a知道bs，这确保Rus|一个通告|B广播，012。三百四十五6|= Cabca知道bs。在这个特定的模型中，Caba知道bs，参与者Cabca知道bs也是有效的。spec_spr_xn =X 3（（a_announce/\ b_announce）=>（ KnowsAb_hand[0]）\/（KnowsAneg b_hand[0]）/\（...）（KnowsA b_hand[6]）\/（KnowsA neg b_hand[6]）部分规范sprxn意味着我们使用MCK的完美召回模块，X 3是三重“下一状态”时间运算符，从阶段0开始计数。因此，在阶段3中检查由运算符绑定的公式。同样，五手协议的其他属性也得到了验证。4模型DEMO该工具DEMO由Jan van Eijck开发[18]。DEMO是动态认知模型的缩写它允许建模认知更新，图形显示所涉及的Kripke结构（即， 认知或状态模型，以及表示认知动作的动作模型），认知状态中的公式评估等。认知模型在互模拟下最小化，动作模型在（更合适，更弱）动作仿真概念下最小化[19] 。 DEMO 是 用 函 数 式 编 程 语 言 Haskell 编 写 的 。 另 见http://www.cwi.nl/~jve/papers/04/demo/。模型检查器DEMO实现了[2]的动态认知逻辑在这种“动作模型逻辑”中动作模型也是基于多智能体Kripke框架的，但它没有携带赋值，而是具有为动作模型中的每个点分配前提条件的前提条件函数，其代表原子动作。系统中的状态更改是通过一个称为更新产品的操作完成的。这是一个受限制的模态产品。在这篇文章中，我们将注意力集中在公共和社会的行动模式上。惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105117不--公告这样的动作模型有一个单例域。我们避免细节，并在DEMO中进行公式的递归定义。表格=顶部|道具道具|阴性形式|Conj[形式]|Disj[表格]|CK [代理人]表格|CK [Agent] FormFormulaTop代表，Prop Prop代表原子命题字母（Prop的第一次出现意味着数据类型是“命题原子”，而Prop的第二次出现是实际命题字母的占位符，例如P0），Neg代表否定，Conj [Form]代表Form类型公式列表的合取，类似地，对于Disj，K Agent代表Agent的个体知识运算符，CK [Agent]代表[Agent]中列出的Agent组的公共知识运算符。一个公共声明的指向（和单例）动作模型是由一个函数public创建的，该函数以一个前提条件（公式）作为参数。更新操作指定为upd：： EpistM ->PoAM-> EpistM在这里，EpistM是一个认知状态，PoAM是一个指向的动作模型。更新生成如上所述的新的认知状态公式检查定义为isTrue：： EpistM ->Form-> Bool它的参数是一个认知状态和一个公式，它返回一个布尔值。演示中的俄语卡片在演示中，我们只能使用以小写字母p、q和r开头的命题字母，因此我们不能像第2节那样，将安妮持有卡片0的原子命题写成0a。相反，原子p，...，p6，q，.，q6，r，.，R6代表这样的原子命题。的名字p4相反对于p 0，我们可以任意地写为p，对于q和r也是如此。初始认知状态表征发牌中的知识012. 三百四十五6是按如下方式建造的 一组整数[0.. 139]代表140个不同的交易。每个整数与七个命题字母相关联- 在这种情况下对事实的估价。前两笔交易对应于（0，[P 0，P 1，P 2，Q 3，Q 4，Q 5，R6]），（1，[P 0，P 1，P 2，Q 3，Q 4，Q 6，R 5]）交易编号0代表实际交易012。三百四十五6. 一对两个整数是在一个代理n的可及性关系，如果该代理持有相同的卡，118惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105两个交易。安妮的两个这样的对是（a，0，0），（a，0，1）。DEMO假设任意的可访问性关系。因此，不幸的是，我们必须显式地列出每个代理的等价关系中的所有对，如上所述Anne的公告a announce对应于下面的名为a announce的单格顿动作模型，它由函数public生成。public（Ka（Disj[Conj[p，p1，p2]，Conj[p，p3，p4]，Conj[p，p5，p6]，Conj[p1，p3，p5]，Conj[p2，p4，p6]]））类似地，我们有一个行动模型bannounce，用于BillAnne知道Bill的一手牌，a知道bs的后置条件a知道wsbs=Conj[Disj[Kaq，Ka（Negq）]，Disj[Kaq1，Ka（Negq1）]，Disj[Kaq2，Ka（Negq2）]，Disj[Kaq3，Ka（Negq3）]，Disj[Kaq4，Ka（Negq4）]，Disj[Kaq5，Ka（Negq5）]，Disj[Kaq6，Ka（Negq6）]]同样的，b知道as和c不知道。模型检查器现在验证所构造模型的后置条件。在比尔宣布之后，安妮和比尔都知道安妮知道比尔的手牌，安妮和比尔也都知道比尔知道安妮的手牌。众所周知，Cath仍然无知：*RUS>isTrue（upd（updrus a_announce）b_announce）（CK[a，b]a_knows_bs）True*RUS>isTrue（upd（updrus a_announce）b_announce）（CK[a，b]b_knows_as）True*RUS>isTrue（upd（upd rus a_announce）b_announce）（CK[a，b，c]c_ignorant）True认知状态（updrus a announce）是用带有前提条件a announce的单例指向动作模型更新初始认知状态rus 认知状态（upd）bannounce）是更新认知状态（upd）的结果 Rusa announce），单例指向动作模型名为b announce（具有该前提条件）。惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）1051195型号MMCMASMCMAS是Model Checking Multi-Agent Systems的缩写。这个模型检查器是由Franco Raimondi和Alessio Lomus-cio [11]开发的。目前的版本是mcmas 0.6。系统描述和协议属性使用有序二元决策图进行验证，与MCK中使用的方法相比。 它扩展了现有的基于obdd的技术，niques的反应系统，增加了一个认知（ATL）和道义的维度的逻辑语言，并允许输入的解释系统。MCMAS是用C++语言实现的。有关更多信息，请参见http://www.cs.ucl.ac.uk/staff/F.Raimondi/MCMAS/网站。在MCMAS中，全局状态被表示为代理的局部状态的元组对于俄罗斯纸牌，代理Anne、Bill和Cath代表玩家，代理Env（环境）代表纸牌交易。代理安妮的本地状态需要五个组件，可以被视为变量;三个代表她手中的牌，两张现状和两张结果的公告MCMAS的0.6版本不支持描述代理本地状态的变量。 因此，我们将变量部分编码为单个字符串。例如，Anne的一个本地状态是a012tf。这意味着安妮持有牌0、1和2，安妮（真实地）在该本地状态是其组成部分的全局状态中做出，并且Bill的公告b公告不能在该全局状态中做出（是虚假的同样，我们有5个变量用于Bill，3个变量用于Cath。代理Env的本地状态有七个变量，因为它代表一个纸牌交易。一个例子是e0123456。这代表了012.345.6成交信息的改变采取通常的步骤：（1）卡片被展示给代理人，（2）安妮宣布一个宣布，（3）比尔宣布b宣布。所有可到达的全局状态都将包含在下一阶段中。 一个例子初始全局状态是（annnnn，bnnnnn，cnnn，e0123456）;一个“n”基本上意味着代理没有关于相应变量的值的信息，通过给变量值n建模。所以，bnnnnn意味着比尔的本地状态是他还不知道他的牌（前三个n），安妮还没有宣布（第四个n），比尔已经宣布了。他还没有宣布。上述全局状态（annnnn，bnnnnn，cnnn，e0123456）然后转换为（a012nn，b345nn，c6nn，e0123456），其中每个代理知道它持有什么牌。然后，安妮的a宣告被做出，导致转换到（a012tn，b345tn，c6tn，e0123456），并且b宣告最终导致（a012tt，b345tt，c6tt，e0123456）-这一次，比尔的宣告成功。这些状态转换在程序中指定例如，对于代理Anne，步骤一的转换如下：120惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105--（当前）座席Anne的本地状态，Env.Lstate是Env.a012nn如果（Lstate=annnnn且（环境Lstate=e0123456或环境Lstate=e0123465或环境Lstate=e0123564或环境Lstate=e0124563））;环境Env在转换期间不会改变，但这必须明确表示为e0123456，如果Lstate=e0123456;在MCMAS程序的例如ab_d0123456如果（Anne.Lstate= a012 tt和Bill.Lstate= b345tt和Cath.Lstate= c6 tt和Env.Lstate=e0123456）;是在全局状态（a012tt，b345tt，c6tt，e0123456）中（唯一）为真的原子。类似地，表示卡片所有权的原子，例如“Anne holds card 0”（安妮持有卡片0）的原子，被定义为以开始的巨大表达式（由60个a0，如果（环境Lstate=e0123456或环境Lstate=e0123465或.也 可 以 命 名 代 理 组 。 这 在 检 查 常 用 知 识 时 很 有 用 。例如， 表 达 式ABC=Anne，Bill，Cath;将由Anne、Bill和Cath组成的组标记为ABC。常识公式Cabc（0a→Ka 0a）则表示为CK（ABC，a0->K（Anne，a0））。 我们用后置条件Cabcc ignorant来结束这个简短的论述，它证明了Cath在两个声明都被发布之后仍然是无知的。–代表否定。2019 - 05 - 22 01：01：01（（啊！K（Cath，a0）和！K（Cath，b0））和（啊！K（Cath，a1）和！K（Cath，b1））和（啊！K（Cath，a2）和！K（Cath，b2））和（啊！K（Cath，a3）和！K（Cath，b3））和（啊！K（Cath，a4）和！K（Cath，b4））和（啊！K（Cath，a5）和！K（Cath，b5））和（啊！K（Cath，a6）和！K（Cath，b6）;6比较上述输入脚本的粗略性能结果基于PC配置Linux 2.4.30 i686 Pentium 4，800Mhz和2018M RAM。惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105121俄罗斯纸牌五手制协议所需的时间分别为：• MCK - 160秒（长BDD包）或109秒（CUDD BDD包）• MCMAS• 演示MCK和MCMAS的时间度量用于整个模型检查过程，即，模型构建和公式检验。对于MCMAS，它包括从C程序自动生成MCMAS输入脚本的时间DEMO的运行原理略有不同：首先，Haskell解释器编译RUS.hs和相关模块DPLL和DEMO。 只有这样，我们才能检查各个公式。我们测量了组合的自动生成、编译和检查步骤。然而，这些结果不能直接解释为模型检查器的相对性能的指示，因为它们是基于相当不同的建模和模型检查问题。一个区别是MCK输入脚本使用转换程序显式地表示发牌，而MCMAS和DEMO的输入已经在初始状态中显式地表示了发牌的结果另一个是MCK和MCMAS检查所有初始状态的时间属性，而DEMO检查单个初始状态的动态属性运行时也可能对建模中的特定选择非常敏感除了在本文中讨论的脚本，我们后来开发了一个更简洁的DEMO程序，以及一个替代MCK建模，其中发牌由初始状态的约束而不是程序表示。我们避免细节，而是参考配套网站。这些版本的复杂性结果如下• DEMO-new• MCK-new上面讨论的模型集中在交易012.345.6的特定情况下的公告我们还开发了一个MCK脚本模型，该协议为Anne提供了一个任意初始状态的五手公告。这个脚本目前需要大约3个小时来运行，并且仍然是我们实验的主题然而，大多数情况下，我们感兴趣的是如何多才多艺的工具似乎是，实现一个问题，最初制定的地方，和动态的认识，条款，到时间的认识条款和/或作为一个跨-122惠普van Ditmarsch等人/理论计算机科学电子笔记149（2006）105预处理系统换句话说，我们对开发时间和支持的功能比任何其他东西都感兴趣根据我们的经验得出的结论是非常初步的。在DEMO中实现俄罗斯卡问题花了大约半天