理论计算机科学电子笔记128（2005）123-143www.elsevier.com/locate/entcs防止定时攻击的静态验证通信协议迈克尔·布赫霍尔茨a，1斯蒂芬·吉尔摩b，2简·希尔斯顿b，3弗莱明·尼尔森a，4a信息学和数学建模丹麦技术大学，Lyngby，丹麦爱丁堡大学计算机科学基础实验室，苏格兰摘要我们提出了一个联合分析的通信协议，同时考虑安全属性和时间。这些不是协议的完全独立的观察;通过使用执行协议的定时观察，即使在存在不可破解的加密的情况下，也有可能计算出旨在保密的加密密钥我们的分析是基于表达的协议作为一个高层次的模型，并从这个过程中推导出的演算模型分析的帝国PEPA封装和LySatool。1介绍通过使用强加密和精心设计的通信协议，可以设计安全系统，允许发送者和接收者交换由认证保证人支持的机密消息，该认证保证人确认通信中主体的身份。对诸如此类的协议的正确性具有非常高的信心，1 电子邮件地址：mib@imm.dtu.dk2 电子邮件地址：stg@inf.ed.ac.uk3 电子邮件地址：jeh@inf.ed.ac.uk4电子邮件：nielson@imm.dtu.dk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.016124M. Buchholtz等人理论计算机科学电子笔记128（2005）123通过应用静态分析方法检测不需要的控制流来获得。这样的分析可以确保不存在从发送者或接收者到攻击者的信息流，攻击者试图窃听他们的对话或通过插入伪造消息或以其他方式破坏发送者和接收者之间的有意义的信息流来进行干扰。在对所使用的加密技术和所部署的通信协议的强烈和合理的信念的支持下，可能会得出这样的结论，即没有信息可以从通信中泄露并被攻击者获得然而，数字通信容易受到一种特别微妙的攻击形式的影响，这种攻击并不总是能够很好地防御。这些攻击中，信息是通过从定时获得的推断而泄露的，安全交互被称为定时攻击。成功的定时攻击的后果可能是灾难性的。成功的定时攻击可以泄露安全协议所依赖的加密密钥。被认为是隐私的消息现在可以被攻击者读取。此外，攻击者可以伪造数字签名的消息，从而完全破坏消息身份验证过程。以前人们认为，定时攻击只能应用于硬件安全令牌，如智能卡，它们已被证明能够暴露用于RSA解密的密钥[20]。在网络计算应用的背景下，人们希望网络固有的不可预测的延迟将引入足够的“噪声”，使定时攻击在这样的设置中不切不幸的是，当Brumley和Boneh能够对OpenSSL进行远程定时攻击时，这种希望被证明是错误的[8]。通过测量服务器响应解密查询的时间，Brumley和Boneh的攻击客户端能够提取存储在服务器上的私钥。他们的攻击适用于网络环境，但也适用于进程间和虚拟机环境。许多密码库完全忽略了定时攻击的问题，并且没有实现任何防御措施来防止它，因此这不仅仅是安全协议的一个特定实现的问题，而是一个没有被广泛理解的普遍问题，或者是一个正在使用有根据的分析方法进行系统性斗争的问题。在开发者可以访问其加密例程的实现的源代码的情况下，则可以添加RSA盲化的实现，其从随机数分配中提取并对其应用加密，以便向每个加密步骤所花费的时间添加随机延迟。有点问题，这种方法需要开发人员有能力和专业知识来实现这个操作，M. Buchholtz等人理论计算机科学电子笔记128（2005）123125正确的操作。在实践中，许多应用程序员不熟悉加密例程的细节，并且有真正的理由担心他们可能在修改其实现的过程中损害加密的完整性定时攻击可以通过对双方会话期间的消息交换进行定时来实现。不需要用户交互的通信部分具有足够的可重复性，这些交互的定时可以用于导出信息。任何用户交互，即使是单个按钮或按钮点击，也会引入足够的随机延迟来掩盖可能从定时信息中获得的任何信息实际上，在播种许多密码例程时，测量用户操作之间的时间被用作不可重复的、弱相关的随机数的来源当两方之间的安全会话可以被一个窃听器监控在成功的交互和失败的交互所花费的时间不同的情况下，则从通信中泄漏一位信息，即该会话是成功结束还是失败结束。一种情况是，如果窃听者在买方和卖方之间的会话期间对消息交换进行计时，则该单个信息位可能具有某种价值。较长的交互可能对应于购买股票（成功完成），而较短的交互可能对应于获得股票价格报价，没有随之而来的购买（失败结果）。如果他们无法破解所使用的加密，那么窃听者可以推断出一些股票已经被购买，但不知道购买了多少，也不知道是谁购买的。另一种对抗针对安全会话的定时攻击的方法，例如上述方法，并且不依赖于对如何安全地修改复杂加密例程的深入理解，是在重要交互中的较快交互中引入延迟，以便掩盖较慢交互和较快交互之间的差异。故意在协议中插入延迟似乎很奇怪。当然，我们应该关注使协议以最高速度运行，因此，我们应该加快执行成功或失败的交互需要更长的时间。如果我们对如何使长时间运行的交互更有效有一些额外的见解（使用更好的加密或身份验证算法，或使用无损压缩或其他方法压缩传输的数据 虽然这可能是理想世界中最理想的选择 实际上，我们可能没有更好的认证协议。此外，本发明还提供了一种方法，126M. Buchholtz等人理论计算机科学电子笔记128（2005）123为了实现更快的加密速率，我们可能倾向于使用较低等级的加密，因此这种方法甚至会产生这样的可能性，即通过试图减少两个交互中较慢的交互所与上述相反，我们总是可以通过引入延迟来使更快的路线变慢。这不需要发明具有未经测试的安全性和性能行为的新颖算法，也不需要利用先前未尝试过的认证协议。出于这个原因，我们将问题框定在填充具有延迟的协议方面，但我们的方法同样适用于我们确实有洞察力或技能来加速成功和失败路径中较慢的路径以与另一条路径保持一致通过向协议添加延迟所带来的修改引起了两个相互关联的问题：(i) 具有额外延迟的协议是否仍然是安全协议，或者延迟本身是否以某种方式损害了其安全性;以及(ii) 插入的延迟是否实际上实现了掩蔽成功完成的会话与不成功的会话之间的差异的效果？为了能够解决这些问题，我们需要有一种方法来有效地重新运行以前开发的协议的安全性和性能分析有可能采取一种工程方法来试图确定这些问题的答案，方法是在系统的实现中填充延迟，并在多次成功和失败的运行中对其进行分析。以这种方式重复测试可以给我们一些信心，即延迟填充已经达到了预期的效果，但很难相信我们可以达到与使用有充分依据的正式方法相同的信心水平为了对安全协议进行形式化分析，我们需要一个形式化的框架来描述协议并对这些描述进行分析而不是开发一个全新的框架，我们利用已经开发的建模形式和分析工具。我们分别使用过程演算LySa [11]和PEPA [18]进行安全性和性能分析。我们用来在这些演算中处理我们的模型的软件工具是LySatool [9]和带有DNAmaca[19]的Imperial PEPA编译器（IPC）[6，5]M. Buchholtz等人理论计算机科学电子笔记128（2005）123127defdefdef本文结构：我们继续概述我们在本文中使用的过程演算，研究它们的相似性和差异。在第3节中，我们描述了使用这些演算的方法，以实现安全性和性能的联邦分析。在第4节中，我们提出的文件，一个安全的移动移动商务应用程序，其中买方和卖方之间的交易是安全的使用“宽嘴青蛙”协议的案例研究第5节对相关工作进行了讨论，并给出了本文的结论。2结石概述LySa和PEPA结石用于不同的分析目的。LySa模型可用于确定协议是否安全，以防止恶意（或意外）伤害，即使在最难的攻击者存在的情况下也能保证可靠的信息交换。PEPA模型可用于确定协议是否在恶意（或意外）过载下继续执行，从而即使在存在增加的网络流量的情况下也能保证及时的信息交换。由于它们的不同目的，LySa和PEPA使建模者具有不同的语言结构。在本节中，我们通过使用一个常见的例子来对比PEPA和LySa过程演算的功能。 的意图在这一部分是给读者足够熟悉的符号是舒适的其余部分的文件。如果需要更多详细信息，请参见附录A和B。我们从一个简单的例子开始，它为用户打印文档建模。用户发出lpr打印命令，将文档发送到打印守护程序。 打印守护程序将它们转换为打印机，并将它们假脱机到打印机。在PEPA中，这些事件发生的比率被量化。传播中的生产者和消费者角色是不同的，因为生产者（生成作品）决定了它的速率并且消费者被动地接受这一点（不指定费率）。用户=（lpr，r1）。用户Daemon=（lpr，T）. （toPS，rPS）. （spool，rs）.守护程序打印机=（spool，T）。（print，rp）. 打印机Sy stemd=ef（UserDDaemonn）D打印机联系我们128M. Buchholtz等人理论计算机科学电子笔记128（2005）123接下来我们将展示这个示例的LySa版本LySa版本看起来非常相似，尽管在演示文稿中有一些小的差异：(i) LySa使用流程复制（通过！操作符），而不是将名称绑定到进程并使用递归实现循环行为;(ii) 在PEPA中，合作是对称的，而在LySa中，输入和输出在语法上是不同的，就像在π演算中一样;(iii) 在LySa中没有索引并行复合算子，进程在它们的所有通用名称上同步;以及(iv) 在LySa中没有单独的动作，因此我们引入了一个过程，该过程对PEPA环境进行建模，并具有匹配各个活动以形成输入/输出对的功能。为了便于一步一步的比较，我们引入了语法缩写的过程中使用的术语，虽然从技术上讲，这种符号不是LySa的一部分，它有无名的过程。User！你好，我是。0守护者！（lpr，rl;）。P.S.P.S.P.S. spool，rs. 0打印机！（spool，rs;）. 打印，rp。0环境污染！（toPS，rPS;）. 0 |！（print，rp;）. 0系统管理员用户|守护进程|打印机|环境PEPA中的合作已经被LySa模型中的模式匹配所取代。上面使用的模式需要输入和输出相同才能匹配。更具体地说，LySa输入要求分号之前的所有内容与输出中的值在分量上相同PEPA的操作由活动类型和活动速率组成。 这些由元组表示 在LySa模型中的大小2。我们可以观察到，攻击者不应该看到单个活动（因为它们不涉及跨网络的活动）。 如果我们不关心协议的时间行为，我们可以删除所有的单个活动，因此也可以删除环境，M. Buchholtz等人理论计算机科学电子笔记128（2005）123129defdefdef一个更简单的LySa模型User！你好，我是。0守护者！（lpr，rl;）。spool，rs. 0打印机！（spool，rs;）. 0系统管理员用户|守护进程|打印机然而，在本文中，我们当然关心协议的定时行为，因此我们现在和以后都保留了PEPA模型的各个活动。在随机过程代数中，通常将从过程传递到过程的数据值抽象出来。然而，在安全性和保密性的分析中，知道交互中的主体之间传递哪些消息是至关重要的。出于这个原因，我们现在考虑PEPA的符号扩展，PEPA与值传递和函数符号。在这个版本的用户打印文档的模型中，我们用一个注释来补充动作类型，该注释给出了正在传递的数据的本地名称。因此，用户将他的文件称为myFile，守护进程将其称为userFile，打印机将其转换为spoolFile后将其视为spoolFile。User=（lpr（myFile），rl）. UserDaemon =（lpr（userFile），T）.（toPS（userFile），rPS）。（spool（userFile），rs）。守护进程打印机=（spool（spoolFile），T）。（print（spoolFile），rp）.打印机Sy stemd=ef（UserDDaemonn）D打印机联系我们与PEPA相比，LySa在其语法中支持值传递。 值通过输入/输出对传递，其中传递值涉及值的精确匹配，以确保正确的输入和输出被结合以及形式参数名称与实际参数名称的绑定在下面的示例中，lpr上的匹配，rl活动产生绑定{userFile›→myFile}。在输入操作前缀的模式中使用的名称在语法上与那里使用的变量分开130M. Buchholtz等人理论计算机科学电子笔记128（2005）123一个分号。User！lpr，rl，myFile0守护者！（lpr，rl; userFile）。toPS，rPS，userFile设置spool，rs，userFile。0打印机！（spool，rs; spoolFile）. 打印、rp、spoolFile。0环境污染！（toPS，rPS; PSFile）. 0 |！（print，rp; printFile）。0系统管理员用户|守护进程|打印机|环境这个简短的例子说明了这里使用的两个进程演算之间的一些差异。我们将在后面的章节中讨论LySa演算中的加密和解密原语。3方法提炼到它们的本质，过程代数记录了离散事件系统中事件的因果顺序，该系统形成为并发活动通信过程的组合。这种系统视图允许验证模型的属性，这些属性可表示为事件之间的相互依赖性。通过以各种方式装饰模型中的事件，可以促进更丰富的分析。一种装饰是对事件持续时间的估计;另一种装饰是对价值的安全分类的记录。反过来，这些类型的装饰导致我们的随机过程代数和微积分的安全分析。不同的分析方法适用于不同类型的语言。这些分析在性质和用途上是如此不同，以至于它们应该被分别贴上静态分析和动态分析的标签和分类。我们希望对一个协议同时进行静态分析和动态分析，所以我们应该先问应该进行哪种分析。静态分析比动态分析在计算上更便宜，因此应首先完成静态分析。如果静态分析过程的结果令人鼓舞，那么接下来将进行动态分析。首先进行动态分析是一种不太谨慎的做法，因为如果随后的静态分析发现模型不令人满意，则必须放弃模型动态分析的计算成本更高的结果。3.1从UML图为了驱动所研究的协议的静态和动态分析，我们从表示为UML项目的协议的根描述开始，M. Buchholtz等人理论计算机科学电子笔记128（2005）123131在此基础上，提出了一个用于静态安全分析的LySa模型和一个用于动态性能分析的PEPA模型UML项目是我们执行的安全性和性能的联邦分析的基础，它包含许多不同类型的图。其中包括类图，序列图，状态图和协作图。在我们的例子中，这些包含额外的注释，从中可以提取LySa和PEPA模型的形式对象。在DEGAS项目中，我们实现了称为提取器的软件组件，可以自动执行此过程。 在先前关于ForLySa浸提器[10]和PEPA浸提器[13]的出版物中讨论了浸提过程，因此我们不在此进一步讨论3.2PEPA和LySa模型我们在前一节中了解到，我们使用的过程演算模型有一个共同的根（它们来自同一个表示为UML项目的高级模型我们现在讨论这些派生模型之间的关系，在正式的语言条款时，他们被视为过程，产生标记的过渡系统。LySa模型表示与无限数量的工作主体副本的交互。与此相反，PEPA模型表示与有限数量的工作主体副本的交互。组件的数量是固定的，进程不会在PEPA中动态生成。两种模型之间存在差异的原因是要进行的分析类型不同，如下所示。• 在分析安全性时，我们希望确定我们不排除当协议的许多运行同时处于活动状态时可能发生的攻击。因此，我们在LySa中使用进程复制对协议进行建模，并且LySatool使用在一个足够大的范围内实例化的参数化复制来计算其最佳近似。• 在分析性能时，只要模型中至少有一个每种类型的主体，我们就可以计算感兴趣的度量。组件的附加副本将导致更大的状态空间生成和模型解决方案成本，而不改变可以计算的度量因此，在PEPA模型中，我们使用所需的最少数量的主体。这种差异的一个后果是，可能天真地期望在两个模型之间保持的强关系（例如互模拟等价）并不成立。然而，微量地下水坑的关系较弱-132M. Buchholtz等人理论计算机科学电子笔记128（2005）123事实确实如此：PEPA模型的每一个可观察到的转换序列都是LySa模型的可观察到的痕迹（但不是相反）。此外，如果主体的附加副本被添加到PEPA模型，则由PEPA模型生成的跟踪继续被LySa模型的跟踪所包含。因此，LySa模型的观察结果代表了PEPA模型在极限下的行为，因为越来越多的主体参与了协议所描述的交互。4案例研究：安全的移动商务我们考虑一个小的案例研究，买方和卖方使用Michael Burrows的“宽口青蛙”（WMF）协议进行安全通信，在协议开始之前，买方与卖方进行初步联系以建立连接。在协议完成后，有一个最终的握手，关闭连接。初始接触和最终握手都可以被攻击者看到，这是定时攻击的基础。这样一个系统的设计似乎从根本上令人敬畏。为什么买方和卖方之间的所有通信都不受安全协议的这样做的原因是，我们考虑的应用程序是一个安全的移动商务（移动电子商务）的应用程序，买家和卖家自发地满足和建立连接。因此，业务拓扑不是静态的，因此虚拟引入是必要的。诸如PDA和手持设备之类的小型设备是移动计算应用的基本执行平台，但是诸如这些设备的计算和存储能力有限，并且不能支持许多同时连接。这使得虚拟告别成为我们应用软件模型的必要我们关心的是，攻击者是否可以从安全的移动商务应用程序的实现的时间分析中得出成功/失败的推断，假设他们可以通过扮演买方的角色并编译成功和失败结果的时间表来确定买方和卖方之间大量交互的时间4.1静态分析从认证分析的角度来看，在移动电子商务环境中使用的WMF协议的描述的突出点在于，它旨在在一个或多个用户之间建立秘密会话密钥KAB下的安全会话。M. Buchholtz等人理论计算机科学电子笔记128（2005）123133买方A和卖方B，他们是对话中的两个主体可信服务器用于建立安全会话，并且A已经向服务器注册了主密钥KAS。类似地，B已经向服务器注册了KBS该协议有三个步骤，我们首先非正式地描述。• 主体A向服务器发送一条消息，其中包括B的名称和新的会话密钥KAB，并在KAS下加密。• 服务器解密并发送A的名称和新密钥KAB到B，在KBS下加密• 主体A向B发送在KAB下加密的消息。在LySa中，该协议可以被建模为三个并行过程，分别代表主体A、B和S。在图1中，我们将每条消息的源地址和目的地址建模为消息的前两个值。请注意，这些地址是明文发送的，因此允许攻击者随意修改或伪造地址信息。LySa中的对称密钥加密被写为{B，KAB}KAS，表示主体B的名称和会话密钥在密钥下加密主体A与服务器共享哪个。该消息的相应解密在服务器处以单独的语言结构在进程PS中它检查是否使用了正确的密钥进行加密，并额外使用匹配来确保加密中的第一个值是B，然后将第二个值绑定到变量zk。ν算子是π演算的一个分支，用于生成新的会话密钥和新的消息内容。除了对称密钥加密之外，LySatool还支持公钥/私钥对加密，但在此协议中没有使用。Wide-Mouthed-Frog协议的LySa模型已经被注释了关于该协议预期具有的认证属性的信息。LySatool进行的静态分析能够判断当与Dolev和Yao [ 14 ]风格的为了指定这些认证属性，我们首先引入标签或密码点，例如[ata1]和[ats1 ]，以表示信息被加密或解密的位置。其次，在每个加密点，我们描述了一组目的地密码点，该消息是要解密。在这种情况下，例如上面，我们确切地知道消息的预期接收者，这个集合只有一个元素。第三，在每个解密点，我们通过给出一组可能的起源点来断言我们认为该消息被加密的位置。LySatool执行的静态分析通过计算LySa进程在所有执行过程中可以做的事情的过度近似来工作134M. Buchholtz等人理论计算机科学电子笔记128（2005）123与任意攻击者并行执行。该分析将计算有关哪些消息可以通过网络发送的信息，并计算有关哪些值可以绑定到模型中使用的变量后者包括可能发生在攻击者内部的变量，因此分析将报告特定值是否会被攻击者所获取，即该值是否是机密的。LySa过程还使用指定消息的预期来源和目的地的身份验证属性进行注释。静态分析也将报告这些属性的违规。由于分析计算过程行为的过度近似，它也可能报告太多错误。在[4]中，证明了关于LySa的形式语义，分析不能报告太少的错误，并且还说明了报告太多错误在实践中不会造成大问题从技术上讲，静态分析被指定为流程逻辑，它给出了流程行为如何在分析结果中表示的逻辑描述。例如，分析结果包含关系κ，该关系κ用于跟踪可能通过网络传输的可能消息元组。为了生成描述例如LySa过程的输出如何影响分析结果的公式，我们使用以下形式的约束生成函数GG（κa，b，c<$.P）=（a，b，c）∈κ <$G（P）这表明要分析LySa进程a，b，c.P，必须保持元组（a，b，c）存在于κ中，因为该元组可能在进程的某个运行中发送。此外，必须对过程P进行分析，这将在输出之后执行。类似的约束生成发生在LySa的其他语言结构中。实际的分析结果是通过找到一个关系κ（和其他分析分量）来计算的，它满足生成的公式。这是通过使用解决逻辑约束系统的标准工具来完成的。为了执行分析过程，LySa模型被编码为一阶逻辑的片段，并且可以通过简洁求解器[21]找到约束的解。保证分析结果的计算在LySa过程大小的多项式所限定的时间内终止。对LySa的完整分析可以在[4]中找到，而对Chronow逻辑的全面介绍可以在[22]中找到。WMF协议的LySa模型如图1所示。LySatool确认在WMF协议中从A发送到B的消息是机密的，会话密钥KAB也是机密的，因为两者都不能进入到WMF协议中。M. Buchholtz等人理论计算机科学电子笔记128（2005）123135defdefdef=P啪！（ν KAB）<$A，S，A，{B，KAB}KAS [at a1 dest s 1]<$.（vmessage）A，B，{message}KAB [ata 2 destb 2]. 0PB！（S，B; x）. 将x解密为（A，B ; y）中的{A;xk}KBS [atb 1 origs 2]。在0将y解密为{;ym}xk[atb2origa 2]PS！（A，S，A; z）。将z解密为{B;zk}KAS[ats1origa 1]，B，{A，zk}KBS [at s 2 dest b 1]0WMFLySa®A|PB|PSFig. 1.宽口蛙协议攻击者在协议的任何运行中的行为此外，认证属性确实适用于这个版本的协议，尽管模型的小变体容易受到并行会话攻击。关于WMF协议的这些LySa编码及其分析的更多信息可以在[4]中找到4.2动态分析图2显示了宽口青蛙协议的PEPA模型。这记录了协议的因果关系信息（通过要求A首先与服务器通信，以及随后的依赖关系），并通过使用随机变量作为负指数分布的参数来PA=（as，ras）. （ab，rab）.PAPB=（sb，T）. （ab，T）.PBPS=（as，T）. （sb，rsb）.WMFPepadefDA{as，ab}（P、S、D、P、B）{sb}图二. 宽口蛙协议通过使用IPC/DNAmaca工具链，我们能够通过计算稳态、瞬态和瞬态分布来分析PEPA模型，如图2DNAmaca解算器提供了直接和136M. Buchholtz等人理论计算机科学电子笔记128（2005）123迭代求解方法，Krylov子空间技术，以及马尔可夫和半马尔可夫过程的基于分解的方法。所有PEPA模型都生成连续时间马尔可夫链（CTMC），因此我们只使用DNAmaca提供的马尔可夫分析功能。从纯马尔可夫系统中提取时间的DNAmaca版本（发布版本HYDROGEN）使用均匀化来计算时间密度和累积分布。这种精确解方法相对于离散事件模拟的近似方法的优点包括解的效率更高，并且不需要根据难以计算的置信区间来解释结果，置信区间估计模拟结果中误差的界限DNamaca工具实现的方法已被证明可以扩展到非常复杂的模型，这些模型生成的状态空间超过1500万个状态[7]。在这里，我们使用IPC/DNAmaca工具链来计算协议成功运行和失败运行的时间分布之间的差异。 我们对成功运行和失败运行之间的差异的成功混淆的度量将是它们所观察到的完成率之间的相对差异是否小于所选择的小容差。观察到的完成率绘制为累积密度函数（CDF），显示完成的概率如何随着时间的推移而增加。使用IPC/DNAmaca计算填充延迟前后模型的CDF。图3示出了要插入到协议的执行中的延迟的合适值的确定。图中的平滑贝塞尔曲线说明了成功运行的方案，作为我们实验的参考点。我们希望通过改变插入到协议中的延迟量，使其他图尽可能接近该参考曲线对于要插入到故障场景中的延迟值进行三种估计，0.5、1.0和2.0秒（分别绘制为菱形、加号和方框符号）。0.5秒的延迟是不够的，这意味着较快的路径仍然比较慢的路径快。2.0秒的延迟会过度补偿，并在另一个方向上出错，使快速路径的修改比慢速路径慢，并且可能仍然可以检测到差异。插入1.0秒的延迟似乎是一个合理的补偿。进一步的调优可能会在0.5和1.0之间找到一个更好的值。使用Imperial PEPA分析仪和DNAmaca以及随机探针方法[3]来选择不同的传代起点和终点，可以使重复的实时分析过程自动化。M. Buchholtz等人理论计算机科学电子笔记128（2005）123137Q+Q+宽口蛙1QQ Q QQQQQQQ0.9QQQ++Q++QQQQQQ”“延迟=0.5”0.8Q+Q+QQQQQ”+的” Q0.70.6Pr 0.50.40.30.20.10 Q+QQ+QQ+QQQ+QQ+QQQ+Q0 1 2 3 4 5 6 7 8 9 10以秒为单位的图三. 从WMF方案ysis。重复分析的目的是排除基于将通过系统的一条路径的定时与另一个，并从中间接推断。证明这些时间分布对于通过系统的所有可观察路径都是可接受的，这些路径不涉及用户交互或其他随机随机延迟源，这足以表明基于聚合定时观测结果的定时攻击是不可行的。通过为原始协议和填充有延迟的协议版本的分布之间的最大容许差异选择一个值，有可能将定时攻击的难度增加到这样一个点，即使用该协议的网络应用程序的用户满意于定时攻击很难发动，攻击者这样做是不经济的。5相关工作Focardi等人对安全协议中的定时信息泄漏问题进行了深入的研究。[16]和[ 17 ]中的密码协议的上下文中。在这项工作中，作者使用了安全进程代数的实时扩展[15]。使用离散时间域，并假设过程是同步的。在[16]中，作者开发了一个基于双向模拟的非演绎成分属性的定时版本，并表明这对于检查是否存在隐蔽信息流是有用的。在[17]138M. Buchholtz等人理论计算机科学电子笔记128（2005）123这项工作被扩展到密码协议分析。一种方法与我们的方法有一些相似之处，并且具有协调安全性和定时行为的类似目标，这已经在Appla-pano和Smith关于并发语言的概率不干扰的工作中被采用[23]。这项工作使用马尔可夫链来研究并发线程之间的时间泄漏所产生的概率行为的调度程序。Agat和Sands的论文[1，2]考虑在实现中引入虚步骤，以保证快速路径不比慢速路径快，他们构造了类型和转换系统，将顺序命令程序P转换为安全版本Pj，该版本PJ在时间无知语义中是语义等价的，并且不允许关于时间遵守语义（由模拟结果表示）的泄漏。我们的工作与他们的不同之处在于，我们认为协议表达在一个高层次的设计中使用注释的过程代数在对比，以命令式语言程序的Agat和Sands。因此，我们的工作有可能适用于一系列令人满意的实现所使用的协议，而不是只有一个单一的实例。6结论在新的通信协议的创新和实验设计中，有必要考虑新设计的安全性和性能，其中性能分析的目标可以是补充由加密和认证提供的强安全性。形式语言在这里是有用的，因为它们提供了一个明确的声明的协议，因为他们是服从自动分析。这些分析也依赖于被检查的属性的明确表达在这样的设置中，安全和性能分析都可以在协议更改后重新运行，以确保更改没有不利影响。我们在这里应用这种方法来分析买方和卖方之间安全通信的高级模型。安全和性能问题往往是不一致的。通常情况下，关注实现峰值性能的应用程序开发人员将内置于应用程序软件层中的安全措施视为执行时间的开销。然而，在当今的网络世界中，安全性不是一个可有可无的额外因素，因此性能分析和安全性分析必须和谐地一起工作。在本文考虑的例子中，我们已经说明了性能分析如何补充系统安全的静态分析，以及控制流分析如何增加M. Buchholtz等人理论计算机科学电子笔记128（2005）123139系统行为的随机模型的值因此，每一项分析都加强了另一项分析的有用性，为设计可靠的系统提供了急需的帮助，从而保证了安全性和性能。确认作者得到了全球应用设计环境项目（DEGAS）IST-2001-32072的支持，该项目由全球计算的未来和新兴技术主动计划资助。作者感谢PASM研讨会的匿名评论者提供的有用评论。Monika Maidl对本文的早期版本提供了详细的评论，这有助于我们改进整个阐述。Imperial PEPA过滤器由Jeremy Bradley开发，可从http://www.doc.ic.ac.uk/ipc 网 站 。 LySatool 和 LySa 提 取 器 可 从http://www.imm.dtu.dk/cs_LySa/获得。 PEPA提取器是 PEPA提取器的一个组件，可以在URL：http://www.dcs.ed.ac.uk/pepa上找到。引用[1] Agat，J.，Transforming out timing leaks，in：Proceedings of the 27th Annual ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages ， Boston ，Massachusetts，2000.[2] Agat，J.和D. Sands，关于保密性和算法，在：IEEE安全和隐私研讨会论文集（2001），pp.六十四比七十七[3] Argent-Katwala ， A. ， J. Bradley 和 N. Dingle ， Expressing performance requirementsusingregular expressions to specify stochastic probes over process algebra models ， in ：Proceedings ofthe Fourth International Workshop on Software and Performance（2004），pp. 49比58[4] Bodei角，M. Buchholtz，P. Degano，F. Nielson和H. Nielson，协议叙述的自动验证，在：第16届IEEE计算机安全基础研讨会（CSFW'03）（2003），pp. 1-15。[5] 布拉德利，J.，N. Dingle，S. Gilmore和W. Knottenbelt，使用IPC推导PEPA模型中的时间密度：Imperial PEPA计数器，在：G. Kotsis，编辑，第11届IEEE/ACM计算机和电信系统建模，分析和仿真国际研讨会论文集（2003年），pp. 344-351[6] 布拉德利，J.，N. Dingle，S. Gilmore和W. Knottenbelt，使用HYPERT工具从PEPA模型中提取通道时间：案例研究，在：S。Jarvis，编辑，第十九届年度英国性能工程研讨会论文集，华威大学，2003年，pp.79比90。[7] 布拉德利，J.，N. Dingle，P. Harrison和W. Knottenbelt，大型半马尔可夫模型中的通过时间分位数和瞬态分布的分布式计算，在：并行和分布式系统性能建模，评估和优化国际研讨会论文集（PMEO-PDS 2003），法国尼斯，2003年4月26日，2003年，pp. 281-289.URLhttp://aesop.doc.ic.ac.uk/pubs/passage-pmeo2003/[8] Brumley ， D. 和 D. Boneh ， Remote Timing Attacks are Practical ， in ： ConferenceProceedingsofthe12thUSENIXSecuritySymposium（2003），pp.1http://www.usenix.org/publications/library/proceedings/sec03/tech/brumley.html140M. Buchholtz等人理论计算机科学电子笔记128（2005）123[9] Buchholtz，M.，LySa-一个过程演算，由丹麦技术大学的信息学和数学建模主办的网站（2004年），http://www.imm.dtu.dk/cs_LySa/。[10] Buchholtz ， M. ， C. 蒙 坦 格 罗 湖 Perrone 和 S.Semprini ， For-LySa ： UML forauthentication analysis，2004，to appear.网址http://www.imm.dtu.dk/pubdb/p.php? 3235[11] Buchholtz ， M. ， H. Nielson 和 F. Nielson ， A calculus for control challenge flowanalysis of securityprotocols，International Journalof Information Security（2004），可在http://dx.doi.org/10.1007/s10207-004-0036-x在线获得。[12] Burrows，M.，M. Abadi和R. Needham，A logic of authentication，ACM Transactions onComputing Systems8（1990），pp. 18比36[13] Canevet，C.，S. Gilmore，J. Hillston，M. Prowse和P. Stevens，使用UML和随机过程代数进行，IEE Proceedings：Computers and Digital Techniques150（2003），pp.107-120[14] Dolev，D.和A. Yao，On the Security of Public Key Protocols，in：22nd Annual Symposiumon Foundations of Computer Science（1981），pp.350-357.[15]福卡尔迪河和R. Gorrieri，安全属性的分类。 第一部分：信息流，载于：安全分析和设计的基础，LNCS2171（2001），pp。331-396.[16] 福卡尔迪河，R. Gorrieri和F.Martinelli，实时信息流分析，IEEE Journal on Selected Areasin Communications21（2003），pp.20-35[17] 戈 列 里 河 和 F.Martinelli ， A simple framework for real-time cryptographic protocolanalysiswith composite proof rules，Science of Computer Programming 50（2004），pp. 23比49[18] 你好，J。，“A Comp osit io n a l A pp r oa c h to P erforma n ce M o d elli n g，“C am b r i d g e U niversity y Press，1996.[19] 知 道 了 ， W 。 ， “ Ge ne r a i l i s e d M a rko v i a n a n a
