排序方式: 共有10条查询结果,搜索用时 0 毫秒
1
1.
电子商务随着计算机技术和网络技术的发展快速发展,但是也存在着诸如合同时间认证等安全性问题使其推广受到阻碍.本文针对目前电子商务中数据处理中存在的不足,结合时态数据库的理论和方法,挖掘在电子商务中存在的时态信息,并提出一种利用时态数据库管理电子商务中数据的框架模型. 相似文献
2.
多重中断技术在计算机中有着非常重要的地位.本文在软硬件逻辑功能等价性原理的思想指导下,介绍了如何运用软件开发环境模拟中断系统并用可视化界面展示之,实现多重中断工作过程.该中断系统的实现表明,在计算机上用软件模拟硬件,应用于实验、教学和进一步的研究中是具有可行性的. 相似文献
3.
4.
基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议. 相似文献
5.
随着计算机技术和网络技术的发展,电子政务在我国开始全面实施。但是其中存在着诸如对信息时效性不能很好地处理等问题,这使其推广受到阻碍。通过分析目前电子政务中信息处理方法的不足,结合时态数据库的理论和方法,提出了一个解决电子政务中信息有效性的处理模型。 相似文献
6.
与证伪法(如模型检测)相比,采用证真法(如定理证明和逻辑推理)能验证协议在任意会话中的正确性,但分析难度较高,验证过程较为复杂。使用SVO逻辑方法,以Netbill微支付协议为例,对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集;在不影响Netbill协议安全性的前提下,为其建立了简化模型;针对协议特点,修正和补充了其验证目标;给出了比之前更合理的协议假设,展示了具体的推理过程,分析了验证结果。结果表明,Netbill协议基本满足认证性。最后对相关研究工作进行了比较。 相似文献
7.
提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显. 相似文献
8.
事务数据常见于各种应用场景中,如购物记录、页面浏览历史等.为了提供更好的服务,服务提供商收集用户数据并进行分析,但收集事务数据会泄露用户的隐私信息.为了解决上述问题,基于压缩的本地差分隐私模型,提出一种事务数据收集方法.首先,定义了一种新的候选项集分值函数;其次,基于该函数,将候选项集的样本空间划分为多个子空间;然后,随机选择其中一个子空间,基于该子空间随机生成事务数据并发送给不可信的数据收集者;最后,考虑到隐私参数的设置问题,基于最大后验置信度攻击模型设计启发式隐私参数设置策略.理论分析表明,该方法能够同时保护事务数据的长度与内容,满足压缩的本地差分隐私要求.实验结果表明,与目前最优的工作相比,所收集的数据具有更高的效用性,隐私参数设置更具有语义性. 相似文献
9.
10.
有界模型检测的优化 总被引:1,自引:1,他引:1
G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值. 相似文献
1