Cryptographic protocol security analysis based on bounded constructing algorithm

An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message concurrent. We propose an efficient structures are complex and their executions are automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra （CPA） model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.

WIDE:A witness-based data priority mechanism for vehicular forensics

In this paper,we present a WItness based Data priority mEchanism(WIDE)for vehicles in the vicinity of an accident to facilitate liability decisions.WIDE evaluates the integrity of data generated by these vehicles,called witnesses,in the event of an accident to assure the reliability of data to be used for making liability decisions and ensure that such data are received from credible witnesses.To achieve this,WIDE introduces a two-level integrity assessment to achieve end-to-end integrity by initially ascertaining the integrity of data-producing sensors,and validating that data generated have not been altered on transit by compromised road-side units(RSUs)by executing a practical byzantine fault tolerance(pBFT)protocol to reach consensus on data reliability.Furthermore,WIDE utilises a blockchain based reputation management system(BRMS)to ensure that only data from highly reputable witnesses are utilised as contributing evidence for facilitating liability decisions.Finally,we formally verify the proposed framework against data integrity requirements using the Automated Verification of Internet Security Protocols and Applications(AVISPA)with High-Level Protocol Specification Language(HLPSL).Qualitative arguments show that our proposed framework is secured against identified security attacks and assures the reliability of data utilised for making liability decisions,while quantitative evaluations demonstrate that our proposal is practical for fully autonomous vehicle forensics.