Security Verification of Real-Time Cryptographic Protocols Using a Rewriting Approach
スポンサーリンク
概要
- 論文の詳細を見る
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.
- 社団法人電子情報通信学会の論文
- 1998-04-25
著者
-
Watanabe Hajime
The First Department of Internal Medicine, Tohoku University School of Medicine
-
Kasami Tadao
The Faculty Of Nara Institute Of Science And Technology
-
Tanaka T
Nara Inst. Sci. And Technol. Nara Jpn
-
TANAKA Takehiko
the Faculty of Nara Institute of Science and Technology
-
KAJI Yuichi
the Faculty of Nara Institute of Science and Technology
-
TAKATA Toyoo
the Faculty of Nara Institute of Science and Technology
-
Watanabe Hajime
The Faculty Of Nara Institute Of Science And Technology
関連論文
- EFFECTS OF AORTIC INPUT IMPEDANCE ON LEFT VENTRICULAR END-EJECTION PRESSURE-VOLUME RELATIONSHIP : PROCEEDINGS OF THE 47th ANNUAL SCIENTIFIC MEETING OF THE JAPANESE CIRCULATION SOCIETY : Ventricular Function (I)
- A System for Deciding the Security of Cryptographic Protocols (Special Section on Cryptography and Information Security)
- Security Verification of Real-Time Cryptographic Protocols Using a Rewriting Approach
- The Universal Recognition Problems for Multiple Context-Free Grammars and for Linear Context-Free Rewriting Systems
- Selection Method of Test Patterns in Soft-Decision Iterative Bounded Distance Decoding Algorithms(Coding Theory)(Information Theory and Its Applications)