论文部分内容阅读
介绍了安全协议形式化分析方法串空间模型的基本概念,给出了检查消息机密性的定理的变形公式,形式化地证明了由未泄漏私钥签字的消息起源于诚实主体串,并利用上述结论检验了BAN修改后的CCITTX.509(3)协议的机密性和认证性。
串空间模型的原理与应用
【摘 要】
：
介绍了安全协议形式化分析方法串空间模型的基本概念,给出了检查消息机密性的定理的变形公式,形式化地证明了由未泄漏私钥签字的消息起源于诚实主体串,并利用上述结论检验了BAN修改后的CCITTX.509(3)协议的机密性和认证性。
【机 构】
：
卫士通信息产业股份有限公司,现代通信国家重点实验室,电子科技大学,卫士通信息产业股份有限公司
【出 处】
：
计算机应用
【发表日期】
：
2005年08期
【基金项目】
：
国家重点实验室基金，国家重点基础研究发展计划(973计划)
其他文献
对n类不同的独立任务在m个不同机器上加工的多任务平行非同类机的加工调度问题进行了探讨,提出了一种基于指派与调度的复合策略的算法,最后用实例进行了排序。通过与文献中的实例比较,证明该方法具有一定的优越性。
XML函数依赖问题是进行XML数据库后续研究的基础。首先基于M.Arenas等人给定的XML中DTD和XML树的定义,提出空值、不完全树元组、数据值偏序、最小扩展树等概念,在此基础上,给出弱函数依赖及其满足性的定义;其次研究了XML弱函数依赖的逻辑蕴含问题,提出一组适合XML空值模型的函数依赖推理规则集;最后给出推理规则集的正确性和完备性证明。
一直以来，诸多研究者对拖延的概念界定各不相同，大都根据自己的理解，对拖延做了种种界定。到目前为止，国内外研究者对拖延还没有形成统一的认识，也没有统一的标准，但下面几种对拖延的解释，已被广大研究者普遍接受。 有人认为拖延指不能在预定的时间内开始或完成任务的行为；也有人认为拖延是不必要地推迟任务以至于产生主观不适的行为。上述研究者都是从开始或者结束的时间上来界定拖延行为。还有人认为拖延是个体延迟或完
国务院《关于大力发展职业教育的决定》明确提出要＂大力推行工学结合、校企合作的培养模式＂。在多年的办学实践中,我们认识到加强校企合作、坚持工学结合是中职学校推进教学改
现有的流媒体系统一般是基于客户/服务器模式和IP组播技术,这限制了用户数量且IP组播需先得到ISP支持,故其发展受到很大限制。而在P2P网络中,每个接收数据的用户同时向外转发数据,这就充分利用了以往忽视的客户机资源。首先指出了P2P流媒体应用中所面临的挑战,并着重从应用层多播树、网络异构性、激励机制等方面阐述了P2P流媒体的研究现状,分析讨论了存在的问题,最后指出进一步的研究方向。