期刊导航
期刊开放获取
cqvip
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
4
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式：
文摘
详细
列表
相关度排序
被引量排序
时效性排序
基于自编码器的未知协议分类方法
被引量：
5
1
作者
顾纯祥
吴伟森
+1 位作者
石雅男
李光松
《通信学报》
EI
CSCD
北大核心
2020年第6期88-97,共10页
针对互联网中存在的大量未知协议导致网络管理和维护网络安全十分困难的问题,提出了一种未知协议的分类识别方法。结合自编码器技术和改进的K-means聚类技术针对网络流量实现了未知协议的分类识别。利用自编码器对网络流量进行降维和特...
针对互联网中存在的大量未知协议导致网络管理和维护网络安全十分困难的问题,提出了一种未知协议的分类识别方法。结合自编码器技术和改进的K-means聚类技术针对网络流量实现了未知协议的分类识别。利用自编码器对网络流量进行降维和特征提取,使用聚类技术对降维后数据进行无监督的分类,最终实现对网络流量的无监督识别分类。实验结果表明,所提方法分类效果优于传统的K-means、DBSCAN、GMM算法,且具有更高的效率。
展开更多
关键词
未知协议分类
自编码器
无监督分类
特征提取
下载PDF
职称材料
基于观察等价性的协议猜测攻击形式化检测方法
2
作者
苗旭阳
顾纯祥
陆思奇
《密码学报》
CSCD
2023年第2期306-319,共14页
由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化...
由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.
展开更多
关键词
形式化分析
观察等价性
口令猜测攻击
Tamarin-Prover
下载PDF
职称材料
C2P:基于Pi演算的协议C代码形式化抽象方法和工具
被引量：
3
3
作者
张协力
祝跃飞
+1 位作者
顾纯祥
陈熹
《软件学报》
EI
CSCD
北大核心
2021年第6期1581-1596,共16页
形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基...
形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.
展开更多
关键词
协议实现
形式化验证
PI演算
模型抽取
ProVerif
下载PDF
职称材料
模型学习与符号执行结合的安全协议代码分析技术
被引量：
2
4
作者
张协力
祝跃飞
+1 位作者
顾纯祥
陈熹
《网络与信息安全学报》
2021年第5期93-104,共12页
符号执行技术从理论上可以全面分析程序执行空间,但对安全协议这样的大型程序,路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点,提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路;...
符号执行技术从理论上可以全面分析程序执行空间,但对安全协议这样的大型程序,路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点,提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路;同时,通过将协议代码中的密码学逻辑与协议交互逻辑相分离,避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在SSH协议开源项目Dropbear上的成功实践表明了所提方法的可行性;通过与Dropbear自带的模糊测试套件对比,验证了所提方法在代码覆盖率与错误点发现上均具有一定优势。
展开更多
关键词
模型学习
符号执行
安全协议代码
状态驱动
下载PDF
职称材料
题名
基于自编码器的未知协议分类方法
被引量：
5
1
作者
顾纯祥
吴伟森
石雅男
李光松
机构
信息工程大学
网络
空间安全学院
网络
密码
技术
河南省
重点
实验室
出处
《通信学报》
EI
CSCD
北大核心
2020年第6期88-97,共10页
基金
国家自然科学基金资助项目(No.61772548)
国家自然科学基金创新研究群体资助项目(No.61521003)
信息保障技术重点实验室开放基金资助项目(No.KJ-17-001)。
文摘
针对互联网中存在的大量未知协议导致网络管理和维护网络安全十分困难的问题,提出了一种未知协议的分类识别方法。结合自编码器技术和改进的K-means聚类技术针对网络流量实现了未知协议的分类识别。利用自编码器对网络流量进行降维和特征提取,使用聚类技术对降维后数据进行无监督的分类,最终实现对网络流量的无监督识别分类。实验结果表明,所提方法分类效果优于传统的K-means、DBSCAN、GMM算法,且具有更高的效率。
关键词
未知协议分类
自编码器
无监督分类
特征提取
Keywords
unknown protocol classification
autoencoder
unsupervised classification
feature extraction
分类号
TP181 [自动化与计算机技术—控制理论与控制工程]
下载PDF
职称材料
题名
基于观察等价性的协议猜测攻击形式化检测方法
2
作者
苗旭阳
顾纯祥
陆思奇
机构
数学工程与先进计算国家
重点
实验室
网络
密码
技术
河南省
重点
实验室
出处
《密码学报》
CSCD
2023年第2期306-319,共14页
文摘
由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.
关键词
形式化分析
观察等价性
口令猜测攻击
Tamarin-Prover
Keywords
formal analysis
observational equivalence
password guessing attack
Tamarin-Prover
分类号
TP309.7 [自动化与计算机技术—计算机系统结构]
下载PDF
职称材料
题名
C2P:基于Pi演算的协议C代码形式化抽象方法和工具
被引量：
3
3
作者
张协力
祝跃飞
顾纯祥
陈熹
机构
数学工程与先进计算国家
重点
实验室
网络
密码
技术
河南省
重点
实验室
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1581-1596,共16页
基金
国家重点研发计划(2019QY1302)。
文摘
形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时,可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.
关键词
协议实现
形式化验证
PI演算
模型抽取
ProVerif
Keywords
protocol implementation
formal verification
Pi calculus
model extraction
ProVerif
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
模型学习与符号执行结合的安全协议代码分析技术
被引量：
2
4
作者
张协力
祝跃飞
顾纯祥
陈熹
机构
数学工程与先进计算国家
重点
实验室
网络
密码
技术
河南省
重点
实验室
出处
《网络与信息安全学报》
2021年第5期93-104,共12页
基金
国家重点研发计划(2019QY1302)。
文摘
符号执行技术从理论上可以全面分析程序执行空间,但对安全协议这样的大型程序,路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点,提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路;同时,通过将协议代码中的密码学逻辑与协议交互逻辑相分离,避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在SSH协议开源项目Dropbear上的成功实践表明了所提方法的可行性;通过与Dropbear自带的模糊测试套件对比,验证了所提方法在代码覆盖率与错误点发现上均具有一定优势。
关键词
模型学习
符号执行
安全协议代码
状态驱动
Keywords
model learning
symbolic execution
security protocol code
state-driver
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
基于自编码器的未知协议分类方法
顾纯祥
吴伟森
石雅男
李光松
《通信学报》
EI
CSCD
北大核心
2020
5
下载PDF
职称材料
2
基于观察等价性的协议猜测攻击形式化检测方法
苗旭阳
顾纯祥
陆思奇
《密码学报》
CSCD
2023
0
下载PDF
职称材料
3
C2P:基于Pi演算的协议C代码形式化抽象方法和工具
张协力
祝跃飞
顾纯祥
陈熹
《软件学报》
EI
CSCD
北大核心
2021
3
下载PDF
职称材料
4
模型学习与符号执行结合的安全协议代码分析技术
张协力
祝跃飞
顾纯祥
陈熹
《网络与信息安全学报》
2021
2
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部
