Specification and Verification of Cryptographic Protocols based on TCPL

被引：0

作者：

Lei Xinfeng ^{[1
]}

Li Xinghua ^{[1
]}

Liu Jun ^{[1
]}

Xiao Junmo ^{[1
]}

机构：

[1] PLA Univ Sci & Technol, Inst Commun Engn, Nanjing 210007, Jiangsu Prov, Peoples R China

来源：

ICCSSE 2009: PROCEEDINGS OF 2009 4TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE & EDUCATION | 2009年

关键词：

cryptographic protocol; specification; verification; LOGIC;

D O I：

10.1109/ICCSE.2009.5228468

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

To facilitate the analysis of cryptographic protocols, based on time-dependent cryptographic protocol logic (TCPL), a method to specify logic formulas in XML is given. And then, a method to automatically verify cryptographic protocol is provided. In this method, the goals of the protocol are reduced to a set of sub-goals, and continually using the similar reduction on these sub-goals will at last lead to some given conditions. Thus, the validness of the given conditions will make the goals valid. Proof shows that our method is sound. Moreover, it can make the process to analyze cryptographic protocols automated and efficient.

引用

页码：1216 / 1220

页数：5

共 8 条

[1] A LOGIC OF AUTHENTICATION
BURROWS, M
ABADI, M
NEEDHAM, RM
[J]. PROCEEDINGS OF THE ROYAL SOCIETY OF LONDON SERIES A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 1989, 426 (1871): : 233 - 271
[2] Logic for verifying public-key cryptographic protocols
Coffey, T
Saidha, P
[J]. IEE PROCEEDINGS-COMPUTERS AND DIGITAL TECHNIQUES, 1997, 144 (01): : 28 - 32
[3] Dojen R., 2005, ACM Transactions on Information and Systems Security, V8, P287, DOI 10.1145/1085126.1085128
[4] ELTON S, 2001, FACILITATING MODELLI
[5] Gong L., 1990, Proceedings. 1990 IEEE Computer Society Symposium on Research in Security and Privacy (Cat. No.90CH2884-5), P234, DOI 10.1109/RISP.1990.63854
[6] LEI XF, 2007, 2 INT C COMP SCI ED, P853
[7] A Logic to Model Time in Cryptographic Protocols
Lei Xinfeng
Liu Jun
Xiao Jumno
[J]. ISCSCT 2008: INTERNATIONAL SYMPOSIUM ON COMPUTER SCIENCE AND COMPUTATIONAL TECHNOLOGY, VOL 1, PROCEEDINGS, 2008, : 399 - 403
[8] WANG YY, 2001, MODERN LOGIC COMPUTE

← 1 →