THE ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY
Year:2016 | Volume:8 | Issue:1 |Papers Count:7

Welcome to the first issue of the eighth volume of the journal. In this issue, we publish six regular papers as well as a single page per paper incorporating the translation of the title and abstract in Persian, to be used by Persian indexing centers.Our invited authors in the first paper of this issue review two formal approaches in verification of security protocols; model checking and theorem proving. In this paper, Scyther operational semantics is explained as a model checking approach, and some of the famous security protocols are modelled and verified using this method. Moreover, the notion \Glass Pipe" is discussed to describe the meaning of authentication, and a deduction system is provided to formally define the notion. Finally, using this deduction system, some of famous protocols are verified, and the results are compared with the results of Scyther model checker...

In this paper, we shortly review two formal approaches in verification of security protocols; model checking and theorem proving. Model checking is based on studying the behavior of protocols via generating all different behaviors of a protocol and checking whether the desired goals are satisfied in all instances or not. We investigate Scyther operational semantics as an example of this approach and then we model and verify some famous security protocols using Scyther. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named Simple Logic for Authentication to formally define the notion of authenticated communication based on the structure of the messages, and then we several famous protocols using our proposed deduction system and compare it with the verification results of Scyther model checking.

In this paper, we introduce a method of threshold secret sharing scheme (TSSS) in which secret reconstruction is based on Babai's nearest plane algorithm. In order to supply secure public channels for transmitting shares to parties, we need to ensure that there are no quantum threats to these channels. A solution to this problem can be utilization of lattice-based cryptosystems for these channels which requires designing lattice-based TSSSs. We investigate the effect of lattice dimension on the security and correctness of the proposed scheme. Moreover, we prove that for a fixed lattice dimension the proposed scheme is asymptotically correct. We also give a quantitative proof of security from information theoretic viewpoint.

Since smartphones are usually personal devices full of private information, they are a popular target for a vast variety of real-world attacks such as Code Reuse Attack (CRA). CRAs enable attackers to execute any arbitrary algorithm on a device without injecting an executable code. Since the standard platform for mobile devices is ARM architecture, we concentrate on available ARM-based CRAs. Currently, three types of CRAs are proposed on ARM architecture including Return2ZP, ROP, and BLX-attack in accordance to three sub-models available on X86. Ret2Libc, ROP, and JOP. In this paper, we have considered some unique aspects of ARM architecture to provide a general model for code reuse attacks called Patulous Code Reuse Attack (PCRA). Our attack applies all available machine instructions that change Program Counter (PC) as well as direct or indirect branches in order to deploy the principles of CRA convention. We have demonstrated the effectiveness of our approach by defining five different sub-models of PCRA, explaining the algorithm of finding PCRA gadgets, introducing a useful set of gadgets, and providing a sample proof of concept exploit on Android 4.4 platform.

FPGA platforms have been widely used in many modern digital applications due to their low prototyping cost, short time-to-market and flexibility. Field-programmability of FPGA bitstream has made it as a flexible and easy-to-use platform. However, access to bitstream degraded the security of FPGA IPs because there is no efficient method to authenticate the originality of bitstream by the FPGA programmer. The issue of secure transmission of configuration information to the FPGAs is of paramount importance to both users and IP providers. In this paper we presented a "Self Authentication" methodology in which the originality of sub-components in bitstream is authenticated in parallel with the intrinsic operation of the design. In the case of discovering violation, the normal data flow is obfuscated and the circuit would be locked. Experimental results show that this methodology considerably improves the IP security against malicious updates with reasonable overheads.

Wireless Sensor Networks (WSNs) offer inherent packet redundancy since each point within the network area is covered by more than one sensor node. This phenomenon, which is known as sensors co-coverage, is used in this paper to detect unauthenticated events. Unauthenticated event broadcasting in a WSN imposes network congestion, worsens the packet loss rate, and increases the network energy congestion. In the proposed method, the more the safe, the less the unsafe (MSLU) method, each secure occurred event must be confirmed by various sensor nodes; otherwise the event is dropped. Indeed, the proposed method tends to forward event occurrence reports that are detected by various sensor nodes. The proposed method is evaluated by means of simulation as well as analytical modeling. A wide range of simulations, which are carried out using NS-2, show that the proposed method detects more than 85% of unauthenticated events. This comes at the cost of the network end-to-end delay of 20% because the proposed method does not impose delay on incoming packets. In addition, the proposed method is evaluated by means of an analytical model based on queuing networks. The model accurately estimates the network performance utilizing the proposed unauthenticated event detection method.

Impossible differential cryptanalysis, the extension of differential cryptanalysis, is one of the most efficient attacks against block ciphers. This cryptanalysis method has been applied to most of the block ciphers and has shown significant results. Using structures, key schedule considerations, early abort, and pre-computation are some common methods to reduce complexities of this attack. In this paper, we present a new method for decreasing the time complexity of impossible differential cryptanalysis through breaking down the target key space into subspaces, and extending the results on subspaces to the main target key space. The main advantage of this method is that there is no need to consider the effects of changes in the values of independent key bits on each other. Using the 14-round impossible differential characteristic observed by Boura et al. at ASIACRYPT 2014, we implement this method on 23-round LBlock and demonstrate that it can reduce the time complexity of the previous attacks to 271.8 23-round encryptions using 259 chosen plaintexts and 273 blocks of memory.