Abstract: Formal analysis of security protocols is becoming more and more important. It is desiderated to expand the existing methods to study more security properties and to form a unified framework to analyze various security properties. Process calculus is a powerful tool for modeling concurrent systems. The existing process calculi, however, are not very convenient to support data structure. In this paper, a generic model is proposed for the analysis of security protocols based on a process calculus with knowledge derivation. The model facilitates the formal definitions of some well known security properties. Using this model the Needham-Schroeder public-key protocol is analyzed as a case study. Some future directions are pointed out.