Formal Analysis of Security Protocol Based on Process Calculus and Knowledge Derivation

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.