-
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.
-
Multi-Wavelength Variability of BL Lacertae Measured with High Time Resolution
Authors:
Zachary R. Weaver,
K. E. Williamson,
S. G. Jorstad,
A. P. Marscher,
V. M. Larionov,
C. M. Raiteri,
M. Villata,
J. A. Acosta-Pulido,
R. Bachev,
G. V. Baida,
T. J. Balonek,
E. Benitez,
G. A. Borman,
V. Bozhilov,
M. I. Carnerero,
D. Carosati,
W. P. Chen,
G. Damljanovic,
V. Dhiman,
D. J. Dougherty,
S. A. Ehgamberdiev,
T. S. Grishina,
A. C. Gupta,
M. Hart,
D. Hiriart
, et al. (32 additional authors not shown)
Abstract:
In an effort to locate the sites of emission at different frequencies and physical processes causing variability in blazar jets, we have obtained high time-resolution observations of BL Lacertae over a wide wavelength range: with the \emph{Transiting Exoplanet Survey Satellite} (TESS) at 6,000-10,000 Å with 2-minute cadence; with the Neil Gehrels \emph{Swift} satellite at optical, UV, and X-ray ba…
▽ More
In an effort to locate the sites of emission at different frequencies and physical processes causing variability in blazar jets, we have obtained high time-resolution observations of BL Lacertae over a wide wavelength range: with the \emph{Transiting Exoplanet Survey Satellite} (TESS) at 6,000-10,000 Å with 2-minute cadence; with the Neil Gehrels \emph{Swift} satellite at optical, UV, and X-ray bands; with the Nuclear Spectroscopic Telescope Array at hard X-ray bands; with the \emph{Fermi} Large Area Telescope at $γ$-ray energies; and with the Whole Earth Blazar Telescope for measurement of the optical flux density and polarization. All light curves are correlated, with similar structure on timescales from hours to days. The shortest timescale of variability at optical frequencies observed with TESS is $\sim 0.5$ hr. The most common timescale is $13\pm1$~hr, comparable with the minimum timescale of X-ray variability, 14.5 hr. The multi-wavelength variability properties cannot be explained by a change solely in the Doppler factor of the emitting plasma. The polarization behavior implies that there are both ordered and turbulent components to the magnetic field in the jet. Correlation analysis indicates that the X-ray variations lag behind the $γ$-ray and optical light curves by up to $\sim 0.4$ days. The timescales of variability, cross-frequency lags, and polarization properties can be explained by turbulent plasma that is energized by a shock in the jet and subsequently loses energy to synchrotron and inverse Compton radiation in a magnetic field of strength $\sim3$ G
△ Less
Submitted 15 July, 2020;
originally announced July 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.
