一种理性安全协议形式化分析方法及应用

博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证.不过在理性环境下,由于参与者对知识的自利性,ATL和ATEL都不适合形式化分析与验证理性安全协议.于是在并行认知博弈结构CEGS中引入效用函数和偏好关系,得到新的并行认知博弈结构rCEGS,并在合作模态算子《Γ》中引入行为ACT参数,提出新的交替时序认知逻辑rA-TEL-A,并基于不动点描述rATEL-A时序算子.然后基于rATEL-A,提出适合于形式化分析理性安全协议的推理系统,并对具体的理性安全协议的公平性、安全性等性质进行形式化分析.     

不可否认协议形式化分析的SVO逻辑方法

使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析．在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因．这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等．分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标．通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性．     

模糊交互时态逻辑及其语义结构

Alur等人建立的交互时态逻辑（ATL ＊）是一种重要的多Agent合作逻辑,它对计算树逻辑（CTL ＊）进行了合作算子拓展,然而它缺乏对不确定时态信息的刻画。通过考察模糊时态事件和模糊时态状态、描述相对时间来改进并发博弈结构,并给出模糊并发博弈结构;把模糊并发博弈结构的若干要件从相对时间域到绝对时间域进行映射,给出已映射模糊并发博弈结构;建立了模糊交互时态逻辑（FATL ＊）,给出其语法,在已映射模糊并发博弈结构下给出其语义;阐述了FATL ＊的表达力比ATL ＊强。     

分析和设计安全协议的新逻辑的语义

文献[1]中提出了一种分析和设计安全协议的新逻辑.协议分析者可以用该逻辑来对安全协议进行分析,而协议设计者可以使用该逻辑用一种系统的方法来构造安全协议.文献[1]没有给出该逻辑的形式化语义,因为串空间模型具有良好的语义,现将新逻辑和串空间模型结合起来,给出新逻辑的串空间语义,并运用该语义证明了新逻辑的推理规则是正确的.     

基于PCL的改进型Helsinki协议的形式化分析

针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于"Cords演算"的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.     

Andrew Secure RPC协议的一种组合分析方法

逻辑方法和模型检验方法是安全协议的两种重要分析方法。逻辑方法简单、直观,但其最大问题是不够完备,模型检验方法自动化程度高且能生成不满足所需求性质的反例。先用BAN逻辑对Andrew Secure RPC协议进行分析,并在此基础上组合模型检验方法进行分析,结果表明逻辑方法组合模型检验方法分析协议比只用逻辑方法分析得到的结果更全面且更具体。     

EKE协议的描述与TLA验证

行为时序逻辑(TLA)是Leslie Lamport于20世纪90年代提出的一种新的逻辑,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达模型程序与系统属性。文中首先介绍了行为时序逻辑的语法和语义,然后以EKE协议为例,用基于行为时序逻辑语言TLA+对EKE协议进行了建模分析,用TLA建模并用行为时序逻辑语言TLA+进行协议的描述,最后用TLC检测工具进行分析,发现存在中间人的重放攻击漏洞。     

应用逻辑推导图方法对一个不可否认协议的分析

以之前所提出基于模态逻辑的协议推导分析方法为基础, 用Java专家系统外壳(JESS)实现了协议推导分析工具, 对一个具体的不可否认协议进行分析,以验证逻辑推导图方法的作用.分析结果清晰地显示各协议内容对协议目标实现的作用, 并以此为基础说明协议内容中的冗余.通过与传统协议分析方法进行比较, 说明了这一方法可以更清晰地说明协议内容对协议目标的贡献作用.同时,也在分析过程中指出了SVO逻辑协议分析方法对假设的过度依赖性这一缺陷.     

Andrew Secure RPG协议的一种组合分析方谢

逻辑方法和模型检验方法是安全协议的两种重要分析方法。逻辑方法简单、直观，但其最大问题是不够完备，模型检验方法自动化程度高且能生成不满足所需求性质的反例。先用BAN逻辑对Andrew Secure RPC协议进行分析，并在此基础上组合模型检验方法进行分析，结果表明逻辑方法组合模型检验方法分析协议比只用逻辑方法分析得到的结果更全面且更具体。     

Kailar逻辑推理中初始状态假设

Kailar逻辑用于分析电子商务协议的可追究性,但初始状态假设引入不当会导致Kailar逻辑分析协议失败.通过对利用Kailar逻辑证明CMP1(b)协议与CMP1协议可追究性的过程以及对初始状态假设进行分析研究,针对初始状态假设所存在的问题,给出了初始状态假设应遵循的两个原则.实例表明,遵循该原则能够发现初始状态假设存在的问题,从而修正不适当的假设、补充新的假设,避免其引入不当所导致的Kailar逻辑分析协议失败问题.     

Multi-agent Belief, Goal and Exceptions Reasoning

Temporal logics are often adopted as basic tools to specifying mental states such as belief and goal of agents. Althoush there are works on non-monotonic extension of linear temporal logic (LTL) and branching time temporal logic (CTL), the non-monotonic extension of alternating-time temporal logic (ATL) which is an important kind of multi-agent cooperation logics has not been discussed yet in literature. To solve this problem, this paper proposed non-monotonic alternating-time temporal logic with belief and goal, namely N-ATL-BG, to facilitate the non-monotonic reasoning of mental states of agents. The semantic model, syntax and semantics of this new logic are developed. A model checking algorithm which can be finished in polynomial time is proposed for this new logic. Examples are given to show its usage.     

海量空间信息的分布式运算

阐述了在三维数字城市系统中，由于三维资料的显示速度主要依赖于数据调度和逻辑运算的速度，海量数据的调度和频繁的逻辑运算使得单机系统不堪重负，因此通过分布式计算可以在多台计算机上平衡计算负载，也可以把程序放在最适合运行它的计算机上．该分布式运算系统基于COM 中间件技术，运用VC6．0／VC7．1和Oracle9i开发环境，借助于ATL动态模板库、IDL接口定义语言，实现了在三维数字城市系统中海量空间信息的分布式调度和分布式运算．     

Nonspecific integration of the HTLV provirus genome into adult T-cell leukaemia cells

Human T-cell leukaemia virus (HTLV), previously also reported as ATLV, is a recently identified retrovirus which is closely associated with adult T-cell leukaemia (ATL) endemic in southwestern Japan and the Caribbean. Determination of the total nucleotide sequence of the HTLV genome has revealed no typical onc gene acquired from the cellular sequence. Screening of the HTLV provirus genome in tumour cells has shown that in all cases of ATL examined, the primary tumour cells contained the provirus genome and were monoclonal with respect to the integration site of the provirus. These findings suggest that ATL leukaemogenesis may be due to insertional mutagenesis in which the provirus genome is integrated into a specific locus on the chromosomal DNA and then activates an adjacent cellular onc gene, a mechanism already demonstrated in avian lymphoma and erythroblastosis induced by avian leukosis viruses. A common site of HTLV provirus integration in leukaemic cells among some ATL patients was reported by Hahn et al. but subsequently retracted. However, this retraction does not imply the random integration of the proviruses. Independently, we have been testing this insertional mutagenesis model in ATL and report here that the provirus did not have a common locus of integration in 35 ATL patients and did not integrate on the same chromosome in 2 ATL patients.     

含铝炸药震源激发地震波能量的实验研究

为提高地震波能量,通过改变震源装药组分,选用硝酸铵/TNT/铝粉(ATL)和聚黑/铝粉(JHL)2种含铝炸药及TNT等5种非含铝炸药,在相同地质条件下,采用远场测震和近场测压的方法,对地震波能量的激发效果进行了测试和评价.单炮记录结果对比发现,在保证不降低信噪比的条件下,含铝炸药产生的地震波品质优于非含铝炸药,且ATL优于JHL;地震波能量分析结果表明,与非含铝炸药相比,含铝炸药产生的地震波能量在不同时域内均有所提高,且ATL激发的地震波能量最高.炸药土中爆炸的近场压力测试结果表明,ATL炸药爆炸产生的应力波峰值压力比TNT(56.21kPa)提高了约78.76%.分析了炸药土中爆炸能量输出结构对地震波能量的影响.     

Isolation of HTLV-transformed B-lymphocyte clone from a patient with HTLV-associated adult T-cell leukaemia

The human T-cell leukaemia/lymphoma virus (HTLV) is an exogenous retrovirus which has been associated with adult T-cell leukaemia/lymphoma (ATL). This malignancy of T lymphocytes is endemic to southern Japan, the West Indies, and to a lesser extent, the Middle East, Central Africa and the southeastern United States. ATL cells from patients of diverse geographical origins have been found to be infected with HTLV-1 (ref.6). HTLV is normally tropic for mature T lymphocytes, especially those expressing the helper-inducer surface antigen phenotype (OKT4 or Leu-3-positive), and the neoplastic T cells infected with HTLV generally express receptors for T-cell growth factor (detected by reactivity with anti-Tac antibody). However, we report here the isolation of a HTLV-infected B-lymphocyte clone from the peripheral blood of a patient with ATL. This clone is cytogenetically normal and is not infected with Epstein-Barr virus (EBV). Co-culture of cells from this clone with cord blood lymphocytes resulted in transmission of HTLV and the immortalization of either T or B lymphocytes. These results suggest that HTLV may be associated with a broader range of host cells than previously recognized.     

Unique cell lines harbouring both Epstein-Barr virus and adult T-cell leukaemia virus, established from leukaemia patients

Members of three distinct classes of animal virus have been associated with naturally occurring neoplasias in man: Epstein--Barr virus (EBV), a DNA virus belonging to herpesvirus group, papillomavirus, and a novel human RNA (retro) virus, human T-cell leukemia virus or adult T-cell leukaemia (ATL) virus. We have established seven continuous cell lines from ATL patients and 0.1-7% of these cells consistently express ATL-specific antigens (ATLA). EBV-associated nuclear antigen (EBNA) is also found in more than 90% of these cells. We have cloned cells from two of these lines and show here that both ATLA and EBNA were present in the same B-cell clone carrying surface immunoglobulin (sIg).     

COM服务器的实现策略和技术

在系统地分析COM服务器软件结构及其线程模型的基础上，分别给出了使用MFC和ATL技术构造COM服务器的具体技术，最后研究了几种主要COM线程模型的实现方法。     

两重巢式PCR检测母体外周血中胎儿游离DNA

使用两重巢式PCR技术检测母体外周血中胎儿游离DNA,为非损伤性产前鉴定胎儿性别和诊断单基因疾病奠定基础.采用改良的chelex100方法提取60例孕龄为16~36周孕妇的外周血浆中游离胎儿DNA,依据NCBIX染色体长臂ATL1位点,Y染色体上DYS14位点序列,设计并合成引物,用巢式PCR同时扩增2个基因片段,以鉴定胎儿性别.结果表明:有ATL1位点和DYS14位点的扩增产物261bp和198bp鉴定为男性胎儿,而仅有261bp扩增产物鉴定为女性胎儿.均以真实出生性别进行确认后发现,此方法能有效提高检测特异性.两重巢式PCR能够简便并准确地鉴定胎儿性别,对单基因疾病特别是X-连锁遗传病的诊断有积极意义.     

桥式起重机运行机构三维参数化设计研究

以SolidWorks为设计平台,对桥式起重机运行机构进行模块划分,以3种方式对系列零件进行参数化建模;根据SolidWorks提供的API进行二次开发,在Visual C＋＋6．0的ATL模板上进行COM编程,实现了桥式起重机运行机构的参数化设计。