基于Tamarin的MQTT协议安全性分析方法

MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。

基于Tamarin的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种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.

Avoiding hepatic metastasis naturally: Lessons from the cotton top tamarin(Saguinus oedipus )

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.

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

Globally dental diseases are mainly caused by Streptococcus mutans, it is one of the leading causative agents of dental caries worldwide, because of its resistance to conventional antibacterial agents, alternative therapies are used to control resistance of oral pathogens. This research was done to determine the antibacterial activities of Psidium guajava (guava) and Velvet tamarin (Icheku) chewing sticks on Streptococcus mutans isolated from the oral cavity. The study was conducted in Owerri Imo State Nigeria during November-December 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 Psidium guajava (guava) and Velvet tamarind (Icheku) extracts were prepared, Muller-Hinton media was used to put together the extract of serial dilutions of Psidium guajava (guava) and Velvet tamarin (Icheku) and a microbiological procedure were used for visually determining the minimum inhibitory concentration as well as minimum bactericidal concentration. Phytochemical evaluation of the plants’ extracts revealed that it contains saponins, tannins, alkaloid, steriods, glycosides and phenol. The results obtained from the antibacterial susceptibility testing of the extracts against Streptococcus mutans showed that the zones of inhibition recorded ranged from 18 mm to 27 mm. Ethanol (Soxhlet) extract of Icheku twig showed no zone of inhibition on the isolated organism. The ethanol (soxhlet) extract of the individual Psidium guajava (guava) and Velvet tamarin (Icheku) has a better antibacterial effect when compared to their aqueous extracts and combined forms. Psidium guajava (Guava) and Velvet tamarin (Icheku) twigs are made up of composite that is active against S. mutans and can be used in oral hygiene. There is a 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.

基于Tamarin的门罗币支付协议分析方法

门罗币作为一款基于区块链技术的高度匿名加密货币协议,旨在为用户提供强大的隐私保护功能。与其他加密货币不同,门罗币通过独特的支付协议对用户的交易隐私加强保护。然而,支付协议中存在的安全漏洞可能导致攻击者对交易信息进行分析或拦截,从而威胁用户的隐私安全。目前,对门罗币支付协议的研究主要集中在对匿名性漏洞的攻击,大部分攻击从外部特征出发,缺少对门罗币机制进行探索,不能充分保障支付过程的安全性和不可追踪性。因此需要进行更系统化的分析,以全面评估门罗币支付协议的安全性和不可追踪性。文章从模型规则、属性定义等角度对门罗币支付协议进行细粒度建模,并运用已有的Tamarin工具对相关属性进行验证,研究结果揭示了多个门罗币支付协议漏洞,并给出优化建议。

基于Tamarin Prover的5G 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自动化验证了该补丁方案的有效性。

基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。

一种具有前向安全的TLS协议0-RTT握手方案

针对传输层安全(TLS)协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT握手方案,传输的早期数据由于不存在身份认证,容易遭受重放、伪造以及中间人的攻击,并且不满足前向安全的问题,提出一种具有前向安全的0-RTT优化握手方案,使用Tamarin安全协议形式化分析工具对改进前、后的协议进行形式化验证,结果表明:改进方案的早期数据在原方案之上具有了前向保密的安全性质。

OTFS-Based Efficient Handover Authentication Scheme with Privacy-Preserving for High Mobility Scenarios

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.

基于观察等价性的协议猜测攻击形式化检测方法

由于口令的低熵性,针对基于口令的安全协议存在特有的口令猜测攻击,当前的形式化语义不能较好地刻画攻击者执行口令猜测攻击的条件,对于协议抗猜测攻击能力没有统一的形式化安全属性定义.本文提出了基于观察等价性的协议猜测攻击形式化检测方法.使用多集重写规则对协议交互流程进行形式化建模,给出了口令初始化、口令猜测行为的标准化规则,修改完善基于口令的对称加密原语,以支持包含基于口令的对称加密的协议验证.理论上将协议口令猜测攻击的形式化分析检测转换为正确猜测和错误猜测下多集重写规则双系统的观察等价性是否成立的判断问题;实现上使用Tamarin形式化分析工具对协议是否存在口令猜测攻击进行自动化分析,首次实现了形式化分析工具对口令猜测攻击路径的自动化生成.使用该方法对EKE、SPAKE等传统口令认证协议和多因子认证协议进行形式化建模和分析,对其中存在口令猜测攻击的协议自动化生成可行的口令猜测攻击路径,验证了方法的正确性和有效性.

基于Lowe分类法的5G网络EAP-AKA’协议安全性分析

移动网鉴权认证协议攻击不断涌现,针对5G网络新协议EAP-AKA’,该文提出一种基于Lowe分类法的EAP-AKA’安全性分析模型。首先对5G网络协议EAP-AKA’、信道及攻击者进行形式化建模。然后对Lowe鉴权性质进行形式化描述,利用TAMARIN证明器分析协议中安全锚点密钥KSEAF的Lowe鉴权性质、完美前向保密性、机密性等安全目标,发现了3GPP隐式鉴权方式下的4条攻击路径。最后针对发现的安全问题提出2种改进方案并验证其有效性,并将5G网络两种鉴权协议EAP-AKA’和5G AKA的安全性进行了对比,发现前者在Lowe鉴权性质方面更安全。

一株产生EB病毒的狨猴淋巴细胞株的建立

用Ｂ９５８细胞株产生的ＥＢ病毒，转化棉顶狨猴外周血淋巴细胞，获得ＫＭＴ３细胞株。该细胞株能产生高滴度的ＥＢ病毒。含ＥＢ病毒衣壳抗原的自然阳性细胞率为３～５％，激活后达５０～６０％，其培养上清液可直接转化人淋巴细胞得到传代细胞系。

笼养棉顶狨猴的育婴行为

笼养棉顶狨猴的育婴行为直接影响婴猴的存活率。作者的研究发现，除了双亲猴的抚育经验外，母猴产后身体状况、婴猴的体重及每胎仔猴个体数均与双亲猴背负、残害、遗弃婴猴行为有关。采取人工喂养是提高婴猴存活率的主要手段。

5G网络认证及密钥协商协议的安全性分析

5G网络发展迅速,作为系统安全基础的认证和密钥协商协议,其安全性是5G安全的核心问题。该文借助TAMARIN证明程序对5G网络中的EAP-AKA'协议进行建模分析。通过分析协议规范将安全性需求归纳为保密属性和认证属性两种安全属性,利用TAMARIN建立模型来验证不同安全属性的满足程度。根据TAMARIN证明程序返回的验证结果,该文发现了SEAF与AUSF间关于SNID的单射一致性违反以及锚定密钥K_(SEAF)前向保密性的违反,从而发现了重放攻击、身份验证同步失败攻击以及锚定密钥K_(SEAF)泄露攻击,并针对这些攻击提出了相应的安全加固方法,最后对方法进行理论分析和实验验证。