伴随着网络攻击的常态化、多样化、多变化,入侵检测技术受到越来越多的关注。入侵检测技术根据检测原理不同可分为误用检测和异常检测,然而由于异常检测存在天然的缺陷导致其误报率较高,所以国际上已经实现的入侵检测系统大多使用基于模式匹配的误用检测技术。然而,随着网络上数据的膨胀以及攻击手段的日益复杂,基于模式匹配技术检测能力明显不足,因此,基于模型检测的入侵检测技术被提出。与传统入侵检测技术相比,基于模型检测的入侵检测技术可以检测复杂变化的攻击类型,然而该检测方法仍然存在若干问题需要研究。首先缺乏对一些常见攻击类型的建模研究以及相关的性能比较。其次,缺乏对复杂变化的通用类型攻击建立通用攻击模型。本文所做的工作如下：1.对KDD CUP数据集中的11种常见的攻击类型进行了攻击原理分析,根据每种攻击的攻击细节推导出攻击的原子动作序列,在此基础上,得到每种攻击的原子公式集合,并根据动作行为建立了所有攻击类型的时间区间时序逻辑公式,根据公式便可对这些类型的攻击实施检测,通过仿真实验表明,基于模型检测的入侵检测方法检测能力更强。2.提出了一种基于并发命题投影时序逻辑(CPPTL)的通用类型攻击检测模型(UTA)。利用CPPTL对五种攻击者、八种攻击效果、六种攻击工具建立形式化公式描述,得到通用类型攻击模型的通用公式。通过对共性模型公式和数据集进行模型检测算法实验,结果表明新模型可涵盖更广的检测范围,并能够检测复杂变化的通用类型网络攻击。