XIAO Meihua, JIANG Yun and LIU Qiaowei. On Formal Analysis of Cryptographic Protocolsand Supporting Tool[J]. Chinese Journal of Electronics, 2010, 19(2): 223-228.
Citation: XIAO Meihua, JIANG Yun and LIU Qiaowei. On Formal Analysis of Cryptographic Protocolsand Supporting Tool[J]. Chinese Journal of Electronics, 2010, 19(2): 223-228.

On Formal Analysis of Cryptographic Protocolsand Supporting Tool

  • Received Date: 2008-06-28
  • Rev Recd Date: 2009-10-08
  • Publish Date: 2010-04-05
  • 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.
  • loading
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (861) PDF downloads(1271) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return