Since SSH’s standardization nearly 20 years ago, real-world requirements for a remote access protocol and our understanding of how to build secure cryptographic network protocols have both evolved significantly. In this work, we introduce Hop, a transport and remote access protocol designed to support today’s needs. Building on modern cryptographic advances, Hop reduces SSH protocol complexity and overhead while simultaneously addressing many of SSH’s shortcomings through a cryptographically-mediated delegation scheme, native host identification based on lessons from TLS and ACME, client authentication for modern enterprise environments, and support for client roaming and intermittent connectivity. We present concrete design requirements for a modern remote access protocol, describe our proposed protocol, and evaluate its performance. We hope that our work encourages discussion of what a modern remote access protocol should look like in the future.
more »
« less
This content will become publicly available on September 1, 2026
Requirement Patterns for Engineering Multiagent Interaction Protocols
An interaction protocol specifies how the member agents of a decentralized multiagent system may communicate to satisfy their respective stakeholders' requirements. We focus on information protocols, which are fully declarative specifications of interaction and support asynchronous communication. We offer Mambo, an approach for protocol design. Mambo identifies common patterns of requirements, provides a notation to express them, and a verification procedure. Mambo incorporates heuristics to generate small internal representations for efficiency. Experimental results demonstrate Mambo's effectiveness on practical protocols.
more »
« less
- Award ID(s):
- 1908374
- PAR ID:
- 10638566
- Publisher / Repository:
- International Joint Conferences on Artificial Intelligence Organization
- Date Published:
- Page Range / eLocation ID:
- 38 to 46
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Abstract Existing experimental demonstrations of quantum computational advantage have had the limitation that verifying the correctness of the quantum device requires exponentially costly classical computations. Here we propose and analyse an interactive protocol for demonstrating quantum computational advantage, which is efficiently classically verifiable. Our protocol relies on a class of cryptographic tools called trapdoor claw-free functions. Although this type of function has been applied to quantum advantage protocols before, our protocol employs a surprising connection to Bell’s inequality to avoid the need for a demanding cryptographic property called the adaptive hardcore bit, while maintaining essentially no increase in the quantum circuit complexity and no extra assumptions. Leveraging the relaxed cryptographic requirements of the protocol, we present two trapdoor claw-free function constructions, based on Rabin’s function and the Diffie–Hellman problem, which have not been used in this context before. We also present two independent innovations that improve the efficiency of our implementation and can be applied to other quantum cryptographic protocols. First, we give a scheme to discard so-called garbage bits, removing the need for reversibility in the quantum circuits. Second, we show a natural way of performing postselection that reduces the fidelity needed to demonstrate quantum advantage. Combining these results, we describe a blueprint for implementing our protocol on Rydberg atom-based quantum devices, using hardware-native operations that have already been demonstrated experimentally.more » « less
-
An interaction protocol specifies a decentralized multiagent system operationally by specifying constraints on messages exchanged by its member agents. Engineering with protocols requires support for a notion of refinement, whereby a protocol may be substituted without loss of correctness by one that refines it. We identify two desiderata for refinement. One, generality: refinement should not restrict enactments by limiting protocols or infrastructures under consideration. Two, preservation: to facilitate modular verification, refinement should preserve liveness and safety. We contribute a novel formal notion of protocol refinement based on enactments. We demonstrate generality by tackling the declarative framework of information protocols. We demonstrate preservation by formally establishing that our notion of refinement is safety and liveness preserving. We show the practical benefits of refinement by implementing a checker. We demonstrate that it is less time-intensive to check refinement (and thereby gain safety and liveness) than to recheck safety and liveness of a composition.more » « less
-
An interaction protocol specifies a decentralized multiagent system operationally by specifying constraints on messages exchanged by its member agents. Engineering with protocols requires support for a notion of refinement, whereby a protocol may be substituted without loss of correctness by one that refines it. We identify two desiderata for refinement. One, generality: refinement should not restrict enactments by limiting protocols or infrastructures under consideration. Two, preservation: to facilitate modular verification, refinement should preserve liveness and safety. We contribute a novel formal notion of protocol refinement based on enactments. We demonstrate generality by tackling the declarative framework of information protocols. We demonstrate preservation by formally establishing that our notion of refinement is safety and liveness preserving. We show the practical benefits of refinement by implementing a checker. We demonstrate that it is less time-intensive to check refinement (and thereby gain safety and liveness) than to recheck safety and liveness of a composition.more » « less
-
Studies of plant–microbe interactions using synthetic microbial communities (SynComs) often require the removal of seed-associated microbes by seed sterilization prior to inoculation to provide gnotobiotic growth conditions. Diverse seed sterilization protocols have been developed and have been used on different plant species with various amounts of validation. From these studies it has become clear that each plant species requires its own optimized sterilization protocol. It has, however, so far not been tested whether the same protocol works equally well for different varieties and seed sources of one plant species. We evaluated six seed sterilization protocols on two different varieties (Sugar Bun and B73) of maize. All unsterilized maize seeds showed fungal growth upon germination on filter paper, highlighting the need for a sterilization protocol. A short sterilization protocol with hypochlorite and ethanol was sufficient to prevent fungal growth on Sugar Bun germinants; however a longer protocol with heat treatment and germination in fungicide was needed to obtain clean B73 germinants. This difference may have arisen from the effect of either genotype or seed source. We then tested the protocol that performed best for B73 on three additional maize genotypes from four sources. Seed germination rates and fungal contamination levels varied widely by genotype and geographic source of seeds. Our study shows that consideration of both variety and seed source is important when optimizing sterilization protocols and highlights the importance of including seed source information in plant–microbe interaction studies that use sterilized seeds. [Formula: see text] Copyright © 2024 The Author(s). This is an open access article distributed under the CC BY-NC-ND 4.0 International license .more » « less
An official website of the United States government
