Showing 1–9 of 9 results for author: Dougherty, J

A Coq Formalization of Unification Modulo Exclusive-Or

Authors: Yichi Xu, Daniel J. Dougherty, Rose Bohrer

Abstract: Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an alg… ▽ More Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml. △ Less

Submitted 13 February, 2025; originally announced February 2025.

Comments: In Proceedings ICLP 2024, arXiv:2502.08453

Journal ref: EPTCS 416, 2025, pp. 267-273

An Empirical Analysis of Speech Self-Supervised Learning at Multiple Resolutions

Authors: Theo Clark, Benedetta Cevoli, Eloy de Jong, Timofey Abramski, Jamie Dougherty

Abstract: Self-supervised learning (SSL) models have become crucial in speech processing, with recent advancements concentrating on developing architectures that capture representations across multiple timescales. The primary goal of these multi-scale architectures is to exploit the hierarchical nature of speech, where lower-resolution components aim to capture representations that align with increasingly a… ▽ More Self-supervised learning (SSL) models have become crucial in speech processing, with recent advancements concentrating on developing architectures that capture representations across multiple timescales. The primary goal of these multi-scale architectures is to exploit the hierarchical nature of speech, where lower-resolution components aim to capture representations that align with increasingly abstract concepts (e.g., from phones to words to sentences). Although multi-scale approaches have demonstrated some improvements over single-scale models, the precise reasons for these enhancements have poor empirical support. In this study, we present an initial analysis of layer-wise representations in multi-scale architectures, with a focus on Canonical Correlation Analysis (CCA) and Mutual Information (MI). We apply this analysis to Multi-Resolution HuBERT (MR-HuBERT) and find that (1) the improved performance on SUPERB tasks is primarily due to the auxiliary low-resolution loss rather than the downsampling itself, and (2) downsampling to lower resolutions neither improves downstream performance nor correlates with higher-level information (e.g., words), though it does improve computational efficiency. These findings challenge assumptions about the multi-scale nature of MR-HuBERT and motivate the importance of disentangling computational efficiency from learning better representations. △ Less

Submitted 31 October, 2024; originally announced October 2024.

ACM Class: I.2.0

Molly: A Verified Compiler for Cryptoprotocol Roles

Authors: Daniel J. Dougherty, Joshua D. Guttman

Abstract: Molly is a program that compiles cryptographic protocol roles written in a high-level notation into straight-line programs in an intermediate-level imperative language, suitable for implementation in a conventional programming language. We define a denotational semantics for protocol roles based on an axiomatization of the runtime. A notable feature of our approach is that we assume that encryptio… ▽ More Molly is a program that compiles cryptographic protocol roles written in a high-level notation into straight-line programs in an intermediate-level imperative language, suitable for implementation in a conventional programming language. We define a denotational semantics for protocol roles based on an axiomatization of the runtime. A notable feature of our approach is that we assume that encryption is randomized. Thus, at the runtime level we treat encryption as a relation rather than a function. Molly is written in Coq, and generates a machine-checked proof that the procedure it constructs is correct with respect to the runtime semantics. Using Coq's extraction mechanism, one can build an efficient functional program for compilation. △ Less

Submitted 22 November, 2023; originally announced November 2023.

Hierarchical Quantized Autoencoders

Authors: Will Williams, Sam Ringer, Tom Ash, John Hughes, David MacLeod, Jamie Dougherty

Abstract: Despite progress in training neural networks for lossy image compression, current approaches fail to maintain both perceptual quality and abstract features at very low bitrates. Encouraged by recent success in learning discrete representations with Vector Quantized Variational Autoencoders (VQ-VAEs), we motivate the use of a hierarchy of VQ-VAEs to attain high factors of compression. We show that… ▽ More Despite progress in training neural networks for lossy image compression, current approaches fail to maintain both perceptual quality and abstract features at very low bitrates. Encouraged by recent success in learning discrete representations with Vector Quantized Variational Autoencoders (VQ-VAEs), we motivate the use of a hierarchy of VQ-VAEs to attain high factors of compression. We show that the combination of stochastic quantization and hierarchical latent structure aids likelihood-based image compression. This leads us to introduce a novel objective for training hierarchical VQ-VAEs. Our resulting scheme produces a Markovian series of latent variables that reconstruct images of high-perceptual quality which retain semantically meaningful features. We provide qualitative and quantitative evaluations on the CelebA and MNIST datasets. △ Less

Submitted 16 October, 2020; v1 submitted 19 February, 2020; originally announced February 2020.

Homomorphisms and Minimality for Enrich-by-Need Security Analysis

Authors: Daniel J. Dougherty, Joshua D. Guttman, John D. Ramsdell

Abstract: Cryptographic protocols are used in different environments, but existing methods for protocol analysis focus only on the protocols, without being sensitive to assumptions about their environments. LPA is a tool which analyzes protocols in context. LPA uses two programs, cooperating with each other: CPSA, a well-known system for protocol analysis, and Razor, a model-finder based on SMT technology.… ▽ More Cryptographic protocols are used in different environments, but existing methods for protocol analysis focus only on the protocols, without being sensitive to assumptions about their environments. LPA is a tool which analyzes protocols in context. LPA uses two programs, cooperating with each other: CPSA, a well-known system for protocol analysis, and Razor, a model-finder based on SMT technology. Our analysis follows the enrich-by-need paradigm, in which models of protocol execution are generated and examined. The choice of which models to generate is important, and we motivate and evaluate LPA's strategy of building minimal models. "Minimality" can be defined with respect to either of two preorders, namely the homomorphism preorder and the embedding preorder (i.e. the preorder of injective homomorphisms); we discuss the merits of each. Our main technical contributions are algorithms for building homomorphism-minimal models and for generating a set-of-support for the models of a theory, in each case by scripting interactions with an SMT solver. △ Less

Submitted 19 April, 2018; originally announced April 2018.

A Hybrid Analysis for Security Protocols with State

Authors: John D. Ramsdell, Daniel J. Dougherty, Joshua D. Guttman, Paul D. Rowe

Abstract: Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platfo… ▽ More Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platform Modules. Sometimes it is the purpose of running the protocol, for example in commercial transactions. Many richly developed tools and techniques, based on well-understood foundations, are available for design and analysis of pure message-passing protocols. But the presence of cross-session state poses difficulties for these techniques. In this paper we provide a framework for modeling stateful protocols. We define a hybrid analysis method. It leverages theorem-proving---in this instance, the PVS prover---for reasoning about computations over state. It combines that with an "enrich-by-need" approach---embodied by CPSA---that focuses on the message-passing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan. △ Less

Submitted 16 June, 2014; v1 submitted 15 April, 2014; originally announced April 2014.

Symbolic Protocol Analysis for Diffie-Hellman

Authors: Daniel J. Dougherty, Joshua D. Guttman

Abstract: We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity… ▽ More We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies. △ Less

Submitted 9 February, 2012; originally announced February 2012.

An Improved Algorithm for Generating Database Transactions from Relational Algebra Specifications

Authors: Daniel J. Dougherty

Abstract: Alloy is a lightweight modeling formalism based on relational algebra. In prior work with Fisler, Giannakopoulos, Krishnamurthi, and Yoo, we have presented a tool, Alchemy, that compiles Alloy specifications into implementations that execute against persistent databases. The foundation of Alchemy is an algorithm for rewriting relational algebra formulas into code for database transactions. In th… ▽ More Alloy is a lightweight modeling formalism based on relational algebra. In prior work with Fisler, Giannakopoulos, Krishnamurthi, and Yoo, we have presented a tool, Alchemy, that compiles Alloy specifications into implementations that execute against persistent databases. The foundation of Alchemy is an algorithm for rewriting relational algebra formulas into code for database transactions. In this paper we report on recent progress in improving the robustness and efficiency of this transformation. △ Less

Submitted 28 March, 2010; originally announced March 2010.

Journal ref: EPTCS 21, 2010, pp. 77-89

A Low Cost Distributed Computing Approach to Pulsar Searches at a Small College

Authors: Andrew Cantino, Fronefield Crawford, Saurav Dhital, John P. Dougherty, Reid Sherman

Abstract: We describe a distributed processing cluster of inexpensive Linux machines developed jointly by the Astronomy and Computer Science departments at Haverford College which has been successfully used to search a large volume of data from a recent radio pulsar survey. Analysis of radio pulsar surveys requires significant computational resources to handle the demanding data storage and processing nee… ▽ More We describe a distributed processing cluster of inexpensive Linux machines developed jointly by the Astronomy and Computer Science departments at Haverford College which has been successfully used to search a large volume of data from a recent radio pulsar survey. Analysis of radio pulsar surveys requires significant computational resources to handle the demanding data storage and processing needs. One goal of this project was to explore issues encountered when processing a large amount of pulsar survey data with limited computational resources. This cluster, which was developed and activated in only a few weeks by supervised undergraduate summer research students, used existing decommissioned computers, the campus network, and a script-based, client-oriented, self-scheduled data distribution approach to process the data. This setup provided simplicity, efficiency, and "on-the-fly" scalability at low cost. The entire 570 GB data set from the pulsar survey was processed at Haverford over the course of a ten-week summer period using this cluster. We conclude that this cluster can serve as a useful computational model in cases where data processing must be carried out on a limited budget. We have also constructed a DVD archive of the raw survey data in order to investigate the feasibility of using DVD as an inexpensive and easily accessible raw data storage format for pulsar surveys. DVD-based storage has not been widely explored in the pulsar community, but it has several advantages. The DVD archive we have constructed is reliable, portable, inexpensive, and can be easily read by any standard modern machine. △ Less

Submitted 7 July, 2004; originally announced July 2004.

Comments: Adapted from a talk given at the Eleventh SIAM Conference on Parallel Computing, February 25-27, 2004 in San Francisco, CA. 18 pages, including 3 figures and 2 tables

ACM Class: J.2