期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
针对A(0)协议的新鲜性攻击及改进方案 被引量:2
1
作者 唐郑熠 李均涛 李祥 《计算机技术与发展》 2009年第10期164-166,共3页
非形式化方法很难保证认证协议的安全性,因此对于形式化方法的研究与应用具有重要的意义,模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A(0)协议进行建模检测的方法,并从检测结果中发现了A(0)协议无法保... 非形式化方法很难保证认证协议的安全性,因此对于形式化方法的研究与应用具有重要的意义,模型检测技术就是其中的一种。该文介绍了使用模型检测工具SPIN和Promela语言对A(0)协议进行建模检测的方法,并从检测结果中发现了A(0)协议无法保证公开协商密钥证书新鲜性的缺陷。据此设计出了针对A(0)协议的新鲜性攻击方法,并提出了弥补其新鲜性缺陷的改进方案。由此可见,使用模型检测技术可以高效便捷地对认证协议进行分析。 展开更多
关键词 a(0) 新鲜性 协议攻击 模型检测 SPIN PROMELa
下载PDF
Dolev-Yao攻击者模型的形式化描述 被引量:8
2
作者 唐郑熠 李祥 《计算机工程与科学》 CSCD 北大核心 2010年第8期36-38,45,共4页
模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形... 模型检测技术能够实现安全协议的自动化分析,是一种高效的形式化分析方法。然而,对于攻击者的建模却一直缺乏通用的方法,这导致了模型检测方法的自动化程度降低。本文为安全协议分析中,应用最为广泛的Dolev-Yao攻击者模型建立了一套形式化描述方法。遵循这一方法,可以使用任何建模语言机械地建立Dolev-Yao攻击者模型,从而大大地减少了人工分析的成份。同时,本文还使用该方法验证了两个目的完全不同的协议,证明了它的通用性。 展开更多
关键词 Dolev-Yao攻击者模型 形式化描述 模型检测 SPIN NSPK a(0)
下载PDF
IMPLICIT-EXPLICIT MULTISTEP FINITE ELEMENT-MIXED FINITE ELEMENT METHODS FOR THE TRANSIENT BEHAVIOR OF A SEMICONDUCTOR DEVICE
3
作者 陈蔚 《Acta Mathematica Scientia》 SCIE CSCD 2003年第3期386-398,共13页
The transient behavior of a semiconductor device consists of a Poisson equation for the electric potential and of two nonlinear parabolic equations for the electron density and hole density. The electric potential equ... The transient behavior of a semiconductor device consists of a Poisson equation for the electric potential and of two nonlinear parabolic equations for the electron density and hole density. The electric potential equation is discretized by a mixed finite element method. The electron and hole density equations are treated by implicit-explicit multistep finite element methods. The schemes are very efficient. The optimal order error estimates both in time and space are derived. 展开更多
关键词 Semiconductor device strongly a(0)-stable multistep methods finite element methods mixed finite element methods
下载PDF
一类反应扩散方程组的隐-显多步有限元方法及其分析 被引量:6
4
作者 陈蔚 《数学物理学报(A辑)》 CSCD 北大核心 2002年第2期180-188,共9页
考虑一类非线性反应扩散方程组 ,提出了隐 -显多步有限元格式逼近 ,证明了格式最优的
关键词 反应扩散方程组 a(0)-稳定 多步法 有限元法
下载PDF
星载全球大气波动成像仪研究 被引量:5
5
作者 钱浩俊 胡雄 涂翠 《空间科学学报》 CAS CSCD 北大核心 2012年第3期362-367,共6页
在卫星上对中间层顶区域的气辉辐射成像观测,对于全球大气波动的监测和研究具有重要的意义.利用TDICCD对O_2A(0-0)气辉进行成像观测,计算了曝光积分时间、信噪比和能达到的最高空间分辨率,分析了地球自转对空间分辨率的影响,在此基础上... 在卫星上对中间层顶区域的气辉辐射成像观测,对于全球大气波动的监测和研究具有重要的意义.利用TDICCD对O_2A(0-0)气辉进行成像观测,计算了曝光积分时间、信噪比和能达到的最高空间分辨率,分析了地球自转对空间分辨率的影响,在此基础上提出一种星载全球大气波动成像仪方案,该方案可以观测垂直波长大于10 km的大气波动,最高水平分辨率可以达到0.33 km. 展开更多
关键词 O2a(0-0)气辉 全球大气波动成像仪 中间层顶区域 大气重力波
下载PDF
半导体设备热传输中的隐式-显式多步有限元法(英文) 被引量:2
6
作者 陈蔚 《数学研究》 CSCD 2002年第2期109-123,共15页
考虑热引导半导体设备中的传输行为 .用一个有限元法离散电子位势所满足的 Poisson方程 ;用隐式 -显式多步有限元法处理电子密度和空洞密度满足的两个对流 -扩散方程 ;热传导方程用隐式多步有限元法离散 .推导了优化的 L2 范误差估计 .
关键词 半导体设备 热传输 a(0)稳定 多步法 有限元法
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部