skip to main content


This content will become publicly available on January 8, 2025

Title: A User Experience Study of MeetingMayhem: a Web-Based Game to Teach Adversarial Thinking
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
Award ID(s):
2138921
NSF-PAR ID:
10507952
Author(s) / Creator(s):
; ; ; ; ; ;
Publisher / Repository:
ACM
Date Published:
Journal Name:
Proceedings of the ACM conference on Innovation and Technology in Computer Science Education (ITiCSE),
Subject(s) / Keyword(s):
["cybersecurity education","educational game","network security"]
Format(s):
Medium: X
Location:
Milan, Italy
Sponsoring Org:
National Science Foundation
More Like this
  1. 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
  2. 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
  3. Security is a critical aspect in the design, development, and testing of software systems. Due to the increasing need for security-related skills within software systems and engineering, there is a growing demand for these skills to be taught at the university level. A series of 41 security modules was developed to assess the impact of these modules on teaching critical cyber security topics to students. This paper presents the implementation and outcomes of the first set of six security modules in a Freshman level course. This set consists of five modules presented in lectures as well as a sixth module emphasizing encryption and decryption used as the semester project for the course. Each module is a collection of concepts related to cyber security. The individual cyber security concepts are presented with a general description of a security issue to avoid, sample code with the security issue written in the Java programming language, and a second version of the code with an effective solution. The set of these modules was implemented in Computer Science I during the Fall 2019 semester. Incorporating each of the concepts in these modules into lectures depends on both the topic covered and the approach to resolving the related security issue. Students were introduced to computing concepts related to both the security issue and the appropriate solution to fully grasp the overall concept. After presenting the materials to students, continual review with students is also essential. This reviewal process requires exploring use-cases for the programming mechanisms presented as solutions to the security issues discussed. In addition to the security modules presented in lectures, students were given a hands-on approach to understanding the concepts through Model-Eliciting Activities (MEAs). MEAs are open-ended, problem-solving activities in which groups of three to four students work to solve realistic complex problems in a classroom setting. The semester project related to encryption and decryption was implemented into the course as an MEA. To assess the effectiveness of incorporating security modules with the MEA project into the curriculum of Computer Science I, two sections of the course were used as a control group and a treatment group. The treatment group included the security modules in lectures and the MEA project while the control group did not. To measure the overall effectiveness of incorporating security modules with the MEA project, both the instructor’s effectiveness as well as the student’s attitudes and interest were measured. For instructors, the primary question to address was to what extent do instructors change their attitudes towards student learning and their teaching practices because of the implementation of cyber security modules through MEAs. For students, the primary question to address was how the inclusion of security modules with the MEA project improved their understanding of the course materials and their interests in computer science. After implementing security modules with the MEA project, students showed a better understanding of cyber security concepts and a greater interest in broader computer science concepts. The instructor’s beliefs about teaching, learning, and assessment shifted from teacher-centered to student-centered, during his experience with the security modules and MEA. 
    more » « less
  4. Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limitedin scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Gregoire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPAPKE (Gentry et al., STOC 2008), (Hierarchical) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the non-commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs. 
    more » « less
  5. Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limited in scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Gre ́goire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPA- PKE (Gentry et al., STOC 2008), (Hierarchical) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the (non-)commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs. 
    more » « less