A Comparative Analysis of Tools for Verification of Security Protocols

The area of formal verification of protocols has gained substantial importance in the recent years. The research results and subsequent applications have amply demonstrated that the formal verification tools have indeed helped correct the protocols even after being standardized. However, the standard protocol verification tools and techniques do not verify the security properties of a cryptographic protocol. This has resulted in the emergence of the security protocol verifiers to fill the need. In this paper, taking the two popular security verification tools namely Scyther and ProVerif as the basis, we identify a few security protocols and implement them in both Scyther and ProVerif, to aptly evaluate the tools, in terms of the security properties of the selected protocols. In the process, we not only characteristically present a comparative evaluation of the two tools, but also reveal interesting security properties of the protocols selected, showing their strengths and weaknesses. To the best of our knowledge, this is a unique attempt to juxtapose and evaluate the two verification tools using the selected security protocols.

Simple index based symmetric searchable encryption with result verifiability

1 Introduction and main contributions Searchable encryption(SE)allows client(data user)to outsource searchable ciphertexts onto server in a way that the data can further be searched by server.For semi-honest-but-curios server(that follows the protocol but curious to learn the plaintext of client's data),data privacy while performing search is of primary concern.However,in case of malicious server(that follows the protocol but may alter the result),besides data privacy,the other design rational,i.e.,verifiable searchability is required.In verifiable searchability,server has to prove client that the retured search result is correct and complete.

Privacy preserving secure expansive aggregation with malicious node identification in linear wireless sensor networks

The Wireless Sensor Networks(WSNs)used for the monitoring applications like pipelines carrying oil,water,and gas;perimeter surveillance;border monitoring;and subway tunnel monitoring form linearWSNs.Here,the infrastructure being monitored inherently forms linearity(straight line through the placement of sensor nodes).Therefore,suchWSNs are called linear WSNs.These applications are security critical because the data being communicated can be used for malicious purposes.The contemporary research of WSNs data security cannot fit in directly to linear WSN as only by capturing few nodes,the adversary can disrupt the entire service of linear WSN.Therefore,we propose a data aggregation scheme that takes care of privacy,confidentiality,and integrity of data.In addition,the scheme is resilient against node capture attack and collusion attacks.There are several schemes detecting the malicious nodes.However,the proposed scheme also provides an identification of malicious nodes with lesser key storage requirements.Moreover,we provide an analysis of communication cost regarding the number of messages being communicated.To the best of our knowledge,the proposed data aggregation scheme is the first lightweight scheme that achieves privacy and verification of data,resistance against node capture and collusion attacks,and malicious node identification in linear WSNs.