Sven Laur · Aaltodoc (Aalto University) · 2008
In this work, we investigate the security of interactive computations. The main emphasis is on the mathematical methodology that is needed to formalise and analyse various security properties. Differently from many classical treatments of secure multi-party computations, we always quantify security in exact terms. Although working with concrete time bounds and success probabilities is technically more demanding, it also has several advantages. As all security guarantees are quantitative, we can always compare different protocol designs. Moreover, these security guarantees also have a clear economical interpretation and it is possible to compare cryptographic and non-cryptographic solutions. The latter is extremely important in practice, since cryptographic techniques are just one possibility to achieve practical security. Also, working with exact bounds makes reasoning errors more apparent, as security proofs are less abstract and it is easier to locate false claims. \n The choice of topics covered in this thesis was guided by two principles. Firstly, we wanted to give a coherent overview of the secure multi-party computation that is based on exact quantification of security guarantees. Secondly, we focused on topics that emerged from the author's own research. In that sense, the thesis generalises many methodological discoveries made by the author. \n As surprising as it may seem, security definitions and proofs mostly utilise principles of hypothesis testing and analysis of stochastic algorithms. Thus, we start our treatment with hypothesis testing and its generalisations. In particular, we show how to quantify various security properties, using security games as tools. Next, we review basic proof techniques and explain how to structure complex proofs so they become easily verifiable. In a nutshell, we describe how to represent a proof as a game tree, where each edge corresponds to an elementary proof step. As a result, one can first verify the overall structure of a proof by looking at the syntactic changes in the game tree and only then verify all individual proof steps corresponding to the edges. \n The remaining part of the thesis is dedicated to various aspects of protocol design. Firstly, we discuss how to formalise various security goals, such as input-privacy, output-consistency and complete security, and how to choose a security goal that is appropriate for a specific setting. Secondly, we also explore alternatives to exact security. More precisely, we analyse connections between exact and asymptotic security models and rigorously formalise a notion of subjective security. Thirdly, we study in which conditions protocols preserve their security guarantees and how to safely combine several protocols. Although composability results are common knowledge, we look at them from a slightly different angle. Namely, it is irrational to design universally composable protocols at any cost; instead, we should design computationally efficient protocols with minimal usage restrictions. Thus, we propose a three-stage design procedure that leads to modular security proofs and minimises usage restrictions.
Cited by 1Open access
Sushil Jajodia, Pierangela Samarati, Moti Yung · 2025
Cited by 0
Ramzan, M., Khan, M. K. · arXiv (Cornell University) · 2009
We propose a multiparty quantum cryptographic protocol. Unitary operators applied by Bob and Charlie, on their respective qubits of a tripartite entangled state encodes a classical symbol that can be decoded at Alice's end with the help of a decoding matrix. Eve's presence can be detected by the disturbance of the decoding matrix. Our protocol is secure against intercept-resend attacks. Furthermore, it is efficient and deterministic in the sense that two classical bits can be transferred per entangled pair of qubits. It is worth mentioning that in this protocol same symbol can be used for key distribution and Eve's detection that enhances the efficiency of the protocol.
Cited by 0Open access
Simon Kramer · 2008
Abstract. We extend the (core) Cryptographic Protocol Logic (CPL) (qualitative time) with real time, i.e., time stamps, timed keys, and potentially drifting local clocks, to tCPL (quantitative time). Our extension is conservative and really simple; it requires only the refinement of two relational symbols (two new axioms resp. one new parameter) and of one operator (one new conjunct in its truth predicate), and the addition of two relational symbols (but no operators!). Our work 1 thus provides further evidence for Lamport’s claim that adding real time to an untimed formalism is really simple. Keywords applied formal logic, cryptographic protocols, propertybased specification and verification, real time The formal modelling, specification, and verification of general-purpose timed systems has received considerable attention from the formal methods community since the end of the nineteen-eighties. See [2] for a survey of timed models (automata, Petri nets), model- and property-based specification languages (process
Cited by 0
Койбічук, В.В. · Electronic Sumy State University Institutional Repository (Sumy State University) · 2010
Опис криптографічних систем, що використовують протокол Kerberos для захисту конфіденційної інформації при передачі по відкритій розподіленій мережі.
Cited by 0Open access
Abdulbasit Ahmed, Alexei P. Lisitsa, Andrei P. Nemytykh · 2014
It has been known for a while [35, 36, 12] that program transformation techniques, in particular, program specialization, can be used to prove the properties of programs automatically. For example, if a program actually implements (in a given context of use) a constant function sufficiently powerful and semantics preserving program transformation may reduce the program to a syntactically trivial “constant ” program, pruning unreachable branches and proving thereby the property. Viability of such an approach to verification has been demonstrated in previous works [16, 19, 18] where it was applied to the verification of parameterized cache coherence protocols and Petri Nets models [11, 20]. In this paper we further extend the method and present a case study on its application to the verification of a cryptographic protocol. The protocol is modeled by functional programs at different levels of abstraction and verification via program specialization is done by using Turchin’s supercompilation method.
Cited by 0
Thomas Genet, Francis Klay · OpenGrey (Institut de l'Information Scientifique et Technique) · 1999
. On a case study, we present a new approach for verifying cryptographic protocols, based on rewriting and on tree automata techniques. Protocols are operationally described using Term Rewriting Systems and the initial set of communication requests is described by a tree automaton. Starting from these two representations, we automatically compute an over-approximation of the set of exchanged messages (also recognized by a tree automaton). Then, proving classical properties like confidentiality or authentication can be done by automatically showing that the intersection between the approximation and a set of prohibited behaviors is the empty set. Furthermore, this method enjoys a simple and powerful way to describe intruder work, the ability to consider an unbounded number of parties, an unbounded number of interleaved sessions, and a theoretical property ensuring safeness of the approximation. Introduction In this paper, we present a new way of verifying cryptographic pro...
Cited by 0
Paul F. Syverson, et al. · 2008
We present a logic for analyzing cryptographic protocols. This logic is based on a uni cation of four of its predecessors in the BAN family of logics, namely those given in [GNY90], [AT91], [vO93b], and BAN itself [BAN89]. The logic herein captures the desirable features of its predecessors and more; nonetheless, as a logic it is relatively simple and simple to use. We also present a model-theoretic semantics, and we prove soundness for the logic with respect to that semantics. We illustrate the logic by applying it to the Needham-Schroeder protocol, revealing that BAN analysis of it may lead to inappropriate conclusions in some settings. We also use the logic to analyze two key agreement protocols, examining an attack on one of them.
Cited by 0
Jonathan Millen, Frederic Muller · 2007
Java code is generated to implement cryptographic network protocols specified abstractly in CAPSL. The translation source is the CAPSL intermediate language CIL, and the output includes code for each party and for a demonstration environment server that permits user examination and control of communication. Standard Java cryptographic providers are used.
Cited by 0
Roberto Zunino · Electronic Theses and Dissertations Repository (University of Pisa) · 2006
Formal models for security protocols often rely on assumptions not to be found in computational models. A first assumption is the perfect encryption one: encrypted data can not be manipulated in any way unless the decryption key is known. Another usual assumption is the free algebra one: only a few cryptographic primitives are considered in the model, and these must form a free algebra. We study these assumptions, and relax them to define more general models. We then define static analysis techniques for veryfing protocols secure in our models.
Cited by 3Open access
Thomas Genet, Francis Klay · Lecture notes in computer science · 2000
Cited by 121
Sven Laur, Abteknillinen Korkeakoulu, Universite De et al. · 2008
ABSTRACT: In this work, we investigate the security of interactive computations. The main emphasis is on the mathematical methodology that is needed to formalise and analyse various security properties. Differently from many classical treatments of secure multi-party computations, we always quantify security in exact terms. Although working with concrete time bounds and success probabilities is technically more demanding, it also has several advantages. As all security guarantees are quantitative, we can always compare different protocol designs. Moreover, these security guarantees also have a clear economical interpretation and it is possible to compare cryptographic and non-cryptographic solutions. The latter is extremely important in practice, since cryptographic techniques are just one possibility to achieve practical security. Also, working with exact bounds makes reasoning errors more apparent, since security proofs are less abstract and it is easier to locate false claims. The choice of topics covered in this thesis was guided by two principles. First, we wanted to give a coherent overview of secure multi-party computation that
Cited by 0
Gandhe Sripriya · International Research Journal of Education and Technology (IRJET). · 2024
Cited by 0Open access
Paul Syverson, Paul C. van Oorschot · 1996
Abstract : We present a logic for analyzing cryptographic protocols. This logic is based on a unification of four of its predecessors in the BAN family of logics, namely those given in [GNY90], [AT91], [vO93b], and BAN itself [BAN89]. The logic herein captures the desirable features of its predecessors and more; nonetheless, as a logic it is relatively simple and simple to use. We also present a model-theoretic semantics, and we prove soundness for the logic with respect to that semantics. We illustrate the logic by applying it to the Needham- Schroeder protocol, revealing that BAN analysis of it may lead to inappropriate conclusions in some settings. We also use the logic to analyze two key agreement protocols, examining an attack on one of them.
Cited by 81
Aaron Hunter, James P. Delgrande · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2007
Cryptographic protocols are structured sequences of messages that are used for exchanging information in a hostile environment. Many protocols have epistemic goals: a successful run of the protocol is intended to cause a participant to hold certain beliefs. As such, epistemic logics have been employed for the verification of cryptographic protocols. Although this approach to verification is explicitly concerned with changing beliefs, formal belief change operators have not been incorporated in previous work. In this paper, we introduce a new approach to protocol verification by combining a monotonic logic with a non-monotonic belief change operator. In this context, a protocol participant is able to retract beliefs in response to new information and a protocol participant is able to postulate the most plausible event explaining new information. We illustrate that this kind of reasoning is particularly important when protocol participants have incorrect beliefs.
Cited by 6Open access
Youliang Tian, Peng Chenggen, Jianfeng Ma et al. · 2014
Cited by 2
Robert W. Baldwin, Wayne C. Gramlich · 1985
A problem with conflicting goals of anonymity and authentication is defined and a cryptographic protocol that solves the problem is presented. The protocol uses an authentication scheme that provides the desired degree of anonymity and authentication. Fake transactions are used to detect active attackers, and to camouflage information that cannot be hidden cryptographically.
Cited by 23
Morton, Robart, Tavares · 1994
In this paper, decomposition techniques are used to simplify the analysis of cryptographic protocols using coloured Petri nets to locate security flaws and weaknesses. These techniques exploit the inherent modularity of the Petri net model which is composed of distinct protocol entities, distinct protocol stages, and an explicit intruder model. The intruder model may embody a suite of threat characteristics, which can be used to formulate simple or complex attacks. The methodology is described in this paper and is applied to a one-way authentication protocol with two stages.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
Cited by 2
Herbrych, Daniel · Brno University of Technology Digital Library (Brno University of Technology) · 2019
Tato práce má za cíl vytvořit generátor eliptických křivek pro kryptografický protokol. Je k tomu použita knihovna MIRACL a jazyk C++. Jedním ze stěžejních problémů je určení řádu grupy eliptické křivky. Pro toto se používá algoritmus SEA (Schoof Elkies Atkin), dle toho je tak metoda napříč zdroji zvána jako metoda počítání bodů na křivce, SEA metoda, případně i jinak. Druhou metodou pro generování je metoda komplexního násobení (complex multiplication, zkráceně CM). Obě jsou v generátoru k dispozici. Byla měřena závislost rychlosti základních operací nad eliptickou křivkou na velikosti křivky a také na jednotlivých parametrech křivky. Bylo implementováno hybridní schéma ECIES jako praktické ověření funkčnosti generátoru. Dále byly měřeny rychlosti ECIES šifrování a dešifrování v závislosti na různých parametrech, např. velikost křivky, jakou metodou byla křivka vygenerována, velikost zprávy a další.
Cited by 0
Jan Van Eijck, Rosa Play, Number Guessing Game · 2016
The talk is about the application of model checking to the analysis of cryptographic security protocols. As a step towards that, I will start with a proposal for how to represent knowledge of large numbers in Kripke models, and I will use this representation to model a protocol for secret key distribution over an insecure network in DEL. An prototype implementation of an epistemic model checker for cryptographic protocol anal-ysis exists. How to Model Ignorance? w: H w ′ : T What does it mean to know a number?
Cited by 0