期刊文献+
共找到15篇文章
< 1 >
每页显示 20 50 100
基于Tamarin的门罗币支付协议分析方法
1
作者 李雨昕 黄文超 +1 位作者 王炯涵 熊焰 《信息网络安全》 CSCD 北大核心 2024年第5期756-766,共11页
门罗币作为一款基于区块链技术的高度匿名加密货币协议,旨在为用户提供强大的隐私保护功能。与其他加密货币不同,门罗币通过独特的支付协议对用户的交易隐私加强保护。然而,支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析... 门罗币作为一款基于区块链技术的高度匿名加密货币协议,旨在为用户提供强大的隐私保护功能。与其他加密货币不同,门罗币通过独特的支付协议对用户的交易隐私加强保护。然而,支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析或拦截,从而威胁用户的隐私安全。目前,对门罗币支付协议的研究主要集中在对匿名性漏洞的攻击,大部分攻击从外部特征出发,缺少对门罗币机制进行探索,不能充分保障支付过程的安全性和不可追踪性。因此需要进行更系统化的分析,以全面评估门罗币支付协议的安全性和不可追踪性。文章从模型规则、属性定义等角度对门罗币支付协议进行细粒度建模,并运用已有的Tamarin工具对相关属性进行验证,研究结果揭示了多个门罗币支付协议漏洞,并给出优化建议。 展开更多
关键词 门罗币 tamarin 支付协议 符号模型
下载PDF
基于Tamarin的MQTT协议安全性分析方法 被引量:2
2
作者 郑红兵 王焕伟 +2 位作者 赵琪 董姝岐 井靖 《计算机应用研究》 CSCD 北大核心 2023年第10期3132-3137,3143,共7页
MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一... MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。 展开更多
关键词 MQTT协议 保密属性 认证属性 形式化分析 tamarin
下载PDF
基于Tamarin的5G AKA协议形式化分析及其改进方法 被引量:2
3
作者 刘镝 王梓屹 +3 位作者 李大伟 关振宇 孙钰 刘建伟 《密码学报》 CSCD 2022年第2期237-247,共11页
对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模... 对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模.安全性质考虑了保密性质和Lowe鉴权性质,保密性质包括安全锚点密钥KSEAF和长期共享密钥K的保密性,鉴权性质包括协议参与实体之间在参数SUPI、SNID、KSEAF上的非单射一致性,以及在KSEAF上的单射一致性.然后本文在Tamarin中验证了5G AKA协议是否满足相关安全性质,发现保密性质全部得到满足,鉴权性质一共验证了36种情况,其中有23种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结. 展开更多
关键词 鉴权协议 5GAKA协议 Lowe分类法 形式化分析 tamarin
下载PDF
Antibacterial Activities of <i>Psidium guajava</i>(Guava) and <i>Velvet tamarin</i>(Icheku) Local Chewing Sticks on <i>Streptococcus mutans</i>Isolated from Human Mouth 被引量:1
4
作者 I. A. Ojiuko C. O. Anyamene +2 位作者 C. U. Ezebialu A. P. Unamadu C. S. Alisigwe 《Open Journal of Medical Microbiology》 2021年第2期80-90,共11页
<span style="font-family:Verdana;">Globally dental diseases are mainly caused by</span><i><span style="font-family:Verdana;"> Streptococcus mutans</span></i><... <span style="font-family:Verdana;">Globally dental diseases are mainly caused by</span><i><span style="font-family:Verdana;"> Streptococcus mutans</span></i><span style="font-family:""><span style="font-family:Verdana;">, it is one of the leading causative agents of dental caries worldwide, because of its resistance to </span><span><span style="font-family:Verdana;">conventional antibacterial agents, alternative therapies are used to control resistance of oral pathogens. This research was done to determine the antibacterial activities of </span><i><span style="font-family:Verdana;">Psidium guajava</span></i><span style="font-family:Verdana;"> (guava) and </span><i><span style="font-family:Verdana;">Velvet tamarin</span></i><span style="font-family:Verdana;"> (Icheku) chewing sticks on </span><i><span style="font-family:Verdana;">Streptococcus mutans</span></i><span style="font-family:Verdana;"> isolated from the oral cavity. The study was conducted in Owerri Imo State Nigeria during November-December</span></span><span style="font-family:Verdana;"> period. Phytochemical analysis of the plant extracts was done using appropriate techniques. The procedure used for antimicrobial susceptibility test was disk diffusion method. Serial dilutions of</span><i><span style="font-family:Verdana;"> Psidium guajava</span></i><span style="font-family:Verdana;"> (guava) and </span><i><span style="font-family:Verdana;">Velvet tamarind</span></i><span style="font-family:Verdana;"> (Icheku) extracts were prepared, Muller-Hinton media was used to put together the extract of serial dilutions of </span><i><span style="font-family:Verdana;">Psidium guajava</span></i><span style="font-family:Verdana;"> (guava) and </span><i><span style="font-family:Verdana;">Velvet tamarin</span></i><span style="font-family:Verdana;"> (Icheku) and </span></span><span style="font-family:Verdana;">a </span><span style="font-family:Verdana;">microbiological procedure w</span><span style="font-family:Verdana;">ere</span><span style="font-family:Verdana;"> used for visually determining the minimum inhibitory concentration as well as minimum bactericidal concentration. Phytochemical evaluation of the plants</span><span style="font-family:Verdana;">’</span><span style="font-family:""><span style="font-family:Verdana;"> extracts revealed that it contains saponins, tannins, alkaloid, steriods, glycosides and phenol. The results obtained from the antibacterial susceptibility testing of the extracts against </span><i><span style="font-family:Verdana;">Streptococcus mutans</span></i><span style="font-family:Verdana;"> showed that the zones of inhibition recorded ranged from 18</span></span><span style="font-family:""> </span><span style="font-family:Verdana;">mm to 27</span><span style="font-family:""> </span><span style="font-family:""><span style="font-family:Verdana;">mm. Ethanol (Soxhlet) extract of I</span><span style="font-family:Verdana;">cheku twig showed no zone of inhibition on the isolated organism. The</span><span style="font-family:Verdana;"> ethanol (soxhlet) extract of the individual </span><i><span style="font-family:Verdana;">Psidium guajava</span></i><span style="font-family:Verdana;"> (guava) and </span><i><span style="font-family:Verdana;">Velvet tamarin</span></i><span style="font-family:Verdana;"> (Icheku) has a better antibacterial effect when compared to their aqueous extracts and combined forms. </span><i><span style="font-family:Verdana;">Psidium guajava</span></i><span style="font-family:Verdana;"> (Guava) and </span><i><span style="font-family:Verdana;">Velvet tamarin</span></i><span style="font-family:Verdana;"> (Icheku) twigs are made up of composite that </span></span><span style="font-family:Verdana;">is</span><span style="font-family:""><span style="font-family:Verdana;"> active against </span><i><span style="font-family:Verdana;">S. mutans</span></i><span style="font-family:Verdana;"> and can be used in oral hygiene. There is </span></span><span style="font-family:Verdana;">a </span><span style="font-family:Verdana;">need for further investigation on the plant extracts as the rural poor make use of it because it is cheap, readily available and the rich also use it once they are in the village mostly in Eastern Nigeria. Similarly chewing sticks has been reported to be practiced by 90 of rural population in Nigeria</span><span style="font-family:Verdana;">. 展开更多
关键词 Antibacterial Activity Chewing Sticks Psidium guajava (Guava) Velvet tamarin (Icheku) Streptococcus mutans
下载PDF
Avoiding hepatic metastasis naturally: Lessons from the cotton top tamarin(Saguinus oedipus )
5
作者 Martin Tobi Peter Thomas Daniel Ezekwudo 《World Journal of Gastroenterology》 SCIE CAS 2016年第24期5479-5494,共16页
Much has been written about hepatic metastasis and animal models abound. In terms of the human experience, progress in treating this final common pathway, a terminal event of many human malignancies has been relativel... Much has been written about hepatic metastasis and animal models abound. In terms of the human experience, progress in treating this final common pathway, a terminal event of many human malignancies has been relatively slow. The current thinking is that primary prevention is best served by early detection of cancer and eradication of early stage cancers by screening. Some cancers spread early in their course and the role of screening may be limited. Until relatively recently there has not been a pathfinder model that makes the evasion of this unfortunate event a reality. This review discusses such an animal model and attempts to relate it to human disease in terms of intervention. Concrete proposals are also offered on how scientists may be able to intervene to prevent this deadly progression of the cancer process. 展开更多
关键词 COTTON TOP tamarin Hepatic metastasis Carcinoembryonic ANTIGEN FIBULIN-5 Common MARMOSET
下载PDF
Effects of Dried Black Cumin and Tamarind Supplementation on Egg Performance and Lipids Concentration in Egg Yolk of Layer Hens
6
作者 S. Yingyuen S. Wongsuthavas +4 位作者 C. Yuangklang K. Vasupen S. Bureenok S. Kempaka A. C. Beynen 《Journal of Agricultural Science and Technology(A)》 2011年第8期1133-1136,共4页
This study was aimed to determine the effects of dried black cumin and tamarind supplementation on egg performance and lipids concentration in egg yolk of layer hens. Sixty laying hens at the age of 18-34 weeks were d... This study was aimed to determine the effects of dried black cumin and tamarind supplementation on egg performance and lipids concentration in egg yolk of layer hens. Sixty laying hens at the age of 18-34 weeks were divided into 4 treatments (control, 1% black cumin, 4% tamarind and 1% black cumin + 4% tamarin in diets) with 4 replications each (15 birds/replication). The experimental treatments were subjected to completely randomized design. Feed and drinking water were provided ad-libitum. 16 h per day for lighting program during experimental period. The results found that feed efficiency ratio, egg production and egg weight were no significant between treatments. However, average daily feed intake was highest in 4% tamarind and 1% black cumin + 4% tamarin in diets. Egg yolk color score, yolk index, white index and shell tickness were no significantly different, However, haugh unit was lowest in control group. Egg yolk lipids concentration was founded that black cumin and tamarind in diet were reduced cholesterol and triacyl-glycerol concentration with statistical significance (P 〈 0.05). So that dried black cumin and tamarind supplementation in diets were no any effect on egg production and egg weight. Furthermore, egg yolk cholesterol and triacyl-glycerol concentration were decreased. Hence, supplementation of dried black cumin and tamarind in diets could benefit to consumer health. 展开更多
关键词 Black cumin tamarin laying hen cholesterol TRIGLYCERIDE
下载PDF
基于Tamarin Prover的5G EAP-TLS协议的形式化分析
7
作者 马壮壮 杜瑞颖 +1 位作者 陈晶 何琨 《武汉大学学报(理学版)》 CAS CSCD 北大核心 2023年第5期653-664,共12页
为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对... 为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此,对5G EAP-TLS协议进行详细的描述,并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模,同时从5G规约中提取并建模了与5G EAPTLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索,解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题,实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果,发现了5G EAP-TLS协议能够满足机密性目标,但难以满足一些认证性目标,同时,揭示了协议存在拒绝服务(denial of service,DoS)攻击和用户通信数据泄露的隐患。针对发现的问题,提出了相应的补丁方案,并通过提出的证据搜索策略引导分析工具Tamarin Prover自动化验证了该补丁方案的有效性。 展开更多
关键词 5G专用网络 EAP-TLS协议 形式化分析 tamarin Prover 自动化验证
原文传递
基于安全协议代码的形式化辅助建模研究 被引量:2
8
作者 葛艺 黄文超 熊焰 《计算机应用研究》 CSCD 北大核心 2023年第4期1189-1193,1202,共6页
随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方... 随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。 展开更多
关键词 形式化验证 形式化建模 协议代码 污点分析 tamarin
下载PDF
一种具有前向安全的TLS协议0-RTT握手方案
9
作者 蒲鹳雄 缪祥华 袁梅宇 《化工自动化及仪表》 CAS 2023年第6期813-819,832,共8页
针对传输层安全(TLS)协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT握手方案,传输的早期数据由于不存在身份认证,容易遭受重放、伪造以及中间人的攻击,并且不满足前向安全的问题,提出一种具有前向安全的0-RTT优化握手方案,... 针对传输层安全(TLS)协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT握手方案,传输的早期数据由于不存在身份认证,容易遭受重放、伪造以及中间人的攻击,并且不满足前向安全的问题,提出一种具有前向安全的0-RTT优化握手方案,使用Tamarin安全协议形式化分析工具对改进前、后的协议进行形式化验证,结果表明:改进方案的早期数据在原方案之上具有了前向保密的安全性质。 展开更多
关键词 传输层安全(TLS) 完美前向安全(PFS) 0-RTT优化握手方案 安全协议形式化分析 tamarin
下载PDF
OTFS-Based Efficient Handover Authentication Scheme with Privacy-Preserving for High Mobility Scenarios
10
作者 Dawei Li Di Liu +1 位作者 Yu Sun Jianwei Liu 《China Communications》 SCIE CSCD 2023年第1期36-49,共14页
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... 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 deterioration of network link quality.Therefore,high mobility scenarios require handover schemes with less handover overhead.However,some existing schemes that meet this requirement cannot provide strong security guarantees,while some schemes that can provide strong security guarantees have large handover overheads.To solve this dilemma,we propose a privacy-preserving handover authentication scheme that can provide strong security guarantees with less computational cost.Based on Orthogonal Time Frequency Space(OTFS)link and Key Encapsulation Mechanism(KEM),we establish the shared key between protocol entities in the initial authentication phase,thereby reducing the overhead in the handover phase.Our proposed scheme can achieve mutual authentication and key agreement among the user equipment,relay node,and authentication server.We demonstrate that our proposed scheme can achieve user anonymity,unlinkability,perfect forward secrecy,and resistance to various attacks through security analysis including the Tamarin.The performance evaluation results show that our scheme has a small computational cost compared with other schemes and can also provide a strong guarantee of security properties. 展开更多
关键词 high mobility condition handover authentication PRIVACY-PRESERVING tamarin OTFS
下载PDF
基于观察等价性的协议猜测攻击形式化检测方法
11
作者 苗旭阳 顾纯祥 陆思奇 《密码学报》 CSCD 2023年第2期306-319,共14页
由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化... 由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性. 展开更多
关键词 形式化分析 观察等价性 口令猜测攻击 tamarin-Prover
下载PDF
基于Lowe分类法的5G网络EAP-AKA’协议安全性分析 被引量:15
12
作者 刘彩霞 胡鑫鑫 +2 位作者 刘树新 游伟 赵宇 《电子与信息学报》 EI CSCD 北大核心 2019年第8期1800-1807,共8页
移动网鉴权认证协议攻击不断涌现,针对5G网络新协议EAP-AKA’,该文提出一种基于Lowe分类法的EAP-AKA’安全性分析模型。首先对5G网络协议EAP-AKA’、信道及攻击者进行形式化建模。然后对Lowe鉴权性质进行形式化描述,利用TAMARIN证明器... 移动网鉴权认证协议攻击不断涌现,针对5G网络新协议EAP-AKA’,该文提出一种基于Lowe分类法的EAP-AKA’安全性分析模型。首先对5G网络协议EAP-AKA’、信道及攻击者进行形式化建模。然后对Lowe鉴权性质进行形式化描述,利用TAMARIN证明器分析协议中安全锚点密钥KSEAF的Lowe鉴权性质、完美前向保密性、机密性等安全目标,发现了3GPP隐式鉴权方式下的4条攻击路径。最后针对发现的安全问题提出2种改进方案并验证其有效性,并将5G网络两种鉴权协议EAP-AKA’和5G AKA的安全性进行了对比,发现前者在Lowe鉴权性质方面更安全。 展开更多
关键词 网络安全 安全锚点密钥 EAP-AKA’ Lowe分类法 Dolev-Yao敌手模型 tamarin
下载PDF
一株产生EB病毒的狨猴淋巴细胞株的建立
13
作者 孙晓梅 梁梧生 +1 位作者 代解杰 高家鸿 《中国病毒学》 CSCD 1998年第1期29-33,共5页
用B958细胞株产生的EB病毒,转化棉顶狨猴外周血淋巴细胞,获得KMT3细胞株。该细胞株能产生高滴度的EB病毒。含EB病毒衣壳抗原的自然阳性细胞率为3~5%,激活后达50~60%,其培养上清液可直接转化人淋巴细胞得... 用B958细胞株产生的EB病毒,转化棉顶狨猴外周血淋巴细胞,获得KMT3细胞株。该细胞株能产生高滴度的EB病毒。含EB病毒衣壳抗原的自然阳性细胞率为3~5%,激活后达50~60%,其培养上清液可直接转化人淋巴细胞得到传代细胞系。 展开更多
关键词 淋巴细胞 EB病毒 细胞株 棉顶绒猴
下载PDF
笼养棉顶狨猴的育婴行为 被引量:1
14
作者 梁梧生 黄小琴 练幼辉 《上海实验动物科学》 1995年第1期14-16,共3页
笼养棉顶狨猴的育婴行为直接影响婴猴的存活率。作者的研究发现,除了双亲猴的抚育经验外,母猴产后身体状况、婴猴的体重及每胎仔猴个体数均与双亲猴背负、残害、遗弃婴猴行为有关。采取人工喂养是提高婴猴存活率的主要手段。
关键词 棉顶狨猴 育婴行为 人工饲养 实验动物
下载PDF
5G网络认证及密钥协商协议的安全性分析 被引量:6
15
作者 贾凡 严妍 +1 位作者 袁开国 赵璐婧 《清华大学学报(自然科学版)》 EI CAS CSCD 北大核心 2021年第11期1260-1266,共7页
5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA'协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAM... 5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA'协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAMARIN建立模型来验证不同安全属性的满足程度。根据TAMARIN证明程序返回的验证结果,该文发现了SEAF与AUSF间关于SNID的单射一致性违反以及锚定密钥K_(SEAF)前向保密性的违反,从而发现了重放攻击、身份验证同步失败攻击以及锚定密钥K_(SEAF)泄露攻击,并针对这些攻击提出了相应的安全加固方法,最后对方法进行理论分析和实验验证。 展开更多
关键词 5G网络安全 EAP-AKA' Lowe分类法 tamarin
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部