基于PCL的改进型Helsinki协议的形式化分析

针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于"Cords演算"的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.     

采用模型检测器的软件安全模型验证方法

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.     

一种理性安全协议形式化分析方法及应用

博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证.不过在理性环境下,由于参与者对知识的自利性,ATL和ATEL都不适合形式化分析与验证理性安全协议.于是在并行认知博弈结构CEGS中引入效用函数和偏好关系,得到新的并行认知博弈结构rCEGS,并在合作模态算子《Γ》中引入行为ACT参数,提出新的交替时序认知逻辑rA-TEL-A,并基于不动点描述rATEL-A时序算子.然后基于rATEL-A,提出适合于形式化分析理性安全协议的推理系统,并对具体的理性安全协议的公平性、安全性等性质进行形式化分析.     

基于BAN逻辑的SADSR协议安全性分析

移动Ad hoc网络路由协议为加强其安全性,采用了密码技术,使其成为安全协议的一种.这使得采用形式化的方法分析其安全性成为可能.本文根据移动Ad Hoc网络路由协议的特点,采用BAN逻辑对协议的安全性进行描述,指出了协议应满足的条件.并对协议的运行过程进行了形式化,给出具体的分析方法.采用该方法对安全路由协议SADSR进行了安全验证,说明方法的有效性.     

Aziz-Diffie协议的形式化分析及其改进

形式化分析方法由于其精炼、简洁和无二义性逐步成为分析密码协议安全性的一条可靠而准确的途径。作为形式化分析方法的典型代表BAN逻辑由于其直观、易用等优点得到广泛的应用。概述了BAN逻辑,并基于BAN逻辑对Aziz-Diffie无线网络密钥协议进行了形式化描述和分析,验证了协议存在的漏洞,同时提出了该协议的改进方案。     

一种改进的属性远程证明方案

为了克服现有基于属性证书的远程证明方案在隐私保护和安全性方面的不足,文中提出了一种基于隐藏证书技术的属性远程证明方案（HCP-RA）,该方案在传统基于属性的远程证明的基础上引入了隐藏证书技术,实现了对机密性证书和策略的保护,同时实现了验证方和被验证方之间的双向可信性验证功能。文中首先给出了HCP-RA模型,随后针对该模型给出了形式化描述和相应的远程证明协议,并通过应用实例来说明该协议的具体工作过程。与传统的基于属性证书的远程证明技术相比较,该方案在隐私保护方面具有很大优势;双向可信性验证提高了传统单向属性远程证明的安全性。     

一种安全DSR协议的形式化分析方法

目前安全 DSR协议由于缺乏有效的形式化分析方法,难以发现一些隐蔽的安全漏洞.针对这一问题,通过分析DSR协议路由过程,给出了安全DSR协议的安全目标.提出了一种基于逻辑的安全DSR协议形式化分析方法,定义了能够反映安全DSR协议特性的基本逻辑构件(包括主体、目标和公式)和推理规则.首先用逻辑公式描述协议初始假设及过程,然后用推理规则进行推导产生推导结果,最后依据推导结果判断协议安全性.使用这种方法对SADSR协议进行了形式化分析与改进,发现了SADSR协议存在的安全漏洞.分析结果表明,提出的方法能够用于安全DSR协议形式化分析,能够发现一些较为隐蔽的安全缺陷.     

数据起源请求协议的安全性分析与验证

数据起源记录的信息有可能揭露用户的隐私,因此对起源的安全保护特别重要。介绍了数据起源和可审计起源系统,从机密性和认证性两个方面对基于起源的审计结构中的数据请求协议进行了分析,改进了协议在起源记录过程中消息传输方式。介绍了BA N逻辑方法,应用BA N逻辑对协议进行了形式化的分析与验证,证明协议满足机密性和认证性要求。     

基于符号模型自动分析隐私保留的用户认证协议安全性

利用大数据特征,PPMUAS协议声称实现了移动用户的隐私保护和认证,但并没有给出严格证明.故本文首先应用Applied PI演算对PPMUAS协议进行形式化描述,然后分别使用非单射一致性和Query对认证性和秘密性进行建模,最后把PPMUAS协议的Applied PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析与证明.结果表明PPMUAS协议具有秘密性,但缺少认证性,并给出了解决方法.     

基于模型检测的SSL协议形式化验证

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.     

网络时代合同法的最新发展

目前，联合国贸法会电子商务工作组的核心工作是在合同法领域起草一个有关电子订约的公约。电子合同的规则集中反映了网络时代合同法的最新发展。在信息技术的推动下，网络时代的合同法发生了巨大的演变，电子合同产生了许多不同于传统合同的法律规则，其中典型的电子合同法律规则有：电子形式规则、电子意思表示规则、电子签名与认证规则以及计算机信息交易合同中的电子错误规则和电子自助规则等。     

一种改进的离线电子现金方案

在分析Brands的受限盲签名方案的基础上提出了一个改进的电子现金支付新方案，基于此构建了一个不带“观察器”的简约高效电子现金方案，详细描述了离线电子现金支付方案作提取、支付和存储三个协议．分析了新方案的效率和安全性，与Brands的电子现金协议相比，在不降低安全他的前提下提高了处理效率、增加了灵活性，尤其适用于因持网上的小额支付．     

关于电子技术基础实验教学的探讨

为了更好地提高学生的实践与创新能力,苏州大学电子信息学院积极响应教育部提出的"卓越工程师教育培养计划",进行了一系列的实验教学改革,其中包括电子技术基础实验模块、模数电综合实验模块、系统设计模块等。作为实验教学改革的第一模块,本院在第3学期新增开设了电子技术基础实验课程,让学生提前走进电子实验室,在系统了解常用电子元器件和常用实验仪器的使用基础上,完成一系列的验证型实验与设计型实验。本基础实验模块锻炼了学生的焊接能力、简单的电路调试能力,并激发了学生的电子设计与动手热情,为后续的理论课程与实验模块奠定坚实的基础。     

电子教室软件在电子阅览室管理中的应用

分析了电子阅览室的功能与管理工作,介绍了电子教室的软件功能和基本使用,找到两者的契合点,探讨了电子教室软件在电子阅览室管理中的具体应用,以提高电子阅览室的管理效益及服务水平。     

浅谈电子档案的有效管理

介绍了电子档案的概念,比较了电子档案与纸质档案的特点,分析了电子档案的管理现状,提出了加强电子档案管理的有效措施。     

现代汽车电子技术应用状况

电子技术现已应用于各行各业。文章着重探讨了电子技术在现代汽车中的应用以及汽车电子产品巨大的市场潜力，并预测了其广阔的市场前景。     

An Efficient Fair Electronic Cash System

In this paper, an efficient fair e-cash system is presented. Based on the improved Brands‘ ecash scheme, it is expanded by adding two roles, government and judges. The user can keep unconditionally anonymous in normal transactions. Authorized by the judges, the government can remove the identity of an illegal user with the help of the bank. So such misuse as blackmailing or money laundering can be prevented. Therefore, this scheme is more efficient, more suitable for adopting pre-processing and post-processing and more practical. In the paper, the details of the scheme are described, its sccuritv is oroved, and its efficiency is analyzed.     

对电子文件归档问题的探讨

介绍了电子文件的含义及与纸质文件不同的特点,分析了电子文件归档的难点,提出了实现电子文件归档的途径。     

浅论信息时代电子文件的管理

从档案管理的角度出发,分析了电子文件产生的条件、途径、现状及制约因素,初步探讨了电子文件的有效管理模式,认为电子文件与纸制文件共存互动是现阶段档案管理的必由之路,档案管理人员应有效利用两种文件的特点.实现全面、科学的文件管理战略.     

织机电子送经和卷取控制系统的研制

研制了一种用步进电机驱动的同步电子送经和卷取控制系统。该控制系统在织造时使经纱保持张力稳定，并通过强大的控制程序来消除停车稀密路，该控制系统不但可以实现均匀卷取，还能织造变纬密织物，可用于特殊织物的开发。