基于计算模型的OpenID Connect协议认证性的自动化分析

分析了OpenID Connect协议的消息结构,基于计算模型应用Blanchet演算对OpenID Connect协议进行了形式化建模,应用自动化验证工具Crypto Verif验证了其认证性.结果表明:在OpenID Connect协议中,客户端能够认证终端用户,但是终端用户与授权服务器之间不能相互认证、令牌终端不能认证客户端.为此,给出了OpenID Connect协议中不具有认证性问题的解决方法.

改进的OpenID Connect协议及其安全性分析

Open ID Connect协议是最新的单点登录协议之一,已经广泛应用于用户身份认证领域,其安全性受到了人们的重点关注。为增强Open ID Connect协议的安全性,首先引入数字签名及非对称加密技术,对其进行改进,重点关注改进后协议的秘密性和认证性;其次基于符号模型,应用应用PI演算对改进的Open ID Connect协议进行形式化建模;然后为验证改进后协议的认证性和秘密性,分别使用非单射性和query对认证性和秘密性进行建模;最后把改进的Open ID Connect协议的应用PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析。实验结果表明,改进后的Open ID Connect协议具有认证性和秘密性。

基于计算模型的安全协议Swift语言实施安全性分析

分析IOS平台上的安全协议Swift语言实施安全性,对保障IOS应用安全具有重要意义。首先对已有安全协议Swift语言实施进行分析,确定Swift语言子集SubSwift,并给出其BNF;其次基于操作语义,建立SubSwift语言到Blanchet演算的映射模型,主要包含SubSwift语言的语句、类型到Blanchet演算的语句及类型的映射关系与规则;再次根据Sub Swift语言到Blanchet演算的映射模型,提出从安全协议Sub Swift语言实施生成安全协议Blanchet演算实施方法;最后应用Antrl4工具和Java语言开发安全协议Blanchet演算实施生成工具SubSwift2CV,分析OpenID Connect协议、Oauth2.0协议和TLS协议的SubSwift语言实施安全性。

云数据安全研究进展

云数据安全问题是制约云计算发展的重要因素之一。该文综述了云数据安全方面的研究进展,将云数据安全所涉及的云身份认证、云访问控制、云数据安全计算、虚拟化安全技术、云数据存储安全、云数据安全删除、云信息流控制、云数据安全审计、云数据隐私保护及云业务可持续性保障10方面相关研究工作纳入到物理资源层、虚拟组件层及云服务层所构成的云架构中进行总结和分析;并给出了相关技术的未来发展趋势。

基于LM3S-811单相逆变器设计

在此实现了基于LM3S-811的高频逆变器,整个系统包括辅助电源、推挽升压、全桥逆变、SPWM产生、过流保护以及低通滤波等模块。DC 12 V低压直流经过挽推升压转换为高频方波,再经过变压器升压和整流、滤波转化为DC 300 V。推挽模块用SG3525驱动MOSFET得到高压直流电,再经过LM3S-811产生SPWM波驱动全桥逆模块并结合低通滤波、输出过流保护得到工频AC 220 V,输出功率可达240 W。该系统具有体积小、输出稳定等优点。

安全协议实施安全性分析综述

安全协议是网络空间安全的重要组成部分,安全协议实施是安全协议的最终表现形式。介绍了安全协议实施安全性分析的意义,分别按照三个前提条件:能够获取安全协议客户端实施和安全协议服务器端实施、仅能够获取安全协议客户端实施、不能获取安全协议客户端与安全协议服务器端实施,并依据安全协议实施安全性分析采用的主要分析方法——程序验证、模型抽取、网络轨迹、指令分析等,对相关研究成果进行归类、分析、比较、总结和讨论。对未来安全协议实施安全性分析的研究方向进行了展望。