Information Security Seminar 

In the research of the relationship between the formal and the computational view of cryptography, a recent approach uses static equivalence from cryptographic pi calculi as a notion of formal indistinguishability. Previous work has shown that this yields the soundness of natural interpretations of some interesting equational theories, such as certain cryptographic operations and a theory of XOR. In this paper however, we argue that static equivalence is too coarse for sound interpretations of equational theories in general. We show some explicit examples how static equivalence fails to work in interesting cases. To fix this problem, we propose a notion of formal indistinguishability that is more flexible than static equivalence. We provide a general framework along with general theorems, and then discuss how this new notion works for the explicit examples where static equivalence failed to ensure soundness. We also improve the treatment by using ordered sorts in the formal view, and by allowing arbitrary probability distributions of the interpretations. Joint work with P. Mohassel and T. Stegers.

In this work we argue that, in the perspective of developing "security-minded" programming languages, the secure information flow property should be defined (as well as disciplined access) as a standard safety property, based on a notion of a security error, namely that one should not put in a public location a value elaborated using confidential information. We show that this is the property guaranteed by a standard security type system, and that, for a simple language, it is strictly stronger than non-interference. Moreover, we show that this notion of secure information flow allows us to give natural semantics to various security-minded programming constructs, including declassification.

Classical: Protection existing in classical cryptographic systems widely used is based on keys generated by pseudo-random number generators or computational complexities (e.g., factoring large numbers into primes). However, pseudo-random sequences have formation rules and algorithms can be used or discovered to find the sequences. Also, other than historical difficulties nothing indicates that an efficient (classical) factoring algorithm cannot be found.

“One-time pad” encryption is the only classical method offering unconditional security. It uses secret symmetric keys [G. S. Vernam, J. Amer. Inst. Elec. Eng. 55, 109 (1926). C. E. Shannon, Bell Syst. Tech. J. 28, 656 (1949)] shared between two users. The difficulty to securely renew the shared keys in modern fast communications is an unsolved challenge that ruled out this technique for broad use.

Quantum: Quantum protocols, such as the well studied single-photon protocol BB84 offer outstanding protection in dedicated networks for short distances and at slow speeds . These systems do not work in generic Internet channels and networks. Good signal amplification is not possible with single photon protocols [Wootters-Zurek theorem: Wooters WK, Zurek WH, Nature, 299 (5886) 1982, 802-803] and the system security reduces to zero if signals are converted from optical to electrical and vice-versa; these conversions are necessary in generic Internet channels. Although systems using continuous variables and other schemes are constantly being proposed, there is no widely accepted vision on purely quantum systems being incorporated to the Internet. 

Systems protected by physical noise: A new class of systems was recently created based on physical noise that, even not offering unconditional security, offer security levels compatible or higher than current protocols. They do not rely on the factoring difficulty and do not need certificate centers; they are under strict control of the users, sender and receiver. They mix classical protocols and quantum noise features. They do not use single photons in entangled states. These systems were created to offer high level of security and at the same time work at high speeds compatible to modern communications. It is practical to have them classified in data encryption systems and key distribution systems.

The data encryption systems are known as alpha eta systems (and as Y00 in Japan) and were created at Northwestern University through a DARPA supported project that led to Patent No. US 7,333,611 (Feb. 19, 2008) [Assignee:  Northwestern University, Inventors: H. P. Yuen, P. Kumar, and G. A. Barbosa]. They were created to operate in fiber channels and use the intrinsic light noise associate to the signal carrier to blur the signal to the attacker while giving the legitimate users a clear signal (see patent). They operate at the physical layer of the communication networks. This kind of system has already been tested in the United States (experimental networks in Washington and currently in the DARPA Quantum Network in Boston) and Japan.  It is already being developed by a new company called NuCrypt, directed by one of the inventors (P. Kumar).

The key distribution system (patented by US-2005-0152540-A1, Inventor: G. A. Barbosa) is the main object of this talk. This system has two versions, one for fiber channels and another one to operate on the user layer. Both start with a sequence of truly random keys shared by the legitimate users. These keys are generated by a Physical Random Generator (PhRG). There is no intrinsic physical limitation for the key generation process speed. This speed may evolve according to the electronic technology advances and may follow computation and the web’s speed evolution. This is in contrast with single-photon cryptographic methods that are inherently slow.

This starting shared sequence provides the security core onto which an attacker has to brake in to obtain the fresh key sequences being constantly generated by the same PhRG and constantly shared by the users. This difficulty is easily set at a computational difficulty level well above current capabilities and is also easily adapted to any computational advances. The sequences of fresh keys shared by the users are used for fast bit-by-bit or block encryption.

Security measures have yet to be developed as well as a working prototype.

Join us in this effort. 

Some references:

Optical fiber channel:

• Fast and secure key distribution using mesoscopic coherent states of light; GA Barbosa, Phys. Rev. A 68, 052307 (2003).
• Information theory for key distribution systems secured by mesoscopic coherent states; G. A. Barbosa, Phys. Rev. A 71, 062333 (2005).

Generic Internet channel: 

• Noise Secured Internet; G. A. Barbosa, quant/ph0510011 (2005).
• Fundamentals for immediate implementation of a quantum secured Internet; G. A. Barbosa, quant-ph/0607093 v2 16 Aug 2006.
• Secure sharing of random bits over the Internet; G. A. Barbosa, quant-ph/0705.2243 v2 17 17 May 07.

 

In this talk a Secure Computing Module (SCM) for reconfigurable computing systems will be presented. The SCM provides a protected and reliable computational environment, where data security and protection against malicious attacks to the system is assured. Secure Computing (SC) is strongly based on encryption algorithms and on the attestation of the executed functions. The use of SC on reconfigurable devices has the advantage of being highly adaptable to the application and the user requirements, while providing high performances. Moreover, it is adaptable to new algorithms, protocols, and threats. Experimental results obtained by implementing the proposed SCM on a reconfigurable device FPGA suggest speedups up to 750 times, compared with software implemented algorithms, achieving throughputs above 1Gbit/s at low area cost. A novel method to attest dynamically reconfigured hardware structures is also presented. The overall results demonstrate the applicability the advantages of implementing SC on reconfigurable systems.

In the past few years it has become a central question of cryptography how relevant purely symbolic analysis of security protocols are to reality. This question can be analyzed by linking the symbolic approach to the so-called computational approach as the latter is a more detailed description of reality, involving probability and complexity theory. Several attempts have been made to link these two approaches. Unfortunately, most of them are not done with sufficient mathematical rigor, and some of the results are questionable. This time, we look at the case when symbolic analysis is done via first order logic. We review some of the basic notions, look at problems with a recent attempt (Computational PCL by Datta et al.) to provide computational semantics to the syntax, and suggest a new way of defining the semantics to avoid those problems, making use of standard notions of the theory of stochastic processes.

This talk is about ensuring confidentiality in networks. More specifically, it is about controlling information flows between subjects that have been given different security clearances, in the context of a distributed setting with code mobility. In a network setting, one cannot assume resources to be accessible by all programs at all times. In fact, a network can be seen as a collection of sites where conditions for computation to occur are not guaranteed by one site alone. New security leaks, that we call migration leaks, arise from the fact that execution or suspension of programs now depend on the position of resources over the network, which may in turn depend on secret information.<br /> In order to deal with migration leaks, we will consider the non-disclosure policy for networks, a generalization of non-interference that handles declassification in a network setting, and see how to enforce it over an expressive distributed calculus, by means of a type and effect system.

From small pilots to nation wide adoption Electronic Voting is appearing all over the world. However, there is no consensus about the benefits and dangers of electronic voting, namely among machine vendors and university researchers. This presentation on electronic voting is divided into two parts. First, we will introduce the main research fields of cryptographic electronic voting protocols that emerge over the last 25 years. Then, we will present the work we have been developing at the Distributed Systems Group of INESC-ID for the last 5 years, namely we will present the REVS voting system and the CodeVoting technique that aims to provide protection against automatic vote manipulation in uncontrolled environments, e.g. remote voting from home.

We present a fair contract signing protocol without communication with a judge during the exchange phase. To this end we use particular Werner states and assume that the agents have no control over the system decoherence. Finally, we show how to implement such Werner states and discuss some limitations and extensions of the proposed protocol (joint work with J. Bouda and N. Paunkovic).

We will discuss automatic verification of liveness properties in security protocols. Liveness properties only hold in general in the Dolev-Yao intruder model if at least some communication channels are resilient. However, the complexity of the resilient communication channels assumption, when used as a fairness constraint, indicates that the Dolev-Yao model is not suitable for automatic verification of liveness properties. Here we present a modified Dolev-Yao intruder that is more suitable for verifying liveness properties. As an application, formal verification of fair exchange protocols is discussed.

We define cryptographic primitives for the pi-calculus extended with polyadic synchronisation (epi), and show that these primitives are derivable constructs, i.e., epi with cryptographic primitives may be fully abstractly encoded in the regular epi calculus. The proposed encoding is sound and complete wrt barbed congruence, which, as we also show, coincides with early bisimilarity. Furthermore, we thoroughly study the behavioural theory of epi (joint work with Joana Martinho).

O que se fez, até hoje, no domínio da criptografia histórica em Portugal? Quais os mais antigos testemunhos da utilização da linguagem criptográfica em Portugal: as suas características e o seu nível de segurança, comparativamente ao que podemos observar, na mesma época, em alguns outros estados europeus. Problemas e projectos no domínio dos estudos da criptografia histórica em Portugal.

Confidentiality and integrity properties in language-based security are specified with the help of a set of security levels, and a partial order that describes permitted flows of information. Security levels associated to variables of programs describe different policies specifying e.g. who can read (confidentiality) and who can write (integrity) a given piece of data. Preservation of specified confidentiality and integrity policies associated with variables can be proved using the definition of non-interference that states that the attacker knowledge is not augmented by execution of programs.
In a distributed setting, a permitted flow of information from one variable to another variable may require communication over untrusted channels, e.g. shared memory that can be access (read and modify) by active adversaries. In this case, primitives for encryption and signing are necessary. However, classical non-interference properties are too strict to express that attacker knowledge is not augmented by execution of programs with cryptography. Hence preservation of specified confidentiality and integrity policies cannot be proved using non-interference. Computational non-interference allows one to specify preservation of confidentiality and integrity properties, using computational hypotheses about the cryptography used in the language.
In this work we propose a sound translation from programs with private communication satisfying non-interference to programs with shared-memory communication and cryptography. To this end, we propose type systems for each language, and prove that the translation is typability preserving. Joint work with Cédric Fournet, Microsoft Research Cambridge.