检索结果-南通市图书馆

实例化空间:一种新的安全协议验证逻辑的语义模型

在线全文

学校读者我要写书评

暂无评论

计算机学报 2006年第9期29卷 1657-1665页

作者：苏开乐岳伟亚陈清亮 ZHENG Xi-Zhong 中山大学计算机科学系广州510275 勃兰登堡州理工大学计算机科学系

给出了一个称为“实例化空间(instantiation space)”的安全协议验证逻辑的语义模型.该语义模型是建立在一种自然的加密信息交换(cryptographical message exchange)模型上的.在此语义模型基础上,文章提出了一系列与安全属性相关的验证... 详细信息

给出了一个称为“实例化空间(instantiation space)”的安全协议验证逻辑的语义模型.该语义模型是建立在一种自然的加密信息交换(cryptographical message exchange)模型上的.在此语义模型基础上,文章提出了一系列与安全属性相关的验证公理,由此可以证明它们在此语义模型下的正确性.更重要的是,在此语义下的公理集在算法上是完全可以实现的,其对应的工具SPV(Security Protocol Verifier)已经开发成功,并且可以验证复杂的协议.在这套安全协议验证模型理论下,可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式.而且,在此语义基础上的公理集是纯命题逻辑的,因此所需要的验证目标可以很方便地转化成可满足性问题(SAT),从而可以利用工业上快速高效的SAT求解器实现.

关键词：实例化空间加密信息交换模型可满足性问题

SET证书申请协议在SPV下的自动化验证及改进

在线全文

学校读者我要写书评

暂无评论

计算机学报 2008年第6期31卷 1035-1045页

作者：肖茵茵苏开乐岳伟亚陈清亮吕关锋杨晋吉中山大学信息科学与技术学院广东省信息安全重点实验室广州510275 暨南大学计算机科学系广州510632 北京工业大学计算机学院北京100022

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPS... 详细信息

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.

关键词： SET证书申请协议自动化验证 SPV 认证性秘密性

Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2006年第6期21卷 932-943页

作者：苏开乐陈清亮 Abdul Sattar 岳伟亚吕关锋郑锡忠 Department of Computer Science Sun Yat-Sen University Guangzhou 510275 P.R China Institute for Integrated and Intelligent Systems Griffth University Brisbane Qld 4111 Australia College of Computer Science and Technology Beijing University of Technology Beijing 100022 P.R. China Department of Computer Science Brandenburg University of Technology Cottbus 03036 Germany

This paper introduces a new methodology for epistemic logic, to analyze communication protocols that uses knowledge structures, a specific form of Kripke semantics over hostile networks. The paper particularly focuses on automatic verification of authentication protocols. Our approach is based on the actual definitions of a protocol, not on some difficultto-establish justifications. The proposed methodology is different from many previous approaches to automatic verification of security protocols in that it is justification-oriented instead of falsification-oriented, i.e., finding bugs in a protocol. The main idea is based on observations： separating a principal executing a run of protocol from the role in the protocol, and inferring a principal＇s knowledge from the local observations of the principal. And we show analytically and empirically that this model can be easily reduced to Satisfiability （SAT） problem and efficiently implemented by a modern SAT solver.

关键词： authentication protocol formal verification knowledge structure SAT

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

基于BDD的图表示及其算法

中山大学学报（自然科学版） 2006年第1期45卷 20-24页

作者：吕关锋苏开乐林瀚骆翔宇陈清亮岳伟亚中山大学计算机科学系广东广州510275

给出基于二元判决图BDD的无权图和有权图的符号化表示,同时给出该表示下的算法设计及实现,并以连通度算法和最短路径算法作为例子。

关键词： BDD 符号化算法连通度最短路径

一种规约于可满足性问题(SAT)的知识推理算法

在线全文

学校读者我要写书评

暂无评论

计算机科学与探索 2007年第1期1卷 79-86页

作者：苏开乐陈清亮岳伟亚中山大学计算机科学系广州510275

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary ... 详细信息

传统的知识推理算法主要依赖于通用的定理证明器,因此会有明显的组合爆炸问题和半自动化问题,只能处理小规模的问题。在文[1]中,给出了一个实用而紧致的知识的语义模型——知识结构(knowledge struc- ture),并给出相应的利用BDD(Binary Decision Diagram)的符号化计算方法,实验表明这种基于BDD的算法比传统方法有很大的优势,但这种基于BDD的方法在计算规模大的例子时仍存在明显的组合爆炸。文章在知识结构(knowledge structure)的语义基础上,通过挖掘知识结构语义中各元素的关系,把知识的计算规约于可满足性问题(SAT),因为SAT Solver在符号化计算方面以及在计算规模和效率上都要明显优于BDD。实验结果证实了这种方法的有效性。

关键词：可满足性问题知识结构推理算法计算规模组合爆炸计算方法符号化定理证明器语义模型语义基础实验结构语义自动化小规模元素效率通用处理

在线全文

学校读者我要写书评

暂无评论

数学形态学在图像处理中的应用与展望

影像技术 2006年第2期18卷 19-21页

作者：岳洪伟李扬蔡肯岳伟亚广东工业大学信息工程学院广州510643 中山大学计算机科学系广州510275

阐述数学形态学的产生及其与图像处理的结合过程,讨论其由二值形态学、灰度形态学、软形态学到模糊形态学、模糊软形态学、形态小波的发展,分析了数学形态学在图像处理中的发展趋势并对其应用前景进行探讨与展望。

关键词：灰度形态学软形态学模糊形态学模糊软形态学形态小波

骨髓微环境中不同细胞对多发性骨髓瘤骨病外泌体环状RNA的贡献及相互作用

在线全文

学校读者我要写书评

暂无评论

中国组织工程研究 2025年

作者：于漫亚崔兴山东中医药大学第一临床学院山东中医药大学第二附属医院肿瘤中心

背景：多发性骨髓瘤骨病是多发性骨髓瘤的严重并发症，其发病机制与骨髓微环境失调密切相关。外泌体环状RNA因高稳定性、高丰度、高特异性、高保守性等特点，正逐渐成为液体活检的焦点。在多发性骨髓瘤骨病中，外泌体环状RNA的作用尚缺... 详细信息

背景：多发性骨髓瘤骨病是多发性骨髓瘤的严重并发症，其发病机制与骨髓微环境失调密切相关。外泌体环状RNA因高稳定性、高丰度、高特异性、高保守性等特点，正逐渐成为液体活检的焦点。在多发性骨髓瘤骨病中，外泌体环状RNA的作用尚缺乏相关研究。随着单细胞测序技术的发展，明确骨髓微环境中各类型细胞对多发性骨髓瘤骨病相关外泌体环状RNA的贡献及相互作用，有助于为多发性骨髓瘤骨病的诊疗提供新的生物标志物。目的：初步明确多发性骨髓瘤骨病相关外周血外泌体环状RNA的骨髓微环境来源细胞，并在单细胞水平上探究骨髓微环境中各细胞相互作用对多发性骨髓瘤骨病的影响。方法：对6例多发性骨髓瘤骨病患者和5名健康志愿者的外周血外泌体进行高通量测序，筛选差异环状RNA，并进行GO和KEGG富集分析。从GEO数据库中获取多发性骨髓瘤骨病患者的骨髓单细胞测序数据集GSE271107，对其中的4例多发性骨髓瘤骨病患者数据进行整合，完成质控和过滤后，利用Harmony法去除批次效应，UMAP进行亚群聚类，SingleR自动注释后手动矫正细胞群，CellChat对单细胞测序数据中的细胞间通讯进行推断和可视化，分析配体、受体间的相互作用。结果与结论：(1)相较于健康志愿者，多发性骨髓瘤骨病患者外周血外泌体中1 265个环状RNA表达水平显著上调；(2)GO和KEGG分析差异环状RNA的亲本基因主要富集在神经系统发育、癌症中的通路、PI3K-Akt信号通路、Hippo信号通路、致心律失常性右心室心肌病、扩张型心肌病等，这与骨髓瘤细胞的增殖、黏附、迁移、归巢，以及多发性骨髓瘤相关并发症(如多发性骨髓瘤骨病、周围神经病变、心脏事件)关系密切；(3)多发性骨髓瘤骨病相关差异环状RNA的亲本基因主要来源于骨髓微环境中的T细胞/自然杀伤细胞、B细胞和单核/巨噬细胞，通过调节多种细胞因子的分泌影响破骨细胞功能；(4)单核细胞/巨噬细胞作为破骨细胞前体细胞与骨髓瘤细胞及其他免疫细胞间均有相互作用，MIF通路是其参与的主要通路。以上结果初步明确了多发性骨髓瘤骨病相关外周血外泌体环状RNA的骨髓微环境来源细胞，并发现单核/巨噬细胞与骨髓瘤细胞及免疫细胞间的MIF通路配体-受体相互作用可能是多发性骨髓瘤骨病发生的重要因素。

关键词：多发性骨髓瘤骨病外泌体环状RNA 单细胞测序骨髓微环境破骨细胞 PI3K-Akt信号通路 Hippo信号通路工程化外泌体

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

爱上学校：构筑我的教育理想国

中小学管理 2025年第1期 5-8页

作者：滕亚杰北京市东城区府学胡同小学

“怀着崇敬接纳孩子，带着爱教育他们，护送他们迈上自由之旅。”每每念起奥地利哲学家鲁道夫·斯坦纳的这首小诗，我的眼眶总是不禁湿润起来。从事教育工作30余载，从一名普通教师成长为正高级教师、特级教师和特级校长，我的所有思绪...

“怀着崇敬接纳孩子，带着爱教育他们，护送他们迈上自由之旅。”每每念起奥地利哲学家鲁道夫·斯坦纳的这首小诗，我的眼眶总是不禁湿润起来。从事教育工作30余载，从一名普通教师成长为正高级教师、特级教师和特级校长，我的所有思绪和情感、我的心、我的爱始终深深扎根于学校这片沃土。这些年来，我先后走过6所学校，其中担任校长19年。我当校长，最想做的事情就是办好一所学校，守护好、激励好、发展好学校里每一位师生，办一所在北京市乃至全国都叫得响的学校。多年来，我带领我的团队一步一个脚印，用心血、汗水、智慧，努力构筑着我们心中的教育理想国。

关键词：

基于注意力胶囊网络的梨树叶部病害图像识别方法

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

农机化研究 2025年

作者：彭炜峰张洲亚西南大学重庆水利电力职业技术学院

针对梨树叶部病害人工识别防治工作中存在主观性强、耗时费工、效率低下、误判率高,以及当前部分网络算法和信息技术对梨树叶部病害图像识别准确率较低的问题,以重庆市永川区黄瓜山梨种植基地为研究区域,以胶囊网络为基础,提出了一种基... 详细信息

针对梨树叶部病害人工识别防治工作中存在主观性强、耗时费工、效率低下、误判率高,以及当前部分网络算法和信息技术对梨树叶部病害图像识别准确率较低的问题,以重庆市永川区黄瓜山梨种植基地为研究区域,以胶囊网络为基础,提出了一种基于注意力胶囊网络的梨树叶部病害图像识别方法。首先,融入优化的注意力机制和残差密集单元,提高模型对病害图像特征提取能力;其次,在不改变网络结构的基础上,验证了不同参数、不同迭代次数对病害图像识别效果的影响;最后,在基本参数相同的情况下,验证了不同算法对病害图像识别的有效性。通过与传统胶囊网络、卷积神经网络、CNN等多种算法在准确率、有效性方面的对比试验,基于注意力胶囊网络的梨树叶部病害识别方法准确率达到93.74%,能够有效抑制病害图像中不相关特征,并很好地提取梨树叶部病害图像有效关键特征,具有较强的病害图像识别能力。研究结果可为梨树叶部病害智能识别诊断鉴定提供新思路、新方法,对推进智慧农业发展和农业农村现代化建设提供理论参考。

关键词：梨树叶部病害图像识别注意力机制胶囊网络智慧农业