Search results for: Threshold Cryptography.

Authors: S.M. Sarwarul Islam Rizvi, Zinat Sultana, Bo Sun, Md. Washiqul Islam

Abstract:

In a very simple form a Mobile Agent is an independent piece of code that has mobility and autonomy behavior. One of the main advantages of using Mobile Agent in a network is - it reduces network traffic load. In an, ad hoc network Mobile Agent can be used to protect the network by using agent based IDS or IPS. Besides, to deploy dynamic software in the network or to retrieve information from network nodes Mobile Agent can be useful. But in an ad hoc network the Mobile Agent itself needs some security. Security services should be guaranteed both for Mobile Agent and for Agent Server. In this paper to protect the Mobile Agent and Agent Server in an ad hoc network we have proposed a solution which is based on Threshold Cryptography, a new vibe in the cryptographic world where trust is distributed among multiple nodes in the network.

Keywords: Ad hoc network, Mobile Agent, Security, Threats, Threshold Cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1920

Authors: Pierre-Louis Cayrel, Sidi Mohamed El Yousfi Alaoui

Abstract:

In this paper, we propose a dual version of the first threshold ring signature scheme based on error-correcting code proposed by Aguilar et. al in [1]. Our scheme uses an improvement of Véron zero-knowledge identification scheme, which provide smaller public and private key sizes and better computation complexity than the Stern one. This scheme is secure in the random oracle model.

Keywords: Stern algorithm, Véron algorithm, threshold ring signature, post-quantum cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1753

Authors: R. Rama Kishore, Sunesh

Abstract:

Nowadays, robust and secure watermarking algorithm and its optimization have been need of the hour. A watermarking algorithm is presented to achieve the copy right protection of the owner based on visual cryptography, histogram shape property and entropy. In this, both host image and watermark are preprocessed. Host image is preprocessed by using Butterworth filter, and watermark is with visual cryptography. Applying visual cryptography on water mark generates two shares. One share is used for embedding the watermark, and the other one is used for solving any dispute with the aid of trusted authority. Usage of histogram shape makes the process more robust against geometric and signal processing attacks. The combination of visual cryptography, Butterworth filter, histogram, and entropy can make the algorithm more robust, imperceptible, and copy right protection of the owner.

Keywords: Butterworth filter, digital watermarking, histogram, visual cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1615

Authors: Youguo Wang, Lenan Wu

Abstract:

We discuss the signal detection through nonlinear threshold systems. The detection performance is assessed by the probability of error Per . We establish that: (1) when the signal is complete suprathreshold, noise always degrades the signal detection both in the single threshold system and in the parallel array of threshold devices. (2) When the signal is a little subthreshold, noise degrades signal detection in the single threshold system. But in the parallel array, noise can improve signal detection, i.e., stochastic resonance (SR) exists in the array. (3) When the signal is predominant subthreshold, noise always can improve signal detection and SR always exists not only in the single threshold system but also in the parallel array. (4) Array can improve signal detection by raising the number of threshold devices. These results extend further the applicability of SR in signal detection.

Keywords: Probability of error, signal detection, stochasticresonance, threshold system.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1390

Authors: Siti Norul Huda Sheikh Abdullah, Farshid Pirahan Siah, Nor Hanisah Haji Zainal Abidin, Shahnorbanun Sahran

Abstract:

The objective of this paper is to propose an adaptive multi threshold for image segmentation precisely in object detection. Due to the different types of license plates being used, the requirement of an automatic LPR is rather different for each country. The proposed technique is applied on Malaysian LPR application. It is based on Multi Layer Perceptron trained by back propagation. The proposed adaptive threshold is introduced to find the optimum threshold values. The technique relies on the peak value from the graph of the number object versus specific range of threshold values. The proposed approach has improved the overall performance compared to current optimal threshold techniques. Further improvement on this method is in progress to accommodate real time system specification.

Keywords: Multi-threshold approach, license plate recognition system.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2474

Authors: Elsa Eka Putri, N.S.V Kameswara Rao, M. A. Mannan

Abstract:

The objective of this study is to evaluate the threshold stress of the clay with sand subgrade soil. Threshold stress can be defined as the stress level above which cyclic loading leads to excessive deformation and eventual failure. The thickness determination of highways formations using the threshold stress approach is a more realistic assessment of the soil behaviour because it is subjected to repeated loadings from moving vehicles. Threshold stress can be evaluated by plastic strain criterion, which is based on the accumulated plastic strain behaviour during cyclic loadings [1]. Several conditions of the all-round pressure the subgrade soil namely, zero confinement, low all-round pressure and high all-round pressure are investigated. The threshold stresses of various soil conditions are determined. Threshold stress of the soil are 60%, 31% and 38.6% for unconfined partially saturated sample, low effective stress saturated sample, high effective stress saturated sample respectively.

Keywords: threshold stress, cyclic loading, pore water pressure.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2552

Authors: A. Javaheri, A. R. Kabiri-Samani

Abstract:

In this study an extensive experimental research is carried out to develop a better understanding of the effects of Piano Key (PK) weir geometry on weir flow threshold submergence. Experiments were conducted in a 12 m long, 0.4 m wide and 0.7 m deep rectangular glass wall flume. The main objectives were to investigate the effect of the PK weir geometries including the weir length, weir height, inlet-outlet key widths, upstream and downstream apex overhangs, and slopped floors on threshold submergence and study the hydraulic flow characteristics. From the experimental results, a practical formula is proposed to evaluate the flow threshold submergence over PK weirs.

Keywords: Model experimentation, flow characteristics, Piano Key weir, threshold submergence.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2129

Authors: Nataša Živić, Christoph Ruland

Abstract:

Method of Parallel Joint Channel Coding and Cryptography has been analyzed and simulated in this paper. The method is an extension of Soft Input Decryption with feedback, which is used for improvement of channel decoding of secured messages. Parallel Joint Channel Coding and Cryptography results in improved coding gain of channel decoding, which achieves more than 2 dB. Such results are an implication of a combination of receiver components and their interoperability.

Keywords: Block length, Coding gain, Feedback, L-values, Parallel Joint Channel Coding and Cryptography, Soft Input Decryption.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1522

Authors: Rawan I. Zaghloul, Enas F. Al-Rawashdeh

Abstract:

In this paper a simple watermarking method for color images is proposed. The proposed method is based on watermark embedding for the histograms of the HSV planes using visual cryptography watermarking. The method has been proved to be robust for various image processing operations such as filtering, compression, additive noise, and various geometrical attacks such as rotation, scaling, cropping, flipping, and shearing.

Keywords: Histogram, HSV image, Visual Cryptography, Watermark.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1926

Authors: Bradley Christensen, Kevin T. McCusker, Daniel J. Gauthier, Daniel Kumor, Venkat Chandar, P. G. Kwiat

Abstract:

We report on a high-speed quantum cryptography system that utilizes simultaneous entanglement in polarization and in “time-bins". With multiple degrees of freedom contributing to the secret key, we can achieve over ten bits of random entropy per detected coincidence. In addition, we collect from multiple spots o the downconversion cone to further amplify the data rate, allowing usto achieve over 10 Mbits of secure key per second.

Keywords: Downconversion, Hyper-entanglement, Quantum Cryptography

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1652

Authors: A. Rangan, A. Tansu

Abstract:

This paper generalizes Yeh Lam-s shock model for renewal shock arrivals and random threshold. Several interesting statistical measures are explicitly obtained. A few special cases and an optimal replacement problem are also discussed.

Keywords: shock model, optimal replacement, random threshold, shocks.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1524

Authors: Neil Morgan

Abstract:

The notion of Threshold Concepts has offered a fertile new perspective on the transformative effects of mastery of particular concepts on student understanding of subject matter and their developing identities as inductees into disciplinary discourse communities. Only by successfully traversing essential knowledge thresholds can neophytes achieve the more sophisticated understandings of subject matter possessed by mature members of a discipline. This paper uses thematic analysis of disciplinary guiding principles to identify nine candidate Threshold Concepts that appear to underpin effective TESOL practice. The relationship between these candidate TESOL Threshold Concepts, TESOL principles, and TESOL instructional techniques appears to be amenable to a schematic representation based on superordinate categories of TESOL practitioner concern and, as such, offers an alternative to the view of Threshold Concepts as a privileged subset of disciplinary core concepts. The paper concludes by exploring the potential of a Threshold Concepts framework to productively inform TESOL initial teacher education (ITE) and in-service education and training (INSET).

Keywords: TESOL, threshold concepts, TESOL principles, TESOL ITE/INSET, community of practice.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 651

Authors: Shuvro Chowdhury, Esmat Farzana, Rizvi Ahmed, A. T. M. Golam Sarwar, M. Ziaur Rahman Khan

Abstract:

The threshold voltage and capacitance voltage characteristics of ultra-thin Silicon-on-Insulator MOSFET are greatly influenced by the thickness and doping concentration of the silicon film. In this work, the capacitance voltage characteristics and threshold voltage of the device have been analyzed with quantum mechanical effects using the Self-Consistent model. Reduction of channel thickness and adding doping impurities cause an increase in the threshold voltage. Moreover, the temperature effects cause a significant amount of threshold voltage shift. The temperature dependence of threshold voltage has also been observed with Self- Consistent approach which are well supported from experimental performance of practical devices.

Keywords: C-V characteristics, Self-Consistent Analysis, Siliconon-Insulator, Ultra-thin film.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2640

Authors: Lenka Krulikovská, Jaroslav Polec

Abstract:

In this paper we present a modification to existed model of threshold for shot cut detection, which is able to adapt itself to the sequence statistics and operate in real time, because it use for calculation only previously evaluated frames. The efficiency of proposed modified adaptive threshold scheme was verified through extensive test experiment with several similarity metrics and achieved results were compared to the results reached by the original model. According to results proposed threshold scheme reached higher accuracy than existed original model.

Keywords: Abrupt cut, shot cut detection, adaptive threshold.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1487

Authors: Ching-Sheng Hsu, Young-Chang Hou

Abstract:

In this paper, a novel copyright protection scheme for digital images based on Visual Cryptography and Statistics is proposed. In our scheme, the theories and properties of sampling distribution of means and visual cryptography are employed to achieve the requirements of robustness and security. Our method does not need to alter the original image and can identify the ownership without resorting to the original image. Besides, our method allows multiple watermarks to be registered for a single host image without causing any damage to other hidden watermarks. Moreover, it is also possible for our scheme to cast a larger watermark into a smaller host image. Finally, experimental results will show the robustness of our scheme against several common attacks.

Keywords: Copyright protection, digital watermarking, samplingdistribution, visual cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1839

Authors: K. Suganya Devi, P. Srinivasan, M. P. Vaishnave, G. Arutperumjothi

Abstract:

Today’s internet world is highly prone to various online attacks, of which the most harmful attack is phishing. The attackers host the fake websites which are very similar and look alike. We propose an image based authentication using steganography and visual cryptography to prevent phishing. This paper presents a secure steganographic technique for true color (RGB) images and uses Discrete Cosine Transform to compress the images. The proposed method hides the secret data inside the cover image. The use of visual cryptography is to preserve the privacy of an image by decomposing the original image into two shares. Original image can be identified only when both qualified shares are simultaneously available. Individual share does not reveal the identity of the original image. Thus, the existence of the secret message is hard to be detected by the RS steganalysis.

Keywords: Image security, random LSB, steganography, visual cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1330

Authors: A. Chillali, A. Tadmori, M. Ziane

Abstract:

In this article we will study the elliptic curve defined over the ring An and we define the mathematical operations of ECC, which provides a high security and advantage for wireless applications compared to other asymmetric key cryptosystem.

Keywords: Elliptic Curves, Finite Ring, Cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2059

Authors: Wei Hua Ho

Abstract:

Vortices can develop in intakes of turbojet and turbo fan aero engines during high power operation in the vicinity of solid surfaces. These vortices can cause catastrophic damage to the engine. The factors determining the formation of the vortex include both geometric dimensions as well as flow parameters. It was shown that the threshold at which the vortex forms or disappears is also dependent on the initial flow condition (i.e. whether a vortex forms after stabilised non vortex flow or vice-versa). A computational fluid dynamics study was conducted to determine the difference in thresholds between the two conditions. This is the first reported numerical investigation of the “memory effect". The numerical results reproduce the phenomenon reported in previous experimental studies and additional factors, which had not been previously studied, were investigated. They are the rate at which ambient velocity changes and the initial value of ambient velocity. The former was found to cause a shift in the threshold but not the later. It was also found that the varying condition thresholds are not symmetrical about the neutral threshold. The vortex to no vortex threshold lie slightly further away from the neutral threshold compared to the no vortex to vortex threshold. The results suggests that experimental investigation of vortex formation threshold performed either in vortex to no vortex conditions, or vice versa, solely may introduce mis-predictions greater than 10%.

Keywords: Jet Engine Test Cell, Unsteady flow, Inlet Vortex

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1995

Authors: Muhibul Haque Bhuyan, Quazi Deen Mohd Khosru

Abstract:

This paper presents a threshold voltage model of pocket implanted sub-100 nm n-MOSFETs incorporating the drain and substrate bias effects using two linear pocket profiles. Two linear equations are used to simulate the pocket profiles along the channel at the surface from the source and drain edges towards the center of the n-MOSFET. Then the effective doping concentration is derived and is used in the threshold voltage equation that is obtained by solving the Poisson-s equation in the depletion region at the surface. Simulated threshold voltages for various gate lengths fit well with the experimental data already published in the literature. The simulated result is compared with the two other pocket profiles used to derive the threshold voltage models of n-MOSFETs. The comparison shows that the linear model has a simple compact form that can be utilized to study and characterize the pocket implanted advanced ULSI devices.

Keywords: Linear pocket profile, pocket implantation, nMOSFET, threshold voltage, short channel effect (SCE), reverse short channeleffect (RSCE).

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1746

Authors: F. Amin, A. H. Jahangir, H. Rasifard

Abstract:

With the widespread growth of applications of Wireless Sensor Networks (WSNs), the need for reliable security mechanisms these networks has increased manifold. Many security solutions have been proposed in the domain of WSN so far. These solutions are usually based on well-known cryptographic algorithms. In this paper, we have made an effort to survey well known security issues in WSNs and study the behavior of WSN nodes that perform public key cryptographic operations. We evaluate time and power consumption of public key cryptography algorithm for signature and key management by simulation.

Keywords: Wireless Sensor Networks, Security, Public Key Cryptography, Key Management.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3638

Authors: Jonathan Bohn, Jorge Rebaza, Kaitlin Speer

Abstract:

The dynamics of a predator-prey model with continuous threshold policy harvesting functions on the prey is studied. Theoretical and numerical methods are used to investigate boundedness of solutions, existence of bionomic equilibria, and the stability properties of coexistence equilibrium points and periodic orbits. Several bifurcations as well as some heteroclinic orbits are computed.

Keywords: Predator-prey models, threshold harvesting, dynamicalsystems

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2257

Authors: Mahmoud A. Hassan, Mohammed A. Khalili

Abstract:

We are proposing a simple watermarking method based on visual cryptography. The method is based on selection of specific pixels from the original image instead of random selection of pixels as per Hwang [1] paper. Verification information is generated which will be used to verify the ownership of the image without the need to embed the watermark pattern into the original digital data. Experimental results show the proposed method can recover the watermark pattern from the marked data even if some changes are made to the original digital data.

Keywords: Watermarking, visual cryptography, visualthreshold.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1694

Authors: Nisarg A. Patel, Hiren B. Patel

Abstract:

Quantum cryptography is described as a point-to-point secure key generation technology that has emerged in recent times in providing absolute security. Researchers have started studying new innovative approaches to exploit the security of Quantum Key Distribution (QKD) for a large-scale communication system. A number of approaches and models for utilization of QKD for secure communication have been developed. The uncertainty principle in quantum mechanics created a new paradigm for QKD. One of the approaches for use of QKD involved network fashioned security. The main goal was point-to-point Quantum network that exploited QKD technology for end-to-end network security via high speed QKD. Other approaches and models equipped with QKD in network fashion are introduced in the literature as. A different approach that this paper deals with is using QKD in existing protocols, which are widely used on the Internet to enhance security with main objective of unconditional security. Our work is towards the analysis of the QKD in Mobile ad-hoc network (MANET).

Keywords: QKD, cryptography, quantum cryptography, network performance.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 850

Authors: K. E. Kaharudin, A. H. Hamidon, F. Salehuddin

Abstract:

Vertical Double Gate (DG) Metal Oxide Semiconductor Field Effect Transistor (MOSFET) is believed to suppress various short channel effect problems. The gate to channel coupling in vertical DG-MOSFET are doubled, thus resulting in higher current density. By having two gates, both gates are able to control the channel from both sides and possess better electrostatic control over the channel. In order to ensure that the transistor possess a superb turn-off characteristic, the subs-threshold swing (SS) must be kept at minimum value (60-90mV/dec). By utilizing SILVACO TCAD software, an n-channel vertical DG-MOSFET was successfully designed while keeping the sub-threshold swing (SS) value as minimum as possible. From the observation made, the value of sub-threshold swing (SS) was able to be varied by adjusting the height of the silicon pillar. The minimum value of sub-threshold swing (SS) was found to be 64.7mV/dec with threshold voltage (V_TH) of 0.895V. The ideal height of the vertical DG-MOSFET pillar was found to be at 0.265 µm.

Keywords: DG-MOSFET, pillar, SCE, vertical

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1816

Authors: Ran-Zan Wang, Yao-Ting Lee

Abstract:

This paper proposes a visual cryptography by random grids scheme with identifiable shares. The method encodes an image O in two shares that exhibits the following features: (1) each generated share has the same scale as O, (2) any share singly has noise-like appearance that reveals no secret information on O, (3) the secrets can be revealed by superimposing the two shares, (4) folding a share up can disclose some identification patterns, and (5) both of the secret information and the designated identification patterns are recognized by naked eye without any computation. The property to show up identification patterns on folded shares establishes a simple and friendly interface for users to manage the numerous shares created by VC schemes.

Keywords: Image Encryption, Image Sharing, Secret Sharing, Visual Cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1717

Authors: Anthony Overmars, Sitalakshmi Venkatraman

Abstract:

This paper presents a method for determining all of the co-prime right angle triangles in the Euclidean field by looking at the intersection of the Pythagorean and Platonic right angle triangles and the corresponding lattice that this produces. The co-prime properties of each lattice point representing a unique right angle triangle are then considered. This paper proposes a conjunction between these two ancient disparaging theorists. This work has wide applications in information security where cryptography involves improved ways of finding tuples of prime numbers for secure communication systems. In particular, this paper has direct impact in enhancing the encryption and decryption algorithms in cryptography.

Keywords: Pythagorean triples, platonic triples, right angle triangles, co-prime numbers, cryptography.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1196

Authors: Aytunc Durlanik, Ibrahim Sogukpinar

Abstract:

SIP (Session Initiation Protocol), using HTML based call control messaging which is quite simple and efficient, is being replaced for VoIP networks recently. As for authentication and authorization purposes there are many approaches and considerations for securing SIP to eliminate forgery on the integrity of SIP messages. On the other hand Elliptic Curve Cryptography has significant advantages like smaller key sizes, faster computations on behalf of other Public Key Cryptography (PKC) systems that obtain data transmission more secure and efficient. In this work a new approach is proposed for secure SIP authentication by using a public key exchange mechanism using ECC. Total execution times and memory requirements of proposed scheme have been improved in comparison with non-elliptic approaches by adopting elliptic-based key exchange mechanism.

Keywords: SIP, Elliptic Curve Cryptography, voice over IP.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2468

Authors: S. Boorboor, S. A. H. Feghhi, H. Jafari

Abstract:

The ionizing radiations cause different kinds of damages in electronic components. MOSFETs, most common transistors in today’s digital and analog circuits, are severely sensitive to TID damage. In this work, the threshold voltage shift of CD4007 device, which is an integrated circuit including P-channel and N-channel MOS transistors, was investigated for low dose gamma irradiation under different gate bias voltages. We used linear extrapolation method to extract threshold voltage from I_D-V_G characteristic curve. The results showed that the threshold voltage shift was approximately 27.5 mV/Gy for N-channel and 3.5 mV/Gy for P-channel transistors at the gate bias of |9 V| after irradiation by Co-60 gamma ray source. Although the sensitivity of the devices under test were strongly dependent to biasing condition and transistor type, the threshold voltage shifted linearly versus accumulated dose in all cases. The overall results show that the application of CD4007 as an electronic buffer in a radiation therapy system is limited by TID damage. However, this integrated circuit can be used as a cheap and sensitive radiation dosimeter for accumulated dose measurement in radiation therapy systems.

Keywords: Threshold voltage shift, MOS transistor, linear extrapolation, gamma irradiation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1320

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1418

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this paper we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (o--algebras, probability spaces and condi¬tional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes' Formula. Besides we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this paper shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2134