Security Standardisation Research

QUIC is a secure transport protocol developed by Google. Lychev et al. proposed a security model (QACCE model) to capture the security of QUIC. However, the QACCE model is very complicated, and it is not clear if security requirements for QUIC are appropriately defined. In this paper, we show the first formal analysis result of QUIC using automated security verification tool ProVerif. Our symbolic model formalizes the QACCE model and the specification of QUIC. As the result of the verification, we find three attacks against QUIC in the QACCE model. It means that the Lychev et al.’s security proofs are not correct. We discuss why such attacks occur, and clarify there are unnecessarily strong points in the QACCE model. Finally, we give a way to improve the QACCE model to exactly address the appropriate security requirements.

Formal protocol analysis tools provide objective evidence that a protocol under standardization meets security goals, as well as counterexamples to goals it does not meet (“attacks”). Different tools are however based on different execution semantics and adversary models. If different tools are applied to alternative protocols under standardization, can formal evidence offer a yardstick to compare the results?

We propose a family of languages within first order predicate logic to formalize protocol safety goals (rather than indistinguishability). Although they were originally designed for the strand space formalism that supports the tool cpsa, we show how to translate them to goals for the applied \(\pi \) calculus that supports the tool ProVerif. We give a criterion for protocols expressed in the two formalisms to correspond, and prove that if a protocol in the strand space formalism satisfies a goal, then a corresponding applied \(\pi \) process satisfies the translation of that goal. We show that the converse also holds for a class of goal formulas, and conjecture a broader equivalence. We also describe a compiler that, from any protocol in the strand space formalism, constructs a corresponding applied \(\pi \) process and the relevant goal translation.

GlobalPlatform (GP) card specifications are the de facto standards for the industry of smart cards. Being highly sensitive, GP specifications were defined regarding stringent security requirements. In this paper, we analyze the cryptographic core of these requirements; i.e. the family of Secure Channel Protocols (SCP). Our main results are twofold. First, we demonstrate a theoretical attack against SCP02, which is the most popular protocol in the SCP family. We discuss the scope of our attack by presenting an actual scenario in which a malicious entity can exploit it in order to recover encrypted messages. Second, we investigate the security of SCP03 that was introduced as an amendment in 2009. We find that it provably satisfies strong notions of security. Of particular interest, we prove that SCP03 withstands algorithm substitution attacks (ASAs) defined by Bellare et al. that may lead to secret mass surveillance. Our findings highlight the great value of the paradigm of provable security for standards and certification, since unlike extensive evaluation, it formally guarantees the absence of security flaws.

Due to this inconsistency between the implementation and the standards, we show an attack that may compromise the user’s privacy by collecting the user’s payment details. We design and implement a malicious app simulating an NFC card which the user needs to install on her phone. When she aims to pay contactlessly while placing her card close to her phone, this app engages with the terminal before the card does. The experiments show that even when the terminal detects a card collision (the app essentially acts like a card), it proceeds with the EMV protocol. We show the app can retrieve from the terminal the transaction data, which include information about the payment such as the amount and date. The experimental results show that our app can effectively spy on contactless payment transactions, winning the race condition caused by card collisions around 66 % when testing with different cards. By suggesting these attacks we raise awareness of privacy and security issues in the specifications, standardisation and implementations of contactless cards and readers.

Due to the success of formal modeling of protocols such as TLS, there is a revival of interest in applying formal modeling to standardized APIs. We argue that formal modeling should happen as the standard is being developed (not afterwards) as it can detect complex or even simple attacks that the standardization group may not otherwise detect. As a case example of this, we discuss in detail the W3C Web Cryptography API. We demonstrate how a formal analysis of the API using the modeling language AVISPA with a SAT solver demonstrates that while the API has no errors in basic API operations and maintains its security properties for the most part, there are nonetheless attacks on secret key material due to how key wrapping and usages are implemented. Furthermore, there were a number of basic problems in terms of algorithm selection and a weakness that led to a padding attack. The results of this study led to the removal of algorithms before its completed standardization and the removal of the padding attack via normalization of error codes, although the key wrapping attack is still open. We expect this sort of formal methodology to be applied to new standardization efforts at the W3C such as the W3C Web Authentication API.

In the development of TLS 1.3, the IETF TLS Working Group has adopted an “analysis-prior-to-deployment” design philosophy. This is in sharp contrast to all previous versions of the protocol. We present an account of the TLS standardisation narrative, examining the differences between the reactive standardisation process for TLS 1.2 and below, and the more proactive standardisation process for TLS 1.3. We explore the possible factors that have contributed to the shift in the TLS WG’s design mindset, considering the protocol analysis tools available, the levels of academic involvement and the incentives governing relevant stakeholders at the time of standardisation. In an attempt to place TLS within the broader realm of standardisation, we perform a comparative analysis of standardisation models and discuss the standardisation of TLS within this context.

Secure data sharing between computational systems is a necessity to many workflows across domains such as healthcare informatics, law enforcement and national security. While there exist many approaches towards securing data for the purpose of dissemination, the vast majority follows the traditional thought of security engineering that occurs as the last step of the overall software engineering process. In this paper we extend the Unified Modeling Language (UML) standard to: (1) modeling tree-structured data and associated schemas and (2) information security via role-based, lattice-based, and discretionary access control; both push it towards the forefront of the software development life-cycle. Tree structured data and associated schemas are dominant in information modeling and exchange formats including: the eXtensible Markup Language (XML), JavaScript Object Notation (JSON), etc. New UML artifacts for tree-structured data and schemas would allow the modeling of generalized information solutions from which XML, JSON, RDF, etc., could be generated; this is akin to generating different object-oriented programming language code from UML class diagrams. This UML extension also allows security experts to model and define information security requirements at the schema level as well, before code is written. The end-result is the assurance of information security for the purpose of sharing across computational systems.

The extended access control protocol has been used for the German identity card since November 2010, primarily to establish a cryptographic key between a card and a service provider and to authenticate the partners. The protocol is also referenced by the International Civil Aviation Organization for machine readable travel documents (Document 9303) as an option, and it is a candidate for the future European eIDAS identity system. Here we show that the system can be used to build a secure access system which operates in various settings (e.g., integrated, distributed, or authentication-service based architectures), and where access can be granted based on card’s attributes. In particular we prove the protocols to provide strong cryptographic guarantees, including privacy of the attributes against outsiders.

Controlling a large number of devices such as sensors and smart end points, is always a challenge where scalability and security are indispensable. This is even more important when it comes to periodic configuration updates to a large number of such devices belonging to one or more groups. One solution could be to take a group of devices as a unit of control and then manage them through a group communication mechanism. An obvious challenge to this approach is how to create such groups dynamically and manage them securely. Moreover, there need to be mechanisms in place by which members of the group can be removed and added dynamically. In this paper, we propose a technique that has been recently standardized in IEEE 802.21 (IEEE Std 802.21d™-2015) with the objective of providing a standard-based solution to the above challenges. The approach relies on Logical Key Hierarchy (LKH) based key distribution mechanism but optimizes the number of encryption and decryption by using “Complete Subtree”. It leverages IEEE 802.21 framework, services, and protocol for communication and management, and provides a scalable and secure way to manage (e.g., add and remove) devices from one or more groups. We describe the group key distribution protocol in details and provide a security analysis of the scheme along with some performance results from a prototype implementation.

We analyze the concrete security of a hash-based signature scheme described in a recent series of Internet Drafts by McGrew and Curcio. We show that an original version of their proposal achieves only a “loose” security bound, but that the latest version can be proven to have tighter security in the random-oracle model.