Automated proofs of computational indistinguishability

We present a tool for automatic analysis of computational indistinguishability between two strings of information. This is designed as a generic tool for proving cryptographic security based on a formalism that provides computational soundness preservation. The tool has been implemented and tested successfully with several cryptographic schemes.

On the security of TLS renegotiation

The Transport Layer Security (TLS) protocol is the most widely used security protocol on the Internet. It supports negotiation of a wide variety of cryptographic primitives through different cipher suites, various modes of client authentication, and additional features such as renegotiation. Despite its widespread use, only recently has the full TLS protocol been proven secure, and only the core cryptographic protocol with no additional features. These additional features have been the cause of several practical attacks on TLS. In 2009, Ray and Dispensa demonstrated how TLS renegotiation allows an attacker to splice together its own session with that of a victim, resulting in a man-in-the-middle attack on TLS-reliant applications such as HTTP. TLS was subsequently patched with two defence mechanisms for protection against this attack. We present the first formal treatment of renegotiation in secure channel establishment protocols. We add optional renegotiation to the authenticated and confidential channel establishment model of Jager et al., an adaptation of the Bellare--Rogaway authenticated key exchange model. We describe the attack of Ray and Dispensa on TLS within our model. We show generically that the proposed fixes for TLS offer good protection against renegotiation attacks, and give a simple new countermeasure that provides renegotiation security for TLS even in the face of stronger adversaries.

Securing multicast groups in ad hoc networks

We propose a reliable and ubiquitous group key distribution scheme that is suitable for ad hoc networks. The scheme has self-initialisation and self-securing features. The former feature allows a cooperation of an arbitrary number of nodes to initialise the system, and it also allows node admission to be performed in a decentralised fashion. The latter feature allows a group member to determine the group key remotely while maintaining the system security. We also consider a decentralised solution of establishing secure point-to-point communication. The solution allows a new node to establish a secure channel with every existing node if it has pre-existing secure channels with a threshold number of the existing nodes.

On the leakage resilience of secure channel establishment

Secure communication channels are typically constructed from an authenticated key exchange (AKE) protocol, which authenticates the communicating parties and establishes shared secret keys, and a secure data transmission layer, which uses the secret keys to encrypt data. We address the partial leakage of communicating parties' long-term secret keys due to various side-channel attacks, and the partial leakage of plaintext due to data compression. Both issues can negatively affect the security of channel establishment and data transmission. In this work, we advance the modelling of security for AKE protocols by considering more granular partial leakage of parties' long-term secrets. We present generic and concrete constructions of two-pass leakage-resilient key exchange protocols that are secure in the proposed security models. We also examine two techniques--heuristic separation of secrets and fixed-dictionary compression--for enabling compression while protecting high-value secrets.

A cryptographic analysis of the TLS 1.3 handshake protocol candidates

The Internet Engineering Task Force (IETF) is currently developing the next version of the Transport Layer Security (TLS) protocol, version 1.3. The transparency of this standardization process allows comprehensive cryptographic analysis of the protocols prior to adoption, whereas previous TLS versions have been scrutinized in the cryptographic literature only after standardization. This is even more important as there are two related, yet slightly different, candidates in discussion for TLS 1.3, called draft-ietf-tls-tls13-05 and draft-ietf-tls-tls13-dh-based. We give a cryptographic analysis of the primary ephemeral Diffie–Hellman-based handshake protocol, which authenticates parties and establishes encryption keys, of both TLS 1.3 candidates. We show that both candidate handshakes achieve the main goal of providing secure authenticated key exchange according to an augmented multi-stage version of the Bellare–Rogaway model. Such a multi-stage approach is convenient for analyzing the design of the candidates, as they establish multiple session keys during the exchange. An important step in our analysis is to consider compositional security guarantees. We show that, since our multi-stage key exchange security notion is composable with arbitrary symmetric-key protocols, the use of session keys in the record layer protocol is safe. Moreover, since we can view the abbreviated TLS resumption procedure also as a symmetric-key protocol, our compositional analysis allows us to directly conclude security of the combined handshake with session resumption. We include a discussion on several design characteristics of the TLS 1.3 drafts based on the observations in our analysis.

Dessy : desktop search and synchronization

Current smartphones have a storage capacity of several gigabytes. More and more information is stored on mobile devices. To meet the challenge of information organization, we turn to desktop search. Users often possess multiple devices, and synchronize (subsets of) information between them. This makes file synchronization more important. This thesis presents Dessy, a desktop search and synchronization framework for mobile devices. Dessy uses desktop search techniques, such as indexing, query and index term stemming, and search relevance ranking. Dessy finds files by their content, metadata, and context information. For example, PDF files may be found by their author, subject, title, or text. EXIF data of JPEG files may be used in finding them. User–defined tags can be added to files to organize and retrieve them later. Retrieved files are ranked according to their relevance to the search query. The Dessy prototype uses the BM25 ranking function, used widely in information retrieval. Dessy provides an interface for locating files for both users and applications. Dessy is closely integrated with the Syxaw file synchronizer, which provides efficient file and metadata synchronization, optimizing network usage. Dessy supports synchronization of search results, individual files, and directory trees. It allows finding and synchronizing files that reside on remote computers, or the Internet. Dessy is designed to solve the problem of efficient mobile desktop search and synchronization, also supporting remote and Internet search. Remote searches may be carried out offline using a downloaded index, or while connected to the remote machine on a weak network. To secure user data, transmissions between the Dessy client and server are encrypted using symmetric encryption. Symmetric encryption keys are exchanged with RSA key exchange. Dessy emphasizes extensibility. Also the cryptography can be extended. Users may tag their files with context tags and control custom file metadata. Adding new indexed file types, metadata fields, ranking methods, and index types is easy. Finding files is done with virtual directories, which are views into the user’s files, browseable by regular file managers. On mobile devices, the Dessy GUI provides easy access to the search and synchronization system. This thesis includes results of Dessy synchronization and search experiments, including power usage measurements. Finally, Dessy has been designed with mobility and device constraints in mind. It requires only MIDP 2.0 Mobile Java with FileConnection support, and Java 1.5 on desktop machines.

Dissolved oxygen probes: making oxygen measurements routine like temperature, St Petersburg, Florida, January 4-6, 2006: workshop proceedings

The Alliance for Coastal Technologies (ACT) Workshop "Making Oxygen Measurements Routine Like Temperature" was convened in St. Petersburg, Florida, January 4th - 6th, 2006. This event was sponsored by the University of South Florida (USF) College of Marine Science, an ACT partner institution and co-hosted by the Ocean Research Interactive Observatory Networks (ORION). Participants from researcldacademia, resource management, industry, and engineering sectors collaborated with the aim to foster ideas and information on how to make measuring dissolved oxygen a routine part of a coastal or open ocean observing system. Plans are in motion to develop large scale ocean observing systems as part of the US Integrated Ocean Observing System (100s; see http://ocean.us) and the NSF Ocean Observatory Initiative (001; see http://www.orionprogram.org/00I/default.hl). These systems will require biological and chemical sensors that can be deployed in large numbers, with high reliability, and for extended periods of time (years). It is also likely that the development cycle for new sensors is sufficiently long enough that completely new instruments, which operate on novel principles, cannot be developed before these complex observing systems will be deployed. The most likely path to development of robust, reliable, high endurance sensors in the near future is to move the current generation of sensors to a much greater degree of readiness. The ACT Oxygen Sensor Technology Evaluation demonstrated two important facts that are related to the need for sensors. There is a suite of commercially available sensors that can, in some circumstances, generate high quality data; however, the evaluation also showed that none of the sensors were able to generate high quality data in all circumstances for even one month time periods due to biofouling issues. Many groups are attempting to use oxygen sensors in large observing programs; however, there often seems to be limited communication between these groups and they often do not have access to sophisticated engineering resources. Instrument manufacturers also do not have sufficient resources to bring sensors, which are marketable, but of limited endurance or reliability, to a higher state of readiness. The goal of this ACT/ORION Oxygen Sensor Workshop was to bring together a group of experienced oceanographers who are now deploying oxygen sensors in extended arrays along with a core of experienced and interested academic and industrial engineers, and manufacturers. The intended direction for this workshop was for this group to exchange information accumulated through a variety of sensor deployments, examine failure mechanisms and explore a variety of potential solutions to these problems. One anticipated outcome was for there to be focused recommendations to funding agencies on development needs and potential solutions for 02 sensors. (pdf contains 19 pages)

基于口令认证的密钥交换协议的安全性分析

在串空间理论模型引入了描述DH问题的方法以及分析猜测攻击的攻击者能力,对基于口令认证的密钥交换协议的安全性进行了形式化分析.提出一个对DH-EKE协议的简化,并证明了该协议的安全性:口令的秘密性,认证性,以及会话密钥的秘密性.根据分析给出基于口令认证的密钥交换协议抵抗猜测攻击的基本条件.将分析方法应用到基于口令的三方密钥交换协议上,给出单纯基于口令进行密钥交换协议的安全性需要满足的一个必要条件.

基于身份的移动网动态群组密钥协商方案

群组密钥协商是群组通信中非常重要的基本工具，如何得到一个安全有效的密钥协商协议是当前密码学研究中的一个重要问题。基于双线性对和随机预言模型，针对移动网络提出了一个动态群组密钥协商方案。此方案就计算复杂度和通信复杂度而言都是高效的，而且满足密钥协商所需耍的安全要求。

Sécurité polynomiale en cryptographie

Dans ce mémoire, nous proposons des protocoles cryptographiques d'échange de clef, de mise en gage, et de transfert équivoque. Un premier protocole de transfert équivoque, primitive cryptographique universelle pour le calcul multi-parties, s'inspire du protocole d'échange de clef par puzzle de Merkle, et améliore les résultats existants. Puis, nous montrons qu'il est possible de construire ces mêmes primitives cryptographiques sans l'hypothèse des fonctions à sens unique, mais avec le problème 3SUM. Ce problème simple ---dans une liste de n entiers, en trouver trois dont la somme a une certaine valeur--- a une borne inférieure conjecturée de Omega(n^2).

A Novel Fast Hybrid Cryptographic System: MARS4

A novel and fast technique for cryptographic applications is designed and developed using the symmetric key algorithm “MAJE4” and the popular asymmetric key algorithm “RSA”. The MAJE4 algorithm is used for encryption / decryption of files since it is much faster and occupies less memory than RSA. The RSA algorithm is used to solve the problem of key exchange as well as to accomplish scalability and message authentication. The focus is to develop a new hybrid system called MARS4 by combining the two cryptographic methods with an aim to get the advantages of both. The performance evaluation of MARS4 is done in comparison with MAJE4 and RSA.

Rerum cognoscere causas: part II - opportunities generated by the agency/structure debate and suggestions for clarifying the social theoretic position of system dynamics

This is the second half of a two-part paper dealing with the social theoretic assumptions underlying system dynamics. In the first half it was concluded that analysing system dynamics using traditional, paradigm-based social theories is highly problematic. An innovative and potentially fruitful resolution is now proposed to these problems. In the first section it is argued that in order to find an appropriate social theoretic home for system dynamics it is necessary to look to a key exchange in contemporary social science: the agency/structure debate. This debate aims to move beyond both the theories based only on the actions of individual human agents, and those theories that emphasise only structural influences. Emerging from this debate are various theories that instead aim to unite the human agent view of the social realm with views that concentrate solely on system structure. It is argued that system dynamics is best viewed as being implicitly grounded in such theories. The main conclusion is therefore that system dynamics can contribute to an important part of social thinking by providing a formal approach for explicating social mechanisms. This conclusion is of general significance for system dynamics. However, the over-arching aim of the two-part paper is to increase the understanding of system dynamics in related disciplines. Four suggestions are therefore offered for how the system dynamics method might be extended further into the social sciences. It is argued that, presented in the right way, the formal yet contingent feedback causality thinking of system dynamics should diffuse widely in the social sciences and make a distinctive and important contribution to them. Felix qui potuit rerum cognoscere causas Happy is he who comes to know the causes of things Virgil - Georgics, Book II, line 490. 29 BCE

O uso de elementos da criptografia como estímulo matemático na sala de aula

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

O uso de elementos da criptografia como estímulo matemático na sala de aula

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)