Security Verification of Real-Time Cryptographic Protocols Using a Rewriting Approach

Takehiko TANAKA  Yuichi KAJI  Hajime WATANABE  Toyoo TAKATA  Tadao KASAMI  

IEICE TRANSACTIONS on Information and Systems   Vol.E81-D   No.4   pp.355-363
Publication Date: 1998/04/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software Theory
security verification,  cryptographic protocol,  timestamp,  conditional term rewriting system,   network security,  

Full Text: PDF(893KB)>>
Buy this Article

A computational model for security verification of cryptographic protocols is proposed. Until most recently, security verification of cryptographic protocols was left to the protocol designers' experience and heuristics. Though some formal verification methods have been proposed for this purpose, they are still insufficient for the verification of practical real-time cryptographic protocols. In this paper we propose a new formalism based on a term rewriting system approach that we have developed. In this model, what and when the saboteur can obtain is expressed by a first-order term of a special form, and time-related concepts such as the passage of time and the causality relation are specified by conditional term rewriting systems. By using our model, a cryptographic protocol which was shown to be secure by the BAN-logic is shown to be insecure.