目前国际上已实现的入侵检测系统绝大多数使用模式匹配来检测入侵。随着网络数据量的增大，上述系统面临着一些难以解决的问题。为此,一些形式化的方法被提了出来并被应用到入侵检测系统中去。其中基于命题线性时序逻辑(PLTL)的方法即为其中具有代表性的一种,并被证实可用来检测可变化的复杂攻击。然而，基于PLTL的方法与其他相关方法相比，其综合性能有哪些优势与不足，目前尚不清楚，这是本文开展研究和解决的问题。本文所做的主要工作包括两个部分：（1）详细分析了误用检测技术中的模式匹配算法(MPA)和基于模型检测的入侵检测算法(MCA)。并在KDD99数据集的基础上，构造基于行为的入侵检测数据集，开展仿真实验，从而对这两个算法的检测能力、检测效率进行了比较。（2）提出了一种基于投影时序逻辑（PTL）的多类型攻击检测方法(USA)。该方法主要通过对攻击者、攻击过程、攻击效果建立形式化子模型，利用PTL把子模型结合起来，得到多类型攻击的PTL公式模型。将数据集和公式模型作为输入，利用模型检测算法来检测入侵。实验结果表明，新方法的检测能力更加全面和有效。上述的研究工作对入侵检测算法的性能比较获得了一些初步结论，从而为实际应用中相关算法的选择提供了参考依据。