skip to main content

Attention:

The NSF Public Access Repository (NSF-PAR) system and access will be unavailable from 11:00 PM ET on Thursday, May 23 until 2:00 AM ET on Friday, May 24 due to maintenance. We apologize for the inconvenience.


Search for: All records

Creators/Authors contains: "Sherman, Alan T."

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. We present the first formal-methods analysis of the Session Binding Proxy (SBP) protocol, which protects a vulnerable system by wrapping it and introducing a reverse proxy between the system and its clients. SBP mitigates thefts of authentication cookies by cryptographically binding the authentication cookie---issued by the server to the client---to an underlying Transport Layer Security (TLS) channel using the channel's master secret and a secret key known only by the proxy. An adversary who steals a bound cookie cannot reuse this cookie to create malicious requests on a separate connection because the cookie's channel binding will not match the adversary's channel. SBP seeks to achieve this goal without modifications to the client or the server software, rendering the client and server ``oblivious protocol participants'' that are not aware of the SBP session. Our analysis verifies that the original SBP design mitigates cookie stealing under the client's cryptographic assumptions but fails to authenticate the client to the proxy. Resulting from two issues, the proxy has no assurance that it shares a session context with a legitimate client: SBP assumes an older flawed version of TLS (1.2), and SBP relies on legacy server usernames and passwords to authenticate clients. Due to these issues, there is no guarantee of cookie-stealing resistance from the proxy's cryptographic perspective. Using the Cryptographic Protocol Shapes Analyzer (CPSA), we model and analyze the original SBP and three variations in the Dolev-Yao network intruder model. Our models differ in the version of TLS they use: 1.2 (original SBP), 1.2 with mutual authentication, 1.3, and {\it 1.3 with mutual authentication (mTLS-1.3)}. For comparison, we also analyze a model of the baseline scenario without SBP. We separately analyze each of our SBP models from two perspectives: client and proxy. In each SBP model, the client has assurance that the cookie is valid only for the client's legitimate session. Only in mTLS-1.3 does the proxy have assurance that it communicates with a legitimate client and that the client's cookie is valid. We formalize these results by stating and proving, or disproving, security goals for each model. SBP is useful because it provides a practical solution to the important challenge of protecting flawed legacy systems that cannot be patched. Our analysis of this obscure protocol sheds insight into the properties necessary for wrapper protocols to resist a Dolev-Yao adversary. When engineering wrapper protocols, designers must carefully consider authentication, freshness, and requirements of cryptographic bindings such as channel bindings. Our work exposes strengths and limitations of wrapper protocols and TLS channel bindings. 
    more » « less
    Free, publicly-accessible full text available January 8, 2025
  2. The game is intended for students who do not necessarily have any prior background in computer science. Assuming the role of agents, two players exchange messages over a network to try to agree on a meeting time and location, while an adversary interferes with their plan. Following the Dolev-Yao model, the adversary has full control of the network: they can see all messages and modify, block, or forward them. We designed the game as a web application, where groups of three students play the game, taking turns being the adversary. The adversary is a legitimate communicant on the network, and the agents do not know who is the other agent and who is the adversary. Through gameplay, we expect students to be able to (1) identify the dangers of communicating through a computer network, (2) describe the capabilities of a Dolev-Yao adversary, and (3) apply three cryptographic primitives: symmetric encryption, asymmetric encryption, and digital signatures. We conducted surveys, focus groups, and interviews to evaluate the effectiveness of the game in achieving the learning objectives. The game helped students achieve the first two learning objectives, as well as using symmetric encryption. We found that students enjoyed playing MeetingMayhem. We are revising MeetingMayhem to improve its user interface and to better support students to learn about asymmetric encryption and digital signatures. 
    more » « less
    Free, publicly-accessible full text available January 8, 2025
  3. s a case study in cryptographic binding, we present a formal-methods analysis of the Fast IDentity Online (FIDO) Universal Authentication Framework (UAF) authentication protocol's cryptographic channel binding mechanisms. First, we show that UAF's channel bindings fail to mitigate protocol interaction by a Dolev-Yao (DY) adversary, enabling the adversary to transfer the server's authentication challenge to alternate sessions of the protocol. As a result, in some contexts, the adversary can masquerade as a client and establish an authenticated session with a server, which might be a bank server. Second, we implement a proof-of-concept man-in-the-middle attack against eBay's open source FIDO UAF implementation. Third, we propose and verify an improvement of UAF channel binding that better resists protocol interaction, in which the client and the server, rather than the client alone, bind the server's challenge to the session. The weakness we analyze is similar to the vulnerability discovered in the Needham-Schroeder protocol over 25 years ago. That this vulnerability appears in FIDO UAF highlights the strong need for protocol designers to bind messages properly and to analyze their designs with formal-methods tools. UAF's channel bindings fail for four reasons: channel binding is optional; the client cannot authenticate the server's challenge, even when channel binding is used; the standard permits the server to accept incorrect channel bindings; and the protocol binds only to the communication endpoints and not to the protocol session. We carry out our analysis of the standard and our suggested improvement using the Cryptographic Protocol Shapes Analyzer (CPSA). To our knowledge, we are first to carry out a formal-methods analysis of channel binding in FIDO UAF, first to identify the structural weakness resulting from improper binding, and first to exhibit details of an attack resulting from this weakness. In FIDO UAF, the client can cryptographically bind protocol data (including a server-generated authentication challenge) to the underlying authenticated communication channel. To facilitate the protocol's adoption, the FIDO Alliance makes the channel binding optional and allows a server to accept incorrect channel bindings, such as when the client communicates through a network perimeter proxy. Practitioners should be aware that, when omitting channel binding or accepting incorrect channel bindings, FIDO UAF is vulnerable to a protocol-interaction attack in which the adversary tricks the client and authenticator to act as confused deputies to sign an authentication challenge for the adversary. In addition to enabling the server to verify the client's binding of the challenge to the channel, our improved mandatory dual channel-binding mechanism provides the following two advantages: (1) By binding the challenge to the channel, the server provides an opportunity for the client to verify this binding. By contrast, in the current standard, the client cannot authenticate the server's challenge. (2) It performs binding at the server where the authentication challenge is created, hindering an adversary from transplanting the challenge into another protocol execution. Our case study illustrates the importance of cryptographically binding context to protocol messages to prevent an adversary from misusing messages out of context. 
    more » « less
    Free, publicly-accessible full text available July 19, 2024
  4. We present a psychometric evaluation of the Cybersecurity Curriculum Assessment (CCA), completed by 193 students from seven colleges and universities. The CCA builds on our prior work developing and validating a Cybersecurity Concept Inventory (CCI), which measures students' conceptual understanding of cybersecurity after a first course in the area. The CCA deepens the conceptual complexity and technical depth expectations, assessing conceptual knowledge of students who had completed multiple courses in cybersecurity. We review our development of the CCA and present our evaluation of the instrument using Classical Test Theory and Item-Response Theory. The CCA is a difficult assessment, providing reliable measurements of student knowledge and deeper information about high-performing students. 
    more » « less
  5. We solve a long-standing challenge to the integrity of votes cast without the supervision of a voting booth: ``{\it improper influence},'' which typically refers to any combination of vote buying and voter coercion. Our approach allows each voter, or their trusted agents (which we call ``{\it hedgehogs}''), to {\it ``nullify''} (effectively cancel) their vote in a way that is unstoppable, irrevocable, and forever unattributable to the voter. In particular, our approach enhances security of online, remote, public-sector elections, for which there is a growing need and the threat of improper influence is most acute. We introduce the new approach, give detailed cryptographic protocols, show how it can be applied to several voting settings, and describe our implementation. The protocols compose a full voting system, which we call {\it {\votexx}}, including registration, voting, nullification, and tallying---using an anonymous communication system for registration, vote casting, and other communication in the system. We demonstrate how the technique can be applied to known systems, including where ballots can be mailed to voters and voters use codes on the ballot to cast their votes online. In comparison with previous proposals, our system makes fewer assumptions and protects against a strong adversary who learns all of the voter's keys. In {\votexx}, each voter has two public-private key pairs. Without revealing their private keys, each voter registers their public keys with the election authority. Each voter may share their keys with one or more hedgehogs. During nullification, the voter, or one or more of their hedgehogs, can interact through the anonymous communication system to nullify a vote by proving knowledge of one of the voter's private keys via a zero-knowledge proof without revealing the private key. We describe a fully decentralizable implementation of {\votexx}, including its public bulletin board, which could be implemented on a blockchain. 
    more » « less
  6. We present a psychometric evaluation of a revised version of the Cybersecurity Concept Inventory (CCI) , completed by 354 students from 29 colleges and universities. The CCI is a conceptual test of understanding created to enable research on instruction quality in cybersecurity education. This work extends previous expert review and small-scale pilot testing of the CCI. Results show that the CCI aligns with a curriculum many instructors expect from an introductory cybersecurity course, and that it is a valid and reliable tool for assessing what conceptual cybersecurity knowledge students learned. 
    more » « less
  7. We explore shadow information technology (IT) at institutions of higher education through a two-tiered approach involving a detailed case study and comprehensive survey of IT professionals. In its many forms, shadow IT is the software or hardware present in a computer system or network that lies outside the typical review process of the responsible IT unit. We carry out a case study of an internally built legacy grants management system at the University of Maryland, Baltimore County that exemplifies the vulnerabilities, including cross-site scripting and SQL injection, typical of such unauthorized and ad-hoc software. We also conduct a survey of IT professionals at universities, colleges, and community colleges that reveals new and actionable information regarding the prevalence, usage patterns, types, benefits, and risks of shadow IT at their respective institutions. Further, we propose a security-based profile of shadow IT, involving a subset of elements from existing shadow IT taxonomies, which categorizes shadow IT from a security perspective. Based on this profile, survey respondents identified the predominant form of shadow IT at their institutions, revealing close similarities to findings from our case study. Through this work, we are the first to identify possible susceptibility factors associated with the occurrence of shadow IT related security incidents within academic institutions. Correlations of significance include the presence of certain graduate schools, the level of decentralization of the IT department, the types of shadow IT present, the percentage of security violations related to shadow IT, and the institution's overall attitude toward shadow IT. The combined elements of our case study, profile, and survey provide the first multifaceted view of shadow IT security at academic institutions, highlighting tension between its risks and benefits, and suggesting strategies for managing it successfully. 
    more » « less
  8. We present and analyze UDM, a new protocol for user discovery in anonymous communication systems that minimizes the information disclosed to the system and users. Unlike existing systems, including those based on private set intersection, UDM learns nothing about the contact lists and social graphs of the users, is not vulnerable to off-line dictionary attacks that expose contact lists, does not reveal platform identifiers to users without the owner’s explicit permission, and enjoys low computation and communication complexity. UDM solves the following user-discovery problem. User Alice wishes to communicate with Bob over an anonymous communication system, such as cMix or Tor. Initially, each party knows each other’s public contact identifier (e.g., email address or phone number), but neither knows the other’s private platform identifier in the communication system. If both parties wish to communicate with each other, UDM enables them to establish a shared key and learn each other’s private platform identifier. UDM uses an untrusted user-discovery system, which processes and stores only public information, hashed values, or values encrypted with keys it does not know. Therefore, UDM cannot learn any information about the social graphs of its users. Using the anonymous communication system, each pair of users who wish to communicate with each other uploads to the user-discovery system their private platform identifier, encrypted with their shared key. Indexing their request by a truncated cryptographic hash of their shared key, each user can then download each other’s encrypted private platform identifier. 
    more » « less
  9. null (Ed.)
    We introduce AOT, an anonymous communication system based on mix network architecture that uses oblivious transfer (OT) to deliver messages. Using OT to deliver messages helps AOT resist blending (n-1) attacks and helps AOT preserve receiver anonymity, even if a covert adversary controls all nodes in AOT. AOT comprises three levels of nodes, where nodes at each level perform a different function and can scale horizontally. The sender encrypts their payload and a tag---derived from a secret shared between the sender and receiver---with the public key of a Level-2 node and sends them to a Level-1 node. On a public bulletin board, Level-3 nodes publish tags associated with messages ready to be retrieved. Each receiver checks the bulletin board, identifies tags, and receives the associated messages using OT. A receiver can receive their messages even if the receiver is offline when messages are ready. Through what we call a ``handshake'' process, communicants can use the AOT protocol to establish shared secrets anonymously. Users play an active role in contributing to the unlinkability of messages: periodically, users initiate requests to AOT to receive dummy messages, such that an adversary cannot distinguish real and dummy requests. 
    more » « less