Volume 3, Issue 1 (2003)                   MJEE 2003, 3(1): 11-29 | Back to browse issues page

XML Persian Abstract Print


Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:

Jalili S, TORK LADANI B. A MODEL FOR SPECIFICATION OF CRYPTOGRAPHIC PROTOCOLS AND ITS OPERATIONAL INTERPRETATION WITH ALGEBRAIC METHODS. MJEE. 3 (1) :11-29
URL: http://mjee.modares.ac.ir/article-17-11508-en.html
1- Tarbiat Modarres University
Abstract:   (2999 Views)
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.
Full-Text [PDF 2427 kb]   (1693 Downloads)    

Received: 2002/03/2 | Accepted: 2003/09/2 | Published: 2003/12/2

Add your comments about this article : Your username or Email:
CAPTCHA