Petri net based models for specification and analysis of cryptographic protocols

Formal specification and analysis of cryptographic protocols play an important role in evaluating cryptosystems. Thus, an efficient specification and analysis model for the protocols is strongly required. In this paper, we review the previous specification and analysis models of protocols and propos...

Full description

Saved in:
Bibliographic Details
Published in:The Journal of systems and software 1997-05, Vol.37 (2), p.141-159
Main Authors: Lee, Gang-Soo, Lee, Jin-Seok
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Cryptography
Exact sciences and technology
Memory and file management (including protection and security)
Memory organisation. Data processing
Protocol
Software
Studies
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal specification and analysis of cryptographic protocols play an important role in evaluating cryptosystems. Thus, an efficient specification and analysis model for the protocols is strongly required. In this paper, we review the previous specification and analysis models of protocols and propose new Petri net based model, which is called CTPN (Cryptographic Timed Petri Net). Also, we suggest a new specification and analysis methodology for the protocols based on our proposed model. We define a CTPN-language for a CTPN-analyzer. A CTPN-analyzer is also developed for the systematic analysis of a protocol. Our CTPN model including CTPN-analyzer is found to have executable, formal, graphical textual, and consistent characteristics suitable for the specification and analysis of cryptographic protocols.
ISSN:0164-1212
1873-1228
DOI:10.1016/S0164-1212(96)00112-4