云南高校图书馆联盟文献共享服务平台- TAMARIN

TAMARIN: 作品数：14被引量：31H指数：4; 导出分析报告; 相关领域：自动化与计算机技术更多>>; 相关作者：熊焰黄文超缪祥华刘彩霞赵宇更多>>; 相关机构：中国科学技术大学昆明理工大学武汉大学国家数字交换系统工程技术研究中心更多>>; 相关期刊：《Open Journal of Medical Microbiology》《清华大学学报（自然科学版）》《World Journal of Gastroenterology》《武汉大学学报（理学版）》更多>>; 相关基金：国家自然科学基金国防基础科研计划安徽省自然科学基金更多>>

基于Lowe分类的EAP-AKA′协议安全性分析与改进: 《数据通信》2025年第1期24-28,32,共6页黄明巍缪祥华张世奇张世杰王欣源; EAP-AKA′协议是5G网络中重要的认证协议之一,但在其协议中存在一些潜在的安全风险。针对EAP-AKA′协议在5G网络中的安全性问题,基于Lowe分类法对协议的安全性进行了分析,并提出了一系列改进措施,包括使用由Fiat-Shamir启发式优化的挑战...; 关键词：5G网络安全 EPA-AKA′协议 Lowe分类 Tamarin分析器 Dolve-Yao敌手模型 Fiat-Shamir启发式形式化方法

基于Tamarin的门罗币支付协议分析方法: 《信息网络安全》2024年第5期756-766,共11页李雨昕黄文超王炯涵熊焰; 国家自然科学基金[62372422,61972369,62102385];安徽省自然科学基金[2108085QF262];中央高校基本科研业务费专项资金[WK2150110024]。; 门罗币作为一款基于区块链技术的高度匿名加密货币协议,旨在为用户提供强大的隐私保护功能。与其他加密货币不同,门罗币通过独特的支付协议对用户的交易隐私加强保护。然而,支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析...; 关键词：门罗币 TAMARIN 支付协议符号模型

一种具有前向安全的TLS协议0-RTT握手方案被引量：1: 《化工自动化及仪表》2023年第6期813-819,832,共8页蒲鹳雄缪祥华袁梅宇; 云南省计算机技术应用重点实验室开放基金(批准号:2021207)资助的课题。; 针对传输层安全(TLS)协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT握手方案,传输的早期数据由于不存在身份认证,容易遭受重放、伪造以及中间人的攻击,并且不满足前向安全的问题,提出一种具有前向安全的0-RTT优化握手方案,...; 关键词：传输层安全(TLS) 完美前向安全(PFS) 0-RTT优化握手方案安全协议形式化分析 TAMARIN

基于Tamarin的MQTT协议安全性分析方法被引量：4: 《计算机应用研究》2023年第10期3132-3137,3143,共7页郑红兵王焕伟赵琪董姝岐井靖; 国家重点研发项目(2019QY502)。; MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一...; 关键词：MQTT协议保密属性认证属性形式化分析 TAMARIN

基于Tamarin Prover的5G EAP-TLS协议的形式化分析: 《武汉大学学报（理学版）》2023年第5期653-664,共12页马壮壮杜瑞颖陈晶何琨; 国家重点研发计划(2021YFB2700200);国家自然科学基金(61772383,U1836202,62076187,62172303)。; 为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对...; 关键词：5G专用网络 EAP-TLS协议形式化分析 Tamarin Prover 自动化验证

基于安全协议代码的形式化辅助建模研究被引量：2: 《计算机应用研究》2023年第4期1189-1193,1202,共6页葛艺黄文超熊焰; 国家自然科学基金面上项目(61972369);国家自然科学基金青年项目(62102385);安徽省自然科学基金资助项目(2108085QF262)。; 随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方...; 关键词：形式化验证形式化建模协议代码污点分析 TAMARIN

OTFS-Based Efficient Handover Authentication Scheme with Privacy-Preserving for High Mobility Scenarios: 《China Communications》2023年第1期36-49,共14页Dawei Li Di Liu Yu Sun Jianwei Liu; supported by Natural Science Foundation of China(No.62002006,U2241213,U21B2021,62172025,61932011,61932014,61972018,61972019,61772538,32071775,91646203);Defense Industrial Technology Development Program(No.JCKY2021211B017)。; Handover authentication in high mobility scenarios is characterized by frequent and shortterm parallel execution.Moreover,the penetration loss and Doppler frequency shift caused by high speed also lead to the deterior...; 关键词：high mobility condition handover authentication PRIVACY-PRESERVING TAMARIN OTFS

基于Tamarin的5G AKA协议形式化分析及其改进方法被引量：4: 《密码学报》2022年第2期237-247,共11页刘镝王梓屹李大伟关振宇孙钰刘建伟; 国家重点研发计划(2021YFB2700200);国家自然科学基金(62002006,62172025,U21B2021,61932011,61932014,61972018,61972019,61772538,32071775,91646203);国防基础科研计划(JCKY2021211B017)。; 对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模...; 关键词：鉴权协议 5GAKA协议 Lowe分类法形式化分析 TAMARIN

5G网络认证及密钥协商协议的安全性分析被引量：7: 《清华大学学报（自然科学版）》2021年第11期1260-1266,共7页贾凡严妍袁开国赵璐婧; 国家自然科学基金资助项目(61872033)。; 5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA'协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAMARI...; 关键词：5G网络安全 EAP-AKA' Lowe分类法 TAMARIN

Antibacterial Activities of Psidium guajava(Guava) and Velvet tamarin(Icheku) Local Chewing Sticks on Streptococcus mutansIsolated from Human Mouth被引量：1: 《Open Journal of Medical Microbiology》2021年第2期80-90,共11页I. A. Ojiuko C. O. Anyamene C. U. Ezebialu A. P. Unamadu C. S. Alisigwe; Globally dental diseases are mainly caused by Streptococcus mutans由于版权政策及相关保密法规原因，条结果未予显示。

TAMARIN