基于Spin/Promela的Woo-Lam协议安全性质高效验证

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于Promela语言,将P.Maggi和R.Sisto提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam协议为例,运用Spin工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。

从Woo-Lam协议到网络协议的抽象验证

形式化方法是验证加密协议的重要手段 ,提出了一种新的验证方法 ,该方法基于 Debbabi的推理规则 ,将参与者 ID|参与者密钥等数据结构从协议中抽象出来 ,建立起抽象的逻辑推理结构 .以 Woo- L am协议为例 ,通过逆向递推的方式得到了协议的所有攻击路径 ,并以图的形式表示其关系 ,详尽分析了协议的漏洞 ,最后 。

文化基因重组视角下的夏葛医学院建筑解读

以生物学基因重组理论为启发,借助文化基因视角,对近代岭南地区首家西医女校——夏葛医学院的历史建筑及其遗存林护堂进行解读。通过实地调研、原始设计图纸剖析和相关历史文献、档案的查阅,研究中西文化交融背景下,夏葛医学院的建筑基因从西式到中西结合式的演变过程,并探究其受到的外部文化的影响。发现林护堂建筑基因的重组主要表现为同源重组、位点特异性重组与异常重组,其中异常重组最为突出,并在建筑的显性与隐性因子中均有体现。为广州近代医院建筑及其装饰的研究提供了新的视角,并解析其文化基因交融重组的深层含义。

关于“为设计认证协议的一个简明逻辑”一文的注记(英文)

Buttyan等人提出了一个简洁的逻辑 ,他们把它用于改进 Woo- L am协议 ,并且未证明地声称 :改进后的协议是抗协议与自身的交互攻击的 .为表明他们的结论是不正确的 ,找到了改进协议的两个不同的攻击 ,并详细解释如何加以实现 .构造攻击的方式除了要求更细致之外 ,与 Debbabi等人的方式在本质上是相似的 .进一步的分析表明Debbabi等人的逻辑没有足够的能力推理交互攻击 。

认证测试方法在应用中出现的问题及改进

在应用中,当关键原子值发生多次形式转换时,需要进行多次认证测试。鉴于此,本文引入了关键分量(Key Component)的概念,提出了多重认证测试(Multiple Authentication Test)方法。使用该方法重新设计了Woo-Lam协议,通过两个"挑战-响应"回合,确保主体角色的非对称性和响应者对发起者的身份认证。设计出的Woo-Lam协议不仅避免了原协议经认证测试方法改进后存在的缺少主体标识的缺陷,而且避免了Abadi和Buttyan等人分别对原协议改进后存在的两个重放攻击。