Design Of Email Mornitor System Based On Formal Protocol Specification

Information content security is becoming a key component of the security architecture. It is a new kind of main stream of security technique as firewall and intrusion detection system. People have made many researches and have got much achievement in this field. Email content monitoring is one of the most urgent problems to be resolved.Firstly, the current development status and the popular technology of network content security are introduced, their advantage and disadvantage is discussed.Secondly, ideal content security tool should have both fast pattern match and stably blocking mechanism. Content filter technology employ packet capture and pattern match. Robust email block depends on the ability of system to specify the protocol correctly and recognize the status of protocol intelligently. The thesis puts forward architecture for email content security monitoring, and details the key transport and control layer of the system.Transport and control protocol in our system needs to face kinds of differential implementation of email protocol and TCP protocol. Obviously this can be achieved by hard-coding protocol information into the system. However, it should be equally obvious that this would be a very inflexible solution: Each new version of a protocol would require a re-implementation of the protocol part of the system to make sure of conformance. A far more flexible solution will be considered here: The core implementation of the protocol verifier will be generic. They are then configured by feeding them with protocol specifications in a suitable format-a formal notation.Therefore a study of several important problems on formal description techniques (FDT) is conducted. First, protocol engineering and formal description techniques are introduced, to lay stress on several formal models: FSM, Petri net CSP and CCS . ESTELLE LOTOS SDL UML and MSC are introduced.After analyzed SDL system structure communication mechanism and data type, we use SDL toolkit Telelogic Tau to develop our formal model. From the SDL specification, an extended finite-state machine (EFSM) description can be generated automatically to configure the protocol-verifier, which then checks observed data traffic. Based on the theory of protocolengineering and comprehension of the protocol, this paper accomplishes the protocol formal specification, simulation, validation and test in software environment. Through simulation and validation to find out and correct the errors of protocol system, by this way the speed of development can be quickened and the quality of protocol software can be well ensured furthest. At last, the conclusion and prospect are developed.