On Formal Analysis of Cryptographic Protocolsand Supporting Tool
-
Graphical Abstract
-
Abstract
Cryptographic protocols are crucial for se-
cure communications and networks, distribution systems
and electronic commerce. Model checking technique and
supporting tool for analyzing cryptographic protocols are
discussed. A model checking technique based on logic of
algorithm knowledge for cryptographic protocols is pro-
posed, which can specify explicitly the intruder model ca-
pabilities. The knowledge completeness of intruder abili-
ties is proved. An e±cient veri¯cation model generating
system is developed based on PDL (Protocols description
language) and SPIN/Promela for cryptographic protocols.
Some optimization strategies are implemented in the sys-
tem to reduce the state explosion complexity, such as par-
tial order reduction, syntactic reorder and static analysis.
More than ten cryptographic protocols are analyzed and
published °aws are rediscovered successfully with the sys-
tem. The veri¯cation system can be used as an e±cient
and reliable tool for evaluation of the network security.
-
-
DownLoad: