摘要：在J2ME(Java 2 Mobile Edition)开发环境-J2ME Wireless Toolkit中,研究了Robert Esser[1]的Petri网开发软件包,在手机(或其他手持移动设备)上实现Petri网的可视化设计的原理,实现了著名的AB(交替比特)通信协议[6],并对该软件包的若干功能进行了改进.

摘要：可验证加密签名方案常用于构建公平交换协议,公平交换协议中的可信第三方往往会成为瓶颈。该文将Boneh等提出的单仲裁者可验证加密签名方案扩展为具有多个仲裁者的方案,方案应用无可信中心的可验证秘密共享技术实现了仲裁权力的分散。基于所构建的方案设计了一个公平合同签署协议,协议的可信第三方由多个仲裁者来构成,降低了第三方与其中一方合谋欺骗的风险。除此之外,协议具有不可伪造性、非透明性、公平性和机密性。由于该方案的设计是基于短签名方案和聚集签名方案,因此具有更高的通信效率。

摘要：特殊安全多方计算问题是近几年国际密码学界一个研究热点。保密计算几何问题就是其中之一,它是指两个或多个互不信任的参与方希望利用他们私有的几何信息作为输入协作解决某一计算几何问题,同时他们想要确保没有把自己的任何私有输入信息泄露给其他参与方,除了规定的输出。设计了基于阈值的两点之间、点线之间距离关系的保密判定协议,点与两平行直线位置关系的保密判定协议,使用这几个协议构造了基于阈值的点与线段之间距离关系的保密判定协议。这些协议在工程、商业和军事等领域中有着潜在的应用前景。

摘要：分析了Boneh等人的短签名方案和Boldyreva门限签名方案因不具备概率签名特性而可能存在的一种对比攻击;然后基于Gap Diffie-Hellman(GDH)群设计了一个概率型的门限签名方案,并在随机预言模型(Random Oracle Model)下证明了方案的安全性。所提出的方案可以避免时比攻击的风险,并且其安全性不低于Boldyreva方案的安全性,即提供了健壮性和在选择消息攻击下的不可伪造性,并能容忍t<n/2个恶意用户的勾结。本文的方案可作为Boldyreva方案的改进。

摘要：计算机及网络技术使远程办公成为可能,但其存在安全隐患.讨论如何实现远程办公的安全性,给出了远程办公用户实时监控的实现(包括远程用户键盘使用及远程计算机进程的实时监控),并通过CryptoAPI实现了对信息加密传送.

摘要：语音应用(VAP)技术是基于语音进行处理的技术,微软近来发布的Speech SDK5.0是基于COM的全程语音开发工具;多播通信是一种重要的网络通信技术;本文讨论与多播通信相关的TCP/IP协议,研究了全程中文语音技术在多播通信中的应用,设计并实现了一个中文语音多播通信实例,本实例可用于多播语音聊天、多播会议等领域。

摘要：为了能够有效的描述现实世界中的相对静止状态,分析了在哲学逻辑理论中的线序时态逻辑定理系统中引入自反性质的可行性,在此基础上建立了具有自反性质的线序时态逻辑系统TA。叙述了TA时态系统的主要定理以及该系统具有无端稠密线序性质,并表明了该系统的紧致性、可靠性和完全性。运用状态重命名方法说明了TA系统与行为时序逻辑TLA系统之间的联系,从而将TA的定理系统运用到行为时序逻辑的研究中。

摘要：行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向。为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统。在此基础上严格的证明了TLA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件。最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型。

摘要：由于参与方较多,多方公平交换协议的执行效率是协议设计的关键因素。利用椭圆曲线上的双线性对构造基于身份的可验证加密签名方案,基于这种签名方案构建了一种新的多方公平交换协议。该协议具有较高的执行效率、签名长度短等优点,而且满足有效性、公平性、时限性、优化性等特性。

摘要：安全协议是确保网络安全的关键,在现有的技术条件下,已经有许多方法来分析协议的安全性,但是对攻击者建模的方法不够高效,导致协议的检测和分析效率较低。形式化方法是检验协议安全性的一种手段,它能高效地分析验证协议设计中存在的漏洞。模型检测作为形式化方法的一种,具有简洁、高效和自动化程度高的特性,模型检测器SPIN具有强大的检测能力。文章使用SPIN对安全协议进行研究,提出了一种更有效的方法来验证攻击者模型的安全协议,首先对攻击者行为进行分析,获取攻击者初始知识库,根据分解规则和合成规则不断地更新攻击者知识库;其次形式化分析各诚实主体,并建立各诚实主体和攻击者的Promela语义模型;最后使用模型检测器SPIN进行验证。实验结果表明,文章提出的方法能使模型复杂度降低,大幅度减少模型的状态数量,有效地避免状态空间爆炸,提升验证效率。