A MODEL FOR SPECIFICATION OF CRYPTOGRAPHIC PROTOCOLS AND ITS OPERATIONAL INTERPRETATION WITH ALGEBRAIC METHODS

Logic analysis and attack construction methods are two major approaches in verification of cryptographic protocols. However, it is almost preferable to use both of them for a complete analysis. In this paper, a generic framework for the integration of the two verification approaches is presented. Using the framework we can propose analysis methods in which security properties and breach scenarios of the properties in a protocol can be verified in a unified manner. The focus on this paper is on a computational model of the protocols as the major component of the framework. The operational interpretation of the computational model with a term rewriting system (TRS) is presented too. To specify an intended protocol, we can represent it as a set of individual steps, and then using a transformation algorithm, a terminated and confluent TRS is generated automatically. This TRS is used to construct a special representation of the protocol named the protocol execution path, which can be used as the base of various verification schemes. Specification and verification of a sample protocol is presented too.

کلیدواژه ها:

Cryptographic protocols ، Formal verification ، Computational model ، Logical analysis ، Attack construction ، Term rewriting systems ، پروتکل های رمزنگاری ، وارسی صوری پروتکل های رمزنگاری ، مدل محاسباتی پروتکل ، تحلیل منطقی