Visible to the public Biblio

Found 116 results

Filters: Keyword is Resistance  [Clear All Filters]
2021-08-03
Zhang, Yan, Li, Bing, Wang, Yazhou, Wu, Jiaxin, Yuan, Pengwei.  2020.  A Blockchain-based User Remote Autentication Scheme in IoT Systems Using Physical Unclonable Functions. 2020 IEEE 5th International Conference on Signal and Image Processing (ICSIP). :1100—1105.
Achieving efficient and secure accesses to real-time information from the designated IoT node is the fundamental key requirement for the applications of the Internet of Things. However, IoT nodes are prone to physical attacks, public channels reveal the sensitive information, and gateways that manage the IoT nodes suffer from the single-point failure, thereby causing the security and privacy problems. In this paper, a blockchain-based user remote authentication scheme using physical unclonable functions (PUFs) is proposed to overcome these problems. The PUFs provide physically secure identities for the IoT nodes and the blockchain acts as a distributed database to manage the key materials reliably for gateways. The security analysis is conducted and shows that our scheme realizes reliable security features and resists various attacks. Furthermore, a prototype was implemented to prove our scheme is efficient, scalable, and suitable for IoT scenarios.
2021-07-08
Alamsyah, Zaenal, Mantoro, Teddy, Adityawarman, Umar, Ayu, Media Anugerah.  2020.  Combination RSA with One Time Pad for Enhanced Scheme of Two-Factor Authentication. 2020 6th International Conference on Computing Engineering and Design (ICCED). :1—5.
RSA is a popular asymmetric key algorithm with two keys scheme, a public key for encryption and private key for decryption. RSA has weaknesses in encryption and decryption of data, including slow in the process of encryption and decryption because it uses a lot of number generation. The reason is RSA algorithm can work well and is resistant to attacks such as brute force and statistical attacks. in this paper, it aims to strengthen the scheme by combining RSA with the One Time Pad algorithm so that it will bring up a new design to be used to enhance security on two-factor authentication. Contribution in this paper is to find a new scheme algorithm for an enhanced scheme of RSA. One Time Pad and RSA can combine as well.
Long, Vu Duc, Duong, Ta Nguyen Binh.  2020.  Group Instance: Flexible Co-Location Resistant Virtual Machine Placement in IaaS Clouds. 2020 IEEE 29th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). :64—69.
This paper proposes and analyzes a new virtual machine (VM) placement technique called Group Instance to deal with co-location attacks in public Infrastructure-as-a-Service (IaaS) clouds. Specifically, Group Instance organizes cloud users into groups with pre-determined sizes set by the cloud provider. Our empirical results obtained via experiments with real-world data sets containing million of VM requests have demonstrated the effectiveness of the new technique. In particular, the advantages of Group Instance are three-fold: 1) it is simple and highly configurable to suit the financial and security needs of cloud providers, 2) it produces better or at least similar performance compared to more complicated, state-of-the-art algorithms in terms of resource utilization and co-location security, and 3) it does not require any modifications to the underlying infrastructures of existing public cloud services.
2021-06-30
Chen, Jichang, Lu, Zhixiang, Zhu, Xueping.  2020.  A Lightweight Dual Authentication Protocol for the Internet of Vehicles. 2020 IEEE 3rd International Conference on Information Systems and Computer Aided Education (ICISCAE). :17—22.
With the development of 5G communication technology, the status of the Internet of Vehicles in people's lives is greatly improved in the general trend of intelligent transportation. The combination of vehicles and Radio Frequency Identification (RFID) makes the application prospects of vehicle networking gradually expand. However, the wireless network of the Internet of Vehicles is open and mobile, so it can be easily stolen or tampered with by attackers. Moreover, it will cause serious traffic security problems and even threat people's lives. In this paper, we propose a lightweight authentication protocol for the Internet of Vehicles based on a mobile RFID system and give corresponding security requirements for modeling potential attacks. The protocol is based on the three-party mutual authentication, and uses bit-operated left-cycle shift operations and hetero-oriented operations to generate encrypted data. The simultaneous inclusion of triparty shared key information and random numbers makes the protocol resistant to counterfeit attacks, violent attacks, replay attacks and desynchronization attacks. Finally, a simulation analysis of the security protocol using the ProVerif tool shows that the protocol secures is not accessible to attackers during the data transfer, and achieve the three-party authentication between sensor nodes (SN), vehicle nodes (Veh) and backend servers.
2021-02-23
Fan, W., Chang, S.-Y., Emery, S., Zhou, X..  2020.  Blockchain-based Distributed Banking for Permissioned and Accountable Financial Transaction Processing. 2020 29th International Conference on Computer Communications and Networks (ICCCN). :1—9.

Distributed banking platforms and services forgo centralized banks to process financial transactions. For example, M-Pesa provides distributed banking service in the developing regions so that the people without a bank account can deposit, withdraw, or transfer money. The current distributed banking systems lack the transparency in monitoring and tracking of distributed banking transactions and thus do not support auditing of distributed banking transactions for accountability. To address this issue, this paper proposes a blockchain-based distributed banking (BDB) scheme, which uses blockchain technology to leverage its built-in properties to record and track immutable transactions. BDB supports distributed financial transaction processing but is significantly different from cryptocurrencies in its design properties, simplicity, and computational efficiency. We implement a prototype of BDB using smart contract and conduct experiments to show BDB's effectiveness and performance. We further compare our prototype with the Ethereum cryptocurrency to highlight the fundamental differences and demonstrate the BDB's superior computational efficiency.

2021-01-18
Sun, J., Ma, J., Quan, J., Zhu, X., I, C..  2019.  A Fuzzy String Matching Scheme Resistant to Statistical Attack. 2019 International Conference on Networking and Network Applications (NaNA). :396–402.
The fuzzy query scheme based on vector index uses Bloom filter to construct vector index for key words. Then the statistical attack based on the deviation of frequency distribution of the vector index brings out the sensitive information disclosure. Using the noise vector, a fuzzy query scheme resistant to the statistical attack serving for encrypted database, i.e. S-BF, is introduced. With the noise vector to clear up the deviation of frequency distribution of vector index, the statistical attacks to the vector index are resolved. Demonstrated by lab experiment, S-BF scheme can achieve the secure fuzzy query with the powerful privation protection capability for encrypted cloud database without the loss of fuzzy query efficiency.
2020-12-14
Pilet, A. B., Frey, D., Taïani, F..  2020.  Foiling Sybils with HAPS in Permissionless Systems: An Address-based Peer Sampling Service. 2020 IEEE Symposium on Computers and Communications (ISCC). :1–6.
Blockchains and distributed ledgers have brought renewed interest in Byzantine fault-tolerant protocols and decentralized systems, two domains studied for several decades. Recent promising works have in particular proposed to use epidemic protocols to overcome the limitations of popular Blockchain mechanisms, such as proof-of-stake or proof-of-work. These works unfortunately assume a perfect peer-sampling service, immune to malicious attacks, a property that is difficult and costly to achieve. We revisit this fundamental problem in this paper, and propose a novel Byzantine-tolerant peer-sampling service that is resilient to Sybil attacks in open systems by exploiting the underlying structure of wide-area networks.
2020-11-23
Kumari, K. A., Sadasivam, G. S., Gowri, S. S., Akash, S. A., Radhika, E. G..  2018.  An Approach for End-to-End (E2E) Security of 5G Applications. 2018 IEEE 4th International Conference on Big Data Security on Cloud (BigDataSecurity), IEEE International Conference on High Performance and Smart Computing, (HPSC) and IEEE International Conference on Intelligent Data and Security (IDS). :133–138.
As 5G transitions from an industrial vision to a tangible, next-generation mobile technology, security remains key business driver. Heterogeneous environment, new networking paradigms and novel use cases makes 5G vulnerable to new security threats. This in turn necessitates a flexible and dependable security mechanism. End-to-End (E2E) data protection provides better security, avoids repeated security operations like encryption/decryption and provides differentiated security based on the services. E2E security deals with authentication, integrity, key management and confidentiality. The attack surface of a 5G system is larger as 5G aims for a heterogeneous networked society. Hence attack resistance needs to be a design consideration when defining new 5G protocols. This framework has been designed for accessing the manifold applications with high security and trust by offering E2E security for various services. The proposed framework is evaluated based on computation complexity, communication complexity, attack resistance rate and security defensive rate. The protocol is also evaluated for correctness, and resistance against passive, active and dictionary attacks using random oracle model and Automated Validation of Internet Security Protocols and Applications (AVISPA) tool.
2020-11-02
Zhang, Yuan, Xu, Chunxiang, Li, Hongwei, Yang, Haomiao, Shen, Xuemin.  2019.  Chronos: Secure and Accurate Time-Stamping Scheme for Digital Files via Blockchain. ICC 2019 - 2019 IEEE International Conference on Communications (ICC). :1—6.

It is common to certify when a file was created in digital investigations, e.g., determining first inventors for patentable ideas in intellectual property systems to resolve disputes. Secure time-stamping schemes can be derived from blockchain-based storage to protect files from backdating/forward-dating, where a file is integrated into a transaction on a blockchain and the timestamp of the corresponding block reflects the latest time the file was created. Nevertheless, blocks' timestamps in blockchains suffer from time errors, which causes the inaccuracy of files' timestamps. In this paper, we propose an accurate blockchain-based time-stamping scheme called Chronos. In Chronos, when a file is created, the file and a sufficient number of successive blocks that are latest confirmed on blockchain are integrated into a transaction. Due to chain quality, it is computationally infeasible to pre-compute these blocks. The time when the last block was chained to the blockchain serves as the earliest creation time of the file. The time when the block including the transaction was chained indicates the latest creation time of the file. Therefore, Chronos makes the file's creation time corresponding to this time interval. Based on chain growth, Chronos derives the time when these two blocks were chained from their heights on the blockchain, which ensures the accuracy of the file's timestamp. The security and performance of Chronos are demonstrated by a comprehensive evaluation.

2020-10-06
Drozd, Oleksandr, Kharchenko, Vyacheslav, Rucinski, Andrzej, Kochanski, Thaddeus, Garbos, Raymond, Maevsky, Dmitry.  2019.  Development of Models in Resilient Computing. 2019 10th International Conference on Dependable Systems, Services and Technologies (DESSERT). :1—6.

The article analyzes the concept of "Resilience" in relation to the development of computing. The strategy for reacting to perturbations in this process can be based either on "harsh Resistance" or "smarter Elasticity." Our "Models" are descriptive in defining the path of evolutionary development as structuring under the perturbations of the natural order and enable the analysis of the relationship among models, structures and factors of evolution. Among those, two features are critical: parallelism and "fuzziness", which to a large extent determine the rate of change of computing development, especially in critical applications. Both reversible and irreversible development processes related to elastic and resistant methods of problem solving are discussed. The sources of perturbations are located in vicinity of the resource boundaries, related to growing problem size with progress combined with the lack of computational "checkability" of resources i.e. data with inadequate models, methodologies and means. As a case study, the problem of hidden faults caused by the growth, the deficit of resources, and the checkability of digital circuits in critical applications is analyzed.

2020-09-11
Azakami, Tomoka, Shibata, Chihiro, Uda, Ryuya, Kinoshita, Toshiyuki.  2019.  Creation of Adversarial Examples with Keeping High Visual Performance. 2019 IEEE 2nd International Conference on Information and Computer Technologies (ICICT). :52—56.
The accuracy of the image classification by the convolutional neural network is exceeding the ability of human being and contributes to various fields. However, the improvement of the image recognition technology gives a great blow to security system with an image such as CAPTCHA. In particular, since the character string CAPTCHA has already added distortion and noise in order not to be read by the computer, it becomes a problem that the human readability is lowered. Adversarial examples is a technique to produce an image letting an image classification by the machine learning be wrong intentionally. The best feature of this technique is that when human beings compare the original image with the adversarial examples, they cannot understand the difference on appearance. However, Adversarial examples that is created with conventional FGSM cannot completely misclassify strong nonlinear networks like CNN. Osadchy et al. have researched to apply this adversarial examples to CAPTCHA and attempted to let CNN misclassify them. However, they could not let CNN misclassify character images. In this research, we propose a method to apply FGSM to the character string CAPTCHAs and to let CNN misclassified them.
2020-08-24
Gohil, Nikhil N., Vemuri, Ranga R..  2019.  Automated Synthesis of Differential Power Attack Resistant Integrated Circuits. 2019 IEEE National Aerospace and Electronics Conference (NAECON). :204–211.
Differential Power Analysis (DPA) attacks were shown to be effective in recovering the secret key information from a variety cryptographic systems. In response, several design methods, ranging from the cell level to the algorithmic level, have been proposed to defend against DPA attacks. Cell level solutions depend on DPA resistant cell designs which attempt to minimize power variance during transitions while minimizing area and power consumption. In this paper, we discuss how a differential circuit design style is incorporated into a COTS tool set, resulting in a fully automated synthesis system DPA resistant integrated circuits. Based on the Secure Differential Multiplexer Logic (SDMLp), this system can be used to synthesize complete cryptographic processors which provide strong defense against DPA while minimizing area and power overhead. We discuss how both combinational and sequential cells are incorporated in the cell library. We show the effectiveness of the tool chain by using it to automatically synthesize the layouts, from RT level Verilog specifications, of both the DES and AES encryption ICs in 90nm CMOS. In each case, we present experimental data to demonstrate DPA attack resistance and area, power and performance overhead and compare these with circuits synthesized in another differential logic called MDPL as well as standard CMOS synthesis results.
2020-07-20
Komargodski, Ilan, Naor, Moni, Yogev, Eylon.  2017.  White-Box vs. Black-Box Complexity of Search Problems: Ramsey and Graph Property Testing. 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS). :622–632.
Ramsey theory assures us that in any graph there is a clique or independent set of a certain size, roughly logarithmic in the graph size. But how difficult is it to find the clique or independent set? If the graph is given explicitly, then it is possible to do so while examining a linear number of edges. If the graph is given by a black-box, where to figure out whether a certain edge exists the box should be queried, then a large number of queries must be issued. But what if one is given a program or circuit for computing the existence of an edge? This problem was raised by Buss and Goldberg and Papadimitriou in the context of TFNP, search problems with a guaranteed solution. We examine the relationship between black-box complexity and white-box complexity for search problems with guaranteed solution such as the above Ramsey problem. We show that under the assumption that collision resistant hash function exist (which follows from the hardness of problems such as factoring, discrete-log and learning with errors) the white-box Ramsey problem is hard and this is true even if one is looking for a much smaller clique or independent set than the theorem guarantees. In general, one cannot hope to translate all black-box hardness for TFNP into white-box hardness: we show this by adapting results concerning the random oracle methodology and the impossibility of instantiating it. Another model we consider is the succinct black-box, where there is a known upper bound on the size of the black-box (but no limit on the computation time). In this case we show that for all TFNP problems there is an upper bound on the number of queries proportional to the description size of the box times the solution size. On the other hand, for promise problems this is not the case. Finally, we consider the complexity of graph property testing in the white-box model. We show a property which is hard to test even when one is given the program for computing the graph. The hard property is whether the graph is a two-source extractor.
Rumez, Marcel, Dürrwang, Jürgen, Brecht, Tim, Steinshorn, Timo, Neugebauer, Peter, Kriesten, Reiner, Sax, Eric.  2019.  CAN Radar: Sensing Physical Devices in CAN Networks based on Time Domain Reflectometry. 2019 IEEE Vehicular Networking Conference (VNC). :1–8.
The presence of security vulnerabilities in automotive networks has already been shown by various publications in recent years. Due to the specification of the Controller Area Network (CAN) as a broadcast medium without security mechanisms, attackers are able to read transmitted messages without being noticed and to inject malicious messages. In order to detect potential attackers within a network or software system as early as possible, Intrusion Detection Systems (IDSs) are prevalent. Many approaches for vehicles are based on techniques which are able to detect deviations from specified CAN network behaviour regarding protocol or payload properties. However, it is challenging to detect attackers who secretly connect to CAN networks and do not actively participate in bus traffic. In this paper, we present an approach that is capable of successfully detecting unknown CAN devices and determining the distance (cable length) between the attacker device and our sensing unit based on Time Domain Reflectometry (TDR) technique. We evaluated our approach on a real vehicle network.
2020-06-19
Gu, Chongyan, Chang, Chip Hong, Liu, Weiqiang, Yu, Shichao, Ma, Qingqing, O'Neill, Maire.  2019.  A Modeling Attack Resistant Deception Technique for Securing PUF based Authentication. 2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). :1—6.

Due to practical constraints in preventing phishing through public network or insecure communication channels, simple physical unclonable function (PDF)-based authentication protocol with unrestricted queries and transparent responses is vulnerable to modeling and replay attacks. In this paper, we present a PUF-based authentication method to mitigate the practical limitations in applications where a resource-rich server authenticates a device with no strong restriction imposed on the type of PUF designs or any additional protection on the binary channel used for the authentication. Our scheme uses an active deception protocol to prevent machine learning (ML) attacks on a device. The monolithic system makes collection of challenge response pairs (CRPs) easy for model building during enrollment but prohibitively time consuming upon device deployment. A genuine server can perform a mutual authentication with the device at any time with a combined fresh challenge contributed by both the server and the device. The message exchanged in clear does not expose the authentic CRPs. The false PUF multiplexing is fortified against prediction of waiting time by doubling the time penalty for every unsuccessful authentication.

2020-06-08
Rajeshwaran, Kartik, Anil Kumar, Kakelli.  2019.  Cellular Automata Based Hashing Algorithm (CABHA) for Strong Cryptographic Hash Function. 2019 IEEE International Conference on Electrical, Computer and Communication Technologies (ICECCT). :1–6.
Cryptographic hash functions play a crucial role in information security. Cryptographic hash functions are used in various cryptographic applications to verify the message authenticity and integrity. In this paper we propose a Cellular Automata Based Hashing Algorithm (CABHA) for generating strong cryptographic hash function. The proposed CABHA algorithm uses the cellular automata rules and a custom transformation function to create a strong hash from an input message and a key.
2020-04-24
Overgaard, Jacob E. F., Hertel, Jens Christian, Pejtersen, Jens, Knott, Arnold.  2018.  Application Specific Integrated Gate-Drive Circuit for Driving Self-Oscillating Gallium Nitride Logic-Level Power Transistors. 2018 IEEE Nordic Circuits and Systems Conference (NORCAS): NORCHIP and International Symposium of System-on-Chip (SoC). :1—6.
Wide bandgap power semiconductors are key enablers for increasing the power density of switch-mode power supplies. However, they require new gate drive technologies. This paper examines and characterizes a fabricated gate-driver in a class-E resonant inverter. The gate-driver's total area of 1.2mm2 includes two high-voltage transistors for gate-driving, integrated complementary metal-oxide-semiconductor (CMOS) gate-drivers, high-speed floating level-shifter and reset circuitry. A prototype printed circuit board (PCB) was designed to assess the implications of an electrostatic discharge (ESD) diode, its parasitic capacitance and package bondwire connections. The parasitic capacitance was estimated using its discharge time from an initial voltage and the capacitance is 56.7 pF. Both bondwires and the diode's parasitic capacitance is neglegible. The gate-driver's functional behaviour is validated using a parallel LC resonant tank resembling a self-oscillating gate-drive. Measurements and simulations show the ESD diode clamps the output voltage to a minimum of -2V.
Balijabudda, Venkata Sreekanth, Thapar, Dhruv, Santikellur, Pranesh, Chakraborty, Rajat Subhra, Chakrabarti, Indrajit.  2019.  Design of a Chaotic Oscillator based Model Building Attack Resistant Arbiter PUF. 2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). :1—6.

Physical Unclonable Functions (PUFs) are vulnerable to various modelling attacks. The chaotic behaviour of oscillating systems can be leveraged to improve their security against these attacks. We have integrated an Arbiter PUF implemented on a FPGA with Chua's oscillator circuit to obtain robust final responses. These responses are tested against conventional Machine Learning and Deep Learning attacks for verifying security of the design. It has been found that such a design is robust with prediction accuracy of nearly 50%. Moreover, the quality of the PUF architecture is evaluated for uniformity and uniqueness metrics and Monte Carlo analysis at varying temperatures is performed for determining reliability.

2020-04-17
Wang, Congli, Lin, Jingqiang, Li, Bingyu, Li, Qi, Wang, Qiongxiao, Zhang, Xiaokun.  2019.  Analyzing the Browser Security Warnings on HTTPS Errors. ICC 2019 - 2019 IEEE International Conference on Communications (ICC). :1—6.
HTTPS provides authentication, data confidentiality, and integrity for secure web applications in the Internet. In order to establish secure connections with the target website but not a man-in-the-middle or impersonation attacker, a browser shows security warnings to users, when different HTTPS errors happen (e.g., it fails to build a valid certificate chain, or the certificate subject does not match the domain visited). Each browser implements its own design of warnings on HTTPS errors, to balance security and usability. This paper presents a list of common HTTPS errors, and we investigate the browser behaviors on each error. Our study discloses browser defects on handling HTTPS errors in terms of cryptographic algorithm, certificate verification, name validation, HPKP, and HSTS.
2020-04-03
Kuznetsov, Alexandr, Kiian, Anastasiia, Gorbenko, Yurii, Smirnov, Oleksii, Cherep, Oleksandr, Bexhter, Liliia.  2019.  Code-based Pseudorandom Generator for the Post-Quantum Period. 2019 IEEE International Conference on Advanced Trends in Information Theory (ATIT). :204—209.
This paper focuses on research of a provably secure code-based pseudorandom sequence generators whose cryptanalysis problem equals to syndrome decoding (belonging to the NP-complex class). It was found that generated sequences of such well-known Fischer-Stern code-based generator don’t have a maximum period, the actual period is much lower than expected. In our work, we have created a new generator scheme. It retains all advantages of the Fisher-Stern algorithm and provides pseudorandom sequences which are formed with maximum period. Also comparative analysis of proposed generator and popular generators was conducted.
2020-03-02
Babkin, Sergey, Epishkina, Anna.  2019.  Authentication Protocols Based on One-Time Passwords. 2019 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus). :1794–1798.
Nowadays one-time passwords are used in a lot of areas of information technologies including e-commerce. A few vulnerabilities in authentication protocols based on one-time passwords are widely known. In current work, we analyze authentication protocols based on one-time passwords and their vulnerabilities. Both simple and complicated protocols which are implementing cryptographic algorithms are reviewed. For example, an analysis of relatively old Lamport's hash-chain protocol is provided. At the same time, we examine HOTP and TOTP protocols which are actively used nowadays. The main result of the work are conclusions about the security of reviewed protocols based on one-time passwords.
2019-01-21
Yao, S., Niu, B., Liu, J..  2018.  Enhancing Sampling and Counting Method for Audio Retrieval with Time-Stretch Resistance. 2018 IEEE Fourth International Conference on Multimedia Big Data (BigMM). :1–5.

An ideal audio retrieval method should be not only highly efficient in identifying an audio track from a massive audio dataset, but also robust to any distortion. Unfortunately, none of the audio retrieval methods is robust to all types of distortions. An audio retrieval method has to do with both the audio fingerprint and the strategy, especially how they are combined. We argue that the Sampling and Counting Method (SC), a state-of-the-art audio retrieval method, would be promising towards an ideal audio retrieval method, if we could make it robust to time-stretch and pitch-stretch. Towards this objective, this paper proposes a turning point alignment method to enhance SC with resistance to time-stretch, which makes Philips and Philips-like fingerprints resist to time-stretch. Experimental results show that our approach can resist to time-stretch from 70% to 130%, which is on a par to the state-of-the-art methods. It also marginally improves the retrieval performance with various noise distortions.

2018-05-01
Li, Z., Beugnon, S., Puech, W., Bors, A. G..  2017.  Rethinking the High Capacity 3D Steganography: Increasing Its Resistance to Steganalysis. 2017 IEEE International Conference on Image Processing (ICIP). :510–414.

3D steganography is used in order to embed or hide information into 3D objects without causing visible or machine detectable modifications. In this paper we rethink about a high capacity 3D steganography based on the Hamiltonian path quantization, and increase its resistance to steganalysis. We analyze the parameters that may influence the distortion of a 3D shape as well as the resistance of the steganography to 3D steganalysis. According to the experimental results, the proposed high capacity 3D steganographic method has an increased resistance to steganalysis.

2018-04-02
Innokentievich, T. P., Vasilevich, M. V..  2017.  The Evaluation of the Cryptographic Strength of Asymmetric Encryption Algorithms. 2017 Second Russia and Pacific Conference on Computer Technology and Applications (RPC). :180–183.

We propose a method for comparative analysis of evaluation of the cryptographic strength of the asymmetric encryption algorithms RSA and the existing GOST R 34.10-2001. Describes the fundamental design ratios, this method is based on computing capacity used for decoding and the forecast for the development of computer technology.

2018-02-28
Hess, A. V., Mödersheim, S..  2017.  Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :451–463.

There are several works on the formalization of security protocols and proofs of their security in Isabelle/HOL; there have also been tools for automatically generating such proofs. This is attractive since a proof in Isabelle gives a higher assurance of the correctness than a pen-and-paper proof or the positive output of a verification tool. However several of these works have used a typed model, where the intruder is restricted to "well-typed" attacks. There also have been several works that show that this is actually not a restriction for a large class of protocols, but all these results so far are again pen-and-paper proofs. In this work we present a formalization of such a typing result in Isabelle/HOL. We formalize a constraint-based approach that is used in the proof argument of such typing results, and prove its soundness, completeness and termination. We then formalize and prove the typing result itself in Isabelle. Finally, to illustrate the real-world feasibility, we prove that the standard Transport Layer Security (TLS) handshake satisfies the main condition of the typing result.