No description available.

We show that the long-standing assumption of "no-communication" between the provers of the two-prover model is not sufficiently precise to guarantee the security of a bit commitment scheme against malicious adversaries. Indeed, we show how a simple correlated random variable, which does not allow to communicate, can be used to cheat a simplified version (sBGKW) of the bit commitment scheme of Ben-Or, Goldwasser, Kilian, and Wigderson [BGKW88]. Instead we propose a stronger notion of separation between the two provers which takes into account correlated computations. To emphasize the risk that entanglement still represents for the security of a commitment scheme despite the stronger notion of separation, we present two variations of the sBGKW scheme that can be cheated by quantum provers with probability (almost) one. A complete proof of security against quantum adversaries is then given for the sBGKW scheme. By reduction we also obtain the security of the original BGKW scheme against quantum provers. For the unfamiliar reader, basic notions of quantum processing are provided to facilitate the understanding of the proofs presented.

Thesis (M.S.)--Rochester Institute of Technology, 1992. / Typescript. Includes bibliographical references.

Thesis (M.S.)--University of North Texas, Dec., 2009. / Title from title page display. Includes bibliographical references.

Thesis (M.S.)--Rochester Institute of Technology, 2009. / Typescript. Includes bibliographical references (leaves 56-59).

We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown access-control policy languages such as eXtensible Access Control Markup Language (XACML) [OAS13] already exist, because access rules in such languages are often expressed in a declarative manner using fragments of a natural language like English, it isn’t alwaysclear what the intended behaviour of the system encoded in these access rules should be. To remedy this ambiguity, formal specification of how an access-control mechanism should behave, is typically given in some sort of logic, often a subset of first order logic. To show that an access-control system actually behaves correctly with respect to its specification, proofs are needed, however the proofs that are often presented in the literature are hard or impossible to formally verify. The verification difficulty is partly due to the fact that the language used to do the proofs while mathematical in nature, utilizes intuitive justifications to derive the proofs. Intuitive language in proofs means that the proofs could be incomplete and/or contain subtle errors. ACCPL is small by design. By small we refer to the size of the language; the syntax, auxiliary definitions and the semantics of ACCPL only take a few pages to describe. This compactness allows us to concentrate on the main goal of this thesis which is the ability to reason about the policies written in ACCPL with respect to specific questions. By making the language compact, we have stayed away from completeness and expressive power in several directions. For example, ACCPL uses only a single policy combinator, the conjunction policy combinator. The design of ACCPL is therefore a trade-off between ease of formal proof of correctness and expressive power. We also consider ACCPL a core policy access-control language since we have retained the core features of many access-control policy languages. For instance ACCPL employs a single condition type called a “prerequisite” where other languages may have very expressive and rich sets of conditions.

Zero-knowledge proofs protocols are effective interactive methods to prove a node's identity without disclosing any additional information other than the veracity of the proof. They are implementable in several ways. In this thesis, I investigate the graph isomorphism based zero-knowledge proofs protocol. My experiments and analyses suggest that graph isomorphism can easily be solved for many types of graphs and hence is not an ideal solution for implementing ZKP.

No description available.

Three studies in the machine assisted proof of recursion implementation are described. The verification system used is Edinburgh LCF (Logic for Computable Functions). Proofs are generated, in LCF, in a goal-oriented fashion by the application of strategies reflecting informal proof plans. LCF is introduced in Chapter 1. We present three case studies in which proof strategies are developed and (except in the third) tested in LCF. Chapter 2 contains an account of the machine generated proofs of three program transformations (from recursive to iterative function schemata). Two of the examples are taken from Manna and Waldinger. In each case, the recursion is implemented by the introduction of a new data type, e.g., a stack or counter. Some progress is made towards the development of a general strategy for producing the equivalence proofs of recursive and iterative function schemata by machine. Chapter 3 is concerned with the machine generated proof of the correctness of a compiling algorithm. The formulation, borrowed from Russell, includes a simple imperative language with a while and conditional construct, and a low level language of labelled statements, including jumps. We have, in LCF, formalised his denotational descriptions of the two languages and performed a proof of the preservation of the semantics under compilation. In Chapter 4, we express and informally prove the correctness of a compiling algorithm for a language containing declarations and calls of recursive procedures. We present a low level language whose semantics model a standard activation stack implementation. Certain theoretical difficulties (connected with recursively defined relations) are discussed, and a proposed proof in LCF is outlined. The emphasis in this work is less on proving original theorems, or even automatically finding proofs of known theorems, than on (i) exhibiting and analysing the underlying structure of proofs, and of machine proof attempts, and (ii) investigating the nature of the interaction (between a user and a computer system) required to generate proofs mechanically; that is, the transition from informal proof plans to behaviours which cause formal proofs to be performed.

According to Plato, we live in a substitute world. The things we see around us are shadows of reality, imperfect imitations of perfect originals. Beyond the world of the senses, there is another, changeless world, more real and more beautiful than our own. But how can we get at this world, or attain knowledge of it, when our senses are unreliable and the perfect philosophical method remains out of reach? In the Divided Line passage of the Republic, Plato is clear that mathematics has a role to play, but the debate about the exact nature of that role remains unresolved. My reading of the Divided Line might provide the answer. I propose that the ‘mathematical’ passages of the Meno and Phaedo contain evidence that we can use to construct the method by which Plato means us to ascend to knowledge of the Forms. In this dissertation, I shall set out my reading of Plato’s Divided Line, and show how Plato’s use of mathematics in the Meno and Phaedo supports this view. The mathematical method, adapted to philosophy, is a central part of the Line’s ‘way up’ to the definitions of Forms that pure philosophy requires. I shall argue that this method is not, as some scholars think, the geometric method of analysis and synthesis, but apagōgē, or reduction. On this reading, mathematics is pivotal on our journey into the world of the Forms.