spitojava：由spi演算自动生成的java代码的密码协议

《spitojava：由spi演算自动生成的java代码的密码协议》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、Spitojava：由SPI演算自动生成的java代码的密码协议摘要:这项工作的目的是描述一个自动生成java代码实现在正式规范中描述的协议语言SPI演算的加密oSpitojava是SPI演算的一组工具的一部分，还包括一个预处理器，一个分析器和一个安全分析仪。后者可以较为正式地分析协议和检测协议的缺陷。当一个协议进行了分析并且对其已经达到的正确性有足够的信心，Spi2Java可以生成一个相应的正确的Java实现的协议，从而大大减少在编码阶段引入的安全缺陷的风险。1简介一个在现代计算机科学中最具挑战性的实际问题是如何保证设计和实现正确的安全协

2、议。这样的协议扮演的角色是实现安全冃标，例如通过使用加密技术实现身份认证，保密性和完整性。出于这个原因，他们也被称为加密协议。最近，许多研究工作一直致力于分析加密协议的逻辑正确性的问题（如⑶⑹⑺⑵[11]）,而实现正确性的问题还没有被认为是这么多。其中一个可能的方法，从正式规范[7][12][9]实现自动牛成以确保实施正确性。如果代码发牛器是这样的，在生成的代码忠实地实现了本说明书和避免编程错误，可能会导致安全漏洞，实施正确的可取的。因此，如果源规范在逻辑上是正确的，那么它就实现了。在本文中我们将展示如何将这种方法可在框架屮投入实践，其中目

3、标代码语言是Java和密码协议在spi演算［1］中被指定，这个过程代数规范语言专门为这种协议定制。2SPI演算该SPI演算在［1］屮被定义为一个扩展口演算⑻与加密基元。它是一个为描述和分析加密协议而设计的过程代数语言。该SPI演算有两个基本的语言：术语，表示数据和流程，以代表的行为。在本文屮，我们只介绍一些功能SPI演算，通过一个例子，由于有限的空间。图。Fig..l显示了SPIcalculus1规范安德鲁［5］密钥交换协议。A->B：A,Na®a)CAB.pBO>CAB(XA,xNa).B->A：{(Na,klAB)}kABC

4、AB(XM5G).(ftceyStore)KeyStore.KeyStore(kAB).casexmsgof{xNa?xklAB}kABin[xNaisNa](*3KeyStore)KeyStore.KeyStore(kAB).(®klAB)CAB<{xNa,klAB}kAB>.A->B：{NaJklABCAB<{Na}xklAB>.cAB(xMSGcypher).casexMSGcypherof{xnewNa}klABin[xnewNaisxNa]KeyStore.B->A：NbcAB(dimy).KeyS

5、tore.(SNb)CAB.A->B：OOklABCAB<{M}xklAB>.0cAB(wcypher).case^cypherof{x}klABin0InSt(M)>(pA(M)

6、pBO)Figure1.TheAndrewProtocolspicalculusspecification本说明书是由两个过程描述命名为PA和PB,这代表了该协议的两个角色。该研究过程所表示的相互作用场景：PA和PB同时运行的一个实例。发起者角色的过程PA和研究所过程是由M数据参数化，且必须被发送。M作为一个参数明传，因为这是由安全分析

7、工具［3］所需的。与睦相反，在其他协议参数都是隐式的。Fig.l的左侧一栏显示交换的消息使用非正式的，直观的表示经常遇到在文献屮，其屮A-B：o意味着A发送消息给B。中间一栏显示pA的SPI演算规范流程，而右边栏展示过程中PB的行为。安德鲁协议假定每个进程都有一个其屮对称密钥存储的本地密钥库。由于密钥存储区明确参与协议，它必须在SPI演算中被建模。我们简单的建模策略是表示密钥存储作为单独的进程(在Fig.l中没有显示)，其与相应的协议交互主要通过专用的通信信道(密钥-存储通道)。获取和存储密钥的操作被建模为在密钥存储通道有区别地输入和输出。

8、更准确地说，…个密钥存储在…个允许其独特的标识的别名下的密钥存储区中。所以，检索存储的密钥的操作由下式表示KeyStore.KeyStore(kAB)其中的KeyStore表示交互通道，XA是别名和kAB是摘录自密钥存储区保存的可变量。相应的存储操作是由语句KeyStore说明，其中klAB是必须根据该别名为xA被存储的密钥。注意密钥存储区的可见性是由运算符@所限制的，所以它被认为是私有的过程。在安德鲁协议运行的屮，五种信息在pA和pB的通道cAB之间交换：1)pA的发送的pB其标识符A和随机数Na。pB收到的消息

9、，并将这两个字段分别存储在变量xA和xNa中。2)pB从它的本地密钥存储区中检索与PA共享的kAB,并建立一个新的密钥klAB,与xNa一起用kAB进行加密，并将结果发送给pA。