Reconsidering Restaurant Bans

Recently, a statement by the Beijing Administration for Industry and Commerce stopping restaurants and catering services from banning outside beverages has provoked heated debate among the public.

基于身份认证的BACnet/IP分析与改进

为了解决BACnet/IP身份认证存在多种可攻击漏洞和密钥泄露带来的安全问题,提出了一种安全增强的BACnet/IP-SA协议认证方案。研究协议身份认证消息流模型,基于着色Petri网理论和CPNTools对身份认证消息流建模,采用Dolev-Yao攻击者模型和形式化分析方法对BACnet/IP进行安全性分析,发现协议漏洞并提出改进方案。BACnet/IP-SA协议使用设备的伪身份来保护真实身份信息,使用PUF响应进行认证,通过多信息集合的验证值来验证端身份的真实性并生成会话密钥。结合BAN逻辑和非形式化方法,对协议的安全性进行了证明。实验结果表明,所提方案能有效抵抗多类攻击和密钥泄露带来的安全威胁,在减少计算开销的同时增强了协议身份认证的安全性。

适用于铁路时间同步协议的双向身份认证方案

针对铁路时间同步协议客户端认证缺失、关键消息明文传输等问题,提出一种更安全的双向身份认证方案,用于时间节点之间的认证和密钥建立.方案采用非对称加密机制和ECDH(elliptic curve Diffie-Hellman)算法安全协商共享密钥,运用主机当前时间作为序列号抵抗重放攻击,由共享密钥和序列号产生的身份校验码完成双向身份认证.随后用共享密钥加密保护之后的关键消息,解决了关键消息明文传输的问题.该方案不仅解决了客户端认证缺失的问题,而且还具有前后向安全性.最后,采用BAN逻辑进行形式化验证,结果表明:该方法在安全性、认证开销方面较其他方法更优,能够满足铁路时间同步协议双向身份认证安全性和实时性的要求.

基于数理逻辑的安全协议本征逻辑分析方法

本文提出了一种基于数理逻辑的安全协议本征逻辑分析方法—SPALL方法.该方法在一阶谓词逻辑的基础上,增加了基于密码学的若干新语义,包括新的密码函数项、与密码学和安全协议分析相关的一阶谓词和二阶谓词等,并给出了十三类二十九条公理,仍使用谓词逻辑的分离规则和概括规则,形成新的安全协议分析系统,称为本征(latent)逻辑系统(也称本征逻辑或L逻辑).该系统是一阶谓词系统的扩充,以密码学和安全协议为“特定解释”,并定义了“概率真”的概念,力求每条公理在“特定解释”下是概率真的,而分离和概括规则又能保证从概率真演绎出概率真,从而使每条定理都概率真,以保证公理系统的可靠性.清晰的语义可以精确描述安全协议的前提与目标,基于公理和定理的协议分析,可简洁有效地推导出协议自身具有的安全特性.本文给出了详细的语义和公理,以及若干实用定理,然后对著名的密钥建立协议进行了详细分析,并对比了可证安全方法的分析结果,展示了本文方法的优势.此外还分析了电子选举协议和非否认协议,展示了本文方法有着广泛的适用范围.

轻量级的两方认证密钥协商协议

轻量级的两方认证密钥协商协议允许通信双方在公开信道上建立一个相同且安全的会话密钥。现有的认证协议难以满足轻量级的需求,同时多数轻量级协议仍存在某些安全问题。基于此,提出了一种基于身份的两方匿名轻量级逆向防火墙认证密钥协商协议。该协议在eCK模型下结合BAN逻辑被证明是安全的。协议提供匿名性、完美前向安全性、抗重放攻击、抗Dos攻击、抗中间人攻击。与其他轻量级认证协议对比发现,该协议具有更高的安全性和较短的运行时间,适用于资源受限设备。

基于混沌映射的无线网络环境三因子身份认证协议

针对无线网络环境当中的身份认证协议易受伪造攻击、重放攻击、用户模仿攻击、计算开销大、不能够提供匿名性等问题,提出一种基于三因子(口令、智能卡、生物特征)的身份认证密钥协商协议。通过BAN逻辑证明了通信实体之间的相互认证,利用AVISPA工具对该方案进行了仿真。安全性分析表明,该认证协议能够实现匿名性、相互认证、会话密钥协商并且能够抵御常见攻击。效率分析表明,该协议通信开销最少,效率更高。

一种基于多因素认证与密钥协商的数据密钥管理方案

隐私数据远程存储技术为用户存储数据带来便捷的同时,也增加了敏感数据在传输过程中遭受拦截攻击的风险。为了提高数据的安全性,需要对上传到远程设备的敏感数据进行加密。因此,高效可靠的密钥管理是确保数据安全的关键。多因素认证是保证数据安全传输的关键技术之一,在安全领域具有广泛的应用,如隐私数据保护、访问权限管理和在线支付等。鉴于此,提出了一种基于多因素认证的密钥存储策略来加强密钥管理:(1)通过确定的设备身份信息对密钥进行Shamir(2,3)分割;(2)对设备身份信息进行公钥加密,然后利用用户私有登录口令和生物特征来隐藏密钥的Shamir分割份额和公钥加密的私钥;(3)对获得的密钥相关信息进行一系列计算处理并分别存储到相应的设备中。理论分析表明,所提方案具有认证灵活,密钥管理高效、可靠以及通信安全等优势。此外,为了进一步说明方案的有效性,进行了BAN逻辑分析和启发式安全分析。分析结果表明,框架能够安全地协商会话密钥并抵抗多种已知攻击。

分布式电力移动终端隐私增强认证方案

针对智能电网移动终端实际环境下轻量化认证和多种密钥协商需求,提出一个基于区块链的轻量级多令牌双向匿名认证协议。方案通过区块链的分散存储机制实现系统身份认证的去中心化,提高了认证的灵活性。基于椭圆曲线生成随机假名,有效保护了用户身份隐私。生成移动终端会话密钥时融合了时敏令牌和多项式令牌机制,进一步提高了会话密钥安全性。采用BAN(Burrows-Abadi-Needham)逻辑证明了协议的正确性及非形式化证明了协议的安全性,并通过仿真实验评估了协议的性能。分析结果表明,该方案具有良好的安全性和实用性。

基于切比雪夫混沌映射和PUF的RFID三方认证协议

针对射频识别(RFID)三方认证协议存在的安全需求和资源开销的平衡问题,利用切比雪夫多项式的半群性质以及混沌性质提出了一个基于切比雪夫混沌映射和物理不可克隆函数(PUF)的RFID三方认证协议:使用切比雪夫混沌映射来实现标签、阅读器和服务器三方共享秘密;使用随机数实现协议每轮会话的新鲜性以抵抗重放攻击,同时也实现了阅读器与标签的匿名性;使用PUF函数实现标签本身的安全认证以及抵抗物理克隆攻击。安全分析表明,该协议能有效抵抗追踪、重放、物理克隆和去同步攻击等多种恶意攻击,使用BAN逻辑分析方法和Scyther工具验证了其安全性。与近期协议对比分析表明,该协议弥补了同类RFID协议的安全缺陷,在满足各种安全属性需求的同时尽量平衡硬件开销,契合了RFID硬件资源受限的处境,适用于RFID三方认证场景。

适用于天地一体化网络的无证书密钥协商协议

为了保证天地一体化网络中用户信息的传输安全,改进传统方案的高时延等问题,本文提出一种轻量级的无证书密钥协商方案。首先,本文分析无证书密钥协商协议系统模型,针对天地一体化网络的特点提出协议需要满足双向认证、抗重放、完整性等安全需求。其次,本文选择一种轻量级的无证书加密方案,在此基础上提出密钥协商协议,满足天地一体化网络的资源和安全要求。最终,本文对提出的密钥协商协议进行BAN(Burrow-Adadi-Needham)逻辑安全性分析,并结合软件对协议性能仿真进行比较,结果表明:该方案在满足网络安全性需求的同时实现高效快速的协商。

适用于智能电表双向互动系统的安全通信协议

根据智能电表双向互动系统逻辑结构和业务需求,提出了一种融合协议过滤、双向身份认证、访问列表查询和优先级控制等方法的智能电表双向互动、多重防护安全通信协议(BIMP),并采用BAN逻辑形式化分析方法和非形式化分析方法验证了其性能。BIMP在达到预期目标的同时具有安全保密性、抗攻击性、通信效率较高等特点,能够满足智能电表双向互动系统实际业务应用需求。

BAN逻辑的可靠性分析与改进

BAN逻辑的推理过程中可能引入错误的推理条件,导致不安全的协议被验证为安全的。为解决该问题,对消息的形式化描述方式进行改进,在消息含义推理规则中加上一个隐含但不能被忽略的条件,以增强验证的可靠性,通过对发送和推理的消息单元进行限定,使消息新鲜性判定规则适用于更多类型的协议安全性验证。

适用于用电信息采集的轻量级认证密钥协商协议

用电信息采集系统信息量巨大、覆盖面广,而传统的认证密钥协商协议计算量开销大、通信交互次数多,无法满足其高实时、低成本的现实需求。为了实现电力数据的安全高效传输,文中基于证书认证及新旧参数保护密钥动态协商机制,提出了一种轻量级认证密钥协商协议,结合BAN逻辑形式化分析和非形式化分析方法对协议进行分析,证明协议在达到一级信仰和二级信仰的同时具有双向实体认证、完美的向前保密性等安全属性。该协议能够抵抗多种攻击,在保证安全的情况下实时高效地完成身份认证及密钥协商,适用于用电信息采集系统对密钥应用的需求。

基于共享秘密的伪随机散列函数RFID双向认证协议

针对资源受限的RFID标签,结合伪随机数和共享秘密机制,该文提出一种基于散列函数的轻量级双向认证协议,实现了后端数据库、阅读器和标签之间的双向认证。详细分析了双向认证协议的抗攻击性能和效率性能,并基于BAN逻辑分析方法对协议模型进行了形式化证明。理论分析表明,该文提出的认证协议能够实现预期安全目标,抗攻击性能好,认证执行效率高且标签开销小,适用于大数量的RFID应用。

基于身份的TLS协议及其BAN逻辑分析

基于身份的密码体制(IBC)轻量、高效,密钥管理方式简单,但缺乏有效安全协议的支持限制了其应用。通过增加支持IBC的加密套件,引入IBC公钥代替RSA证书公钥,减少消息交换数量,提出支持IBC的、高效的基于身份的IB_TLS协议。使用BAN逻辑对其进行形式化分析,证明IB_TLS协议是安全的。

基于Hash函数的RFID安全认证协议的研究

为了改善RFID传感网络中阅读器与标签之间存在的安全隐私问题,通过分析现有安全协议,提出一种新的基于Hash函数的RFID安全认证协议。分析表明,该协议可以有效抵御非法读取、位置跟踪、窃听、伪装哄骗和重放等不安全问题,具有成本低、效率高、安全性高等特点。通过建立协议的理想化模型,利用BAN逻辑形式化分析该协议,在理论上证明其安全性。

密码协议分析工具——BAN逻辑及其缺陷

在介绍密码协议分析工具——ＢＡＮ逻辑的基础上，研究和分析了ＢＡＮ逻辑在初始假设、理想化步骤、语义和探测协议违规运行等方面所存在的缺陷，并用实际例子具体说明了这些缺陷，最后指出了ＢＡＮ逻辑改进的方向．

WAPI认证机制的性能和安全性分析

利用BAN类逻辑(WK逻辑),对中国无线局域网安全标准WAPI的认证基础设施WAI进行了形式化分析,指出其无法实现全部的认证及密钥协商目标.进一步分析表明,WAI中存在诸多安全问题,如无法提供身份保护、无法抵抗密钥一致性等攻击、缺乏私钥验证、不能提供如PFS、密钥控制等相应的安全属性等.因此,WAPI无法提供足够级别的安全保护.最后对WAPI与IEEE802 11i在安全性和性能上进行了比较.

基于智能卡的多服务器远程匿名认证密钥协商协议

针对Xu等近期提出的一个基于智能卡的动态身份用户远程认证方案(简称XJWM)进行分析,指出其不能抵抗冒充攻击和密钥泄露攻击,且不能实现前向安全和后向安全。利用Diffie-Hellman密钥协商算法及生物认证技术,提出一个新的多服务器环境下多因子远程匿名认证密钥协商协议。新方案不仅有效弥补了XJWM方案存在的安全缺陷,而且增加了智能卡对持卡者的口令与生物信息的认证,避免了智能卡丢失引起的冒充攻击。最后,用改进的BAN逻辑证明了新方案密钥协商的正确性、会话密钥机密性与新鲜性以及双向认证性。安全性和性能分析说明,新方案在少量增加计算量的情况下具有良好的安全性。

基于非对称密钥和Hash函数的RFID双向认证协议

随着RFID系统的广泛应用,系统安全问题日益突出.认证协议是一种面向应用层的协议,防止攻击者对敏感数据进行窃取,保证通信内容的完整性.由于无源RFID标签内存和容量的限制,使得目前通用的无线传感器网络中的安全协议在RFID系统不能直接使用.本文首先分析现有的基于密码学的认证协议和基于Hash函数的4种典型的RFID认证协议,包括Hash锁协议、随机化Hash锁协议、Hash链协议、基于Hash函数的ID变化协议的特点和缺陷,针对构架于物联网开放的EPC服务环境,提出了一种新的基于非对称密钥和Hash函数的双向认证协议,并给出了标签生成数字串和读写器生成数字串两种更新方案.该协议通过私钥对读写器的身份进行验证,使读写器与数据库相互独立;利用Hash函数对随机数字串进行运算来认证标签,保证了标签的前向安全性;运用BAN逻辑的形式化分析方法,对该协议的安全性进行了推导证明.通过对几种基于Hash函数认证协议的标签计算时间、读写器计算时间、数据库计算复杂度、标签存储容量4种性能对比分析表明,该协议实现复杂度低,更适合低成本、多用户系统使用.