For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 1998/04/25
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)>>
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.