eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-17
8
1
3
24
10.22042/isecure.2016.8.1.1
40676
A short introduction to two approaches in formal verification of security protocols: model checking and theorem proving
M. Pourpouneh
mpourpouneh@mehr.sharif.edu
1
R. Ramezanian
2
Department of Mathematical Science, Sharif University of Technology, Tehran, Iran
Department of Mathematical Science, Ferdowsi University of Mashhad, Mashhad, Iran
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 n 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.
https://www.isecure-journal.com/article_40676_b04f81eb888f84ee26045d193b349ee0.pdf
Cryptographic Protocols
Formal
Verification
Model Checking
Theorem Proving
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2015-12-15
8
1
25
38
10.22042/isecure.2016.8.1.2
40678
On the design and security of a lattice-based threshold secret sharing scheme
H. R. Amini Khorasgani
aminikhhr@gmail.com
1
S. Asaad
saba_asaad@ee.sharif.edu
2
H. Pilaram
h_pilaram@ee.sharif.edu
3
T. Eghlidos
teghlidos@gmail.com
4
M. R. Aref
isecure@sharif.ir
5
Information Systems and Security Lab (ISSL), Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran
Information Systems and Security Lab (ISSL), Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran
Information Systems and Security Lab (ISSL), Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran
Electronics Research Institute, Sharif University of Technology, Tehran, Iran
Information Systems and Security Lab (ISSL), Department of Electrical Engineering, Sharif University of Technology, Tehran, Iran
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.
https://www.isecure-journal.com/article_40678_f82f17612cd3e8ae7eb3461c69ae1da4.pdf
Threshold Secret Sharing Scheme
Closest Vector Problem
Lattice-based Cryptography
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-23
8
1
39
52
10.22042/isecure.2016.8.1.6
41105
Aggrandizing the beast's limbs: patulous code reuse attack on ARM architecture
F. Aminmansour
fr.aminmansour@aut.ac.ir
1
H. Shahriari
shahriari@aut.ac.ir
2
Department of Computer Engineering and Information Technology, Amirkabir University of Technology, Tehran, Iran
Department of Computer Engineering and Information Technology, Amirkabir University of Technology, Tehran, Iran
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.
https://www.isecure-journal.com/article_41105_1e1b8cb7048bbf028416256f2a21f211.pdf
Code Reuse Attack
ARM Architecture
Android
Return Oriented Programming
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-04
8
1
53
60
10.22042/isecure.2016.8.1.3
40685
Self authentication path insertion in FPGA-based design flow for tamper-resistant purpose
Sh. Zamanzadeh
s.zamanzadeh@gmail.com
1
A. Jahanian
jahanian@sbu.ac.ir
2
Computer Science and Engineering Department, Shahid Beheshti University, Tehran, Iran
Computer Science and Engineering Department, Shahid Beheshti University, Tehran, Iran
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.
https://www.isecure-journal.com/article_40685_1715613c63061e272ba7164900d92832.pdf
FPGA
Hardware Security, IP Protection, Security Path
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-31
8
1
61
71
10.22042/isecure.2016.8.1.4
40690
Unauthenticated event detection in wireless sensor networks using sensors co-coverage
M. Kamarei
1
A. Patooghy
2
M. Fazeli
3
University of Applied Science and Technology, Tehran, Iran
Department of Computer Engineering, Iran University of Science & Technology Tehran, Iran
Department of Computer Engineering, Iran University of Science and Technology Tehran, Iran
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.
https://www.isecure-journal.com/article_40690_3cadb400a7a8230cc8d8ece46daf6336.pdf
Attack
Wireless Sensor Networks, the More the Safe, the Less the Unsafe Policy, Unauthenticated Events
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-04
8
1
73
84
10.22042/isecure.2016.8.1.5
40692
A new method for accelerating impossible differential cryptanalysis and its application on LBlock
A. Khalesi
khalesiakram@yahoo.com
1
H. Bahramgiri
bahramgiri@mut.ac.ir
2
D. Mansuri
davodmansuri@mut.ac.ir
3
Department of Information and Communication Technology, Malek-e-Ashtar University of Technology, Tehran, Iran
Institute of Research on Information and Communication Security (IRICS), Malek-e-Ashtar University of Technology, Tehran, Iran
Institute of Research on Information and Communication Security (IRICS), Malek-e-Ashtar University of Technology, Tehran, Iran
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 2 73 blocks of memory.
https://www.isecure-journal.com/article_40692_f474c1dd8dc2c510d0cc70641b88b834.pdf
Differential Cryptanalysis
Impossible Differential Cryptanalysis
LBlock
eng
Iranian Society of Cryptology
The ISC International Journal of Information Security
2008-2045
2008-3076
2016-01-31
8
1
85
90
10.22042/isecure.2016.8.1.8
45390
Persian Abstract
Persian abstracts of the issue's article
https://www.isecure-journal.com/article_45390_1ebefb3a042397df79e7105d1812a908.pdf
No Keywords