ABSTRACT. In this talk I'll describe how our research project into adapting formal analysis technqiues for cryptographic protocols to security APIs turned into an industry collaboration and finally a spin-off company, Cryptosense, that was created in September 2013. Though the company is still in its early stages, we've already learned a lot about the journey from academic results to commercial product. I'll talk about what we're doing now, what we're developing for the future, and what its like to transition from full time researcher to start-up CEO.

ABSTRACT. The main goal of this paper is to describe the JCAlgTest project. The JCAlgTest project is designed for an automatic testing of the degree of support for algorithms listed in the JavaCard API specification by a given smart card. Discussion of the results and trends drawn from the database of 28 different cryptographic smart cards is performed. Additional information about particular algorithm or protocol obtained via timing and power analysis is also described and (partially) available in JCAlgTest database.

ABSTRACT. We demonstrate how to use a tiny domain-specific language for the description of APIs make it possible to perform black-box testing of APIs. Given an API, our testing framework behaves like regular client code and combines functions exported by the API to build elements of the data-types that are exported by the API. Once the API has been systematically exercised, the user can verify that some properties hold at the API level. In the submitted abstract, we use the running example of data-structures APIs, but the very same ideas apply to the smart-fuzzing of security APIs.

ABSTRACT. The goal of the paper is to develop a software for automated analysis of PKCS#11 tokens with focus on the security of stored cryptographic keys. The paper first outlines the PKCS#11 standard and the Cryptoki API specified by the standard, including the various components of the API. Then the paper describes the mechanics of cryptographic key protection in Cryptoki. It analyses the individual functions relevant to key protection and defines the first set of tests. Then the paper performs an analysis of the previously published attacks against keys stored on the device and also outlines the second set of tests with focus on discovering attack vulnerabilities. Afterwards the paper examines various ways to improve the security of Cryptoki by altering the standard. The discussion of the proposed restrictions takes into consideration their impact on practical usability of the tokens. In order to further evaluate the security of the tokens against possible attacks, the paper also utilizes model checker software. The results of the previously defined tests are used to compose a model that is sent to a model checker for further analysis. Since the developed software is written in Java, the paper also examines the Java PKCS#11 wrapper and discusses the advantages and disadvantages against using C for implementation. The most obvious advantage is that the software can be easily deployed on other operating systems, which is particularly useful for testing tokens that only work on Windows. The disadvantage is that the used wrapper does not implement all the Cryptoki functions, but the paper shows that all these limitations either do not matter or they can be worked around. The paper also presents the developed tool called Caetus. The tool first connects into the token, discovers the basic capabilities of the device and based on these capabilities it performs in-depth testing of Cryptoki functions. First part of the tests focuses on adherence to the PKCS#11 standard, which means the discovered issues do not necessarily mean security risks. The other set of tests attempts to discover vulnerability of the token to the previously published attacks and other trivial attacks. Finally the tool can use the discovered capabilities in order to compose a model specification which is then sent to the model checker. The tool is currently optimized for analysis of software tokens. The last part of the paper consists of tables with results of token testing and discussion of the results.

ABSTRACT. Building an HSM out of Smartcards

ABSTRACT. This talk considers the challenges in designing a Security API for back end systems which enrol devices into a central network, such as a payments network. Since no prior relationship exists with the device, whatever the enrolment protocol, in effect it will reveal keys in clear to the endpoint upon completion.

In order to save on database space, key derivation is a common approach in financial organisations, but revelation in clear can be a problem if device keys are derived rather than randomly generated - since the same process could be repeated to reveal the same key with an unwanted party.

The talk discusses how to harmonise the desire for secure APIs that support enrolment while minimising storage requirements, and find that parametric API designs (where the API uses a configurable mixture of security mechanisms) can offer a convenient solution -- for better or worse -- when hammering out a design which will satisfy parties with differing interests within a design team. A parametric design for enrolment is presented and constrasted with previously presented parametric designs for data tokenisation.