Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Characteristics and Temporal Behavior of Internet Backbone Traffic

With the rapid increase demand for data usage, Internet has become complex and harder to analyze. Characterizing the Internet traffic might reveal information that are important for Network Operators to formulate policy decisions, develop techniques to detect network anomalies, help better provision network resources (capacity, buffers) and use workload characteristics for simulations (typical packet sizes, flow durations, common protocols). In this paper, using passive monitoring and measurements, we show collected data traffic at Internet backbone routers. First, we reveal main observations on patterns and characteristics of this dataset including packet sizes, traffic volume for inter and intra domain and protocol composition. Second, we further investigate independence structure of packet size arrivals using both visual and computational statistics. Finally, we show the temporal behavior of most active destination IP and Port addresses.

Automated Proof of Authentication Protocols in a Logic of Events

Using the language of event orderings and event classes, and using a type of atoms to represent nonces, keys, signatures, and ciphertexts, we give an axiomatization of a theory in which authentication protocols can be formally defined and strong authentication properties proven. This theory is inspired by PCL, the protocol composition logic defined by Datta, Derek, Mitchell, and Roy.We developed a general purpose <i>tactic</i> (in the NuPrl theorem prover), and applied it to automatically prove that several protocols satisfy a strong authentication property. Several unexpected subtleties exposed in this development are addressed with new concepts <i>legal protocols</i>, and a <i>fresh signature criterion</i> - and reasoning that makes use of a well-founded causal ordering on events.This work shows that proofs in a logic like PCL can be automated, provides a new and possibly simpler axiomatization for a theory of authentication, and addresses some issues raised in a critique of PCL.