Password Authenticated Key Exchange in a Group

Today, we release a new paper entitled “The Fairy-Ring Dance: Password Authenticated Key Exchange in a Group“. This is joint work with Xun Yi (RMIT University), Liqun Chen (HP Labs) and Siamak Shahandashti (Newcastle University). The initial work started when Xun visited us at the School of Computing Science, Newcastle University in Feb, 2014. This is one of the collaborative research outcomes, which stem from that visit.

The subject of two-party Password Authenticated Key Exchange (PAKE) has been well studied for nearly three decades, however the topic of multi-party Group PAKE (GPAKE) has so far received little attention. Partly, this is because a Group PAKE is significantly more complex to design than a two-party PAKE due to more interactions between participants, hence exposing more potential attack vectors for an adversary to exploit.

We decided to investigate this subject as we believed Group PAKE protocols would become increasingly more important in the next 10 years – especially in the era of Internet of Things (IoT). Using a Group PAKE protocol can help set up a group of out-of-box IoT devices that have no pre-installed secrets or certificates; one just needs to enter a common (low-entropy) passcode into each of the devices. The protocol can then take over to ensure secure group communication among these IoT devices despite that all data is transmitted through an insecure Internet.

One major technical challenge here is to make the protocol as round efficient as possible. With Moore’s law, the computational efficiency can rapidly improve over time, but the round efficiency will stay more or less the same. Intuitively, when a group of entities engage in multiple rounds of interactions over a distributed network, the bottleneck of the overall latency will likely be determined by the slowest responder in each round. Hence, our strategy is to trade off computation for optimal round efficiency, with the aim to minimize the number of rounds as much as possible.

The paper (a free copy available at IACR ePrint) gives more technical details about how the above strategy is realized. I’ll present the paper at the ASIACCS Workshop on IoT Privacy, Trust, and Security (IoTPTS), in April 2015. It will be interesting to hear feedback from academic and industrial researchers working on IoT.

Before reading the paper, I would suggest the reader to watch the following “Fairy Ring Dance” from YouTube first, since the structural design of our solution shares some similarity to that dance.

Fairy Ring Dance (YouTube)

 

How much do you trust your own software?

On my recent trip to Arizona for CCS 2014 I took some time out to fly paragliders in the desert with Arizona Paragliding. Turns out that they also design and manufacture the SlingMachine towing winch that is used to transport paraglider pilots safely the desert floor to 3,000 feet in a matter of minutes. When I arrived Sean Buckner the designer and creator of SlingMachine was in the process of automating the towing winch. Sean had already designed and built the electronics for the automated control system on the SlingMachine and I helped design and build the software for the automated control box.

This is me being towed to into the air by the SlingMachine controlled by software designed and written by myself and Sean Buckner:

Paraglider being towed using SlingMachines software

It felt amazing to be towed into the air by my own software and when we perfected the software I could to actually feel changes we were making to the software.

This is very cool but you may be wondering how is this relevant to software reliability and security; the end goal of the project is to develop embedded devices (hardware and software) that put some science into improving the safety of paragliding as a sport.

We have made a start by creating an automated control box (with associated software) for the SlingMachines winch. The automated control box makes the towing process more repeatable (delivering the same tow every time) and thereby safer because it is less prone to certain categories of operator error. We are also developing a pilot telemetry pack to increase pilot safety on the towing line and a novice pilot telemetry pack to help with pilot safety during training flights.

This blog entry about what I feel is a cool software project with obvious safety and reliability issues. It is also a call for help, to the members of the Secure and Reliant Systems (SRS) and Centre for Software Reliability (CSR), we are continuing to develop the software and create new projects that are designed to improve safety in paragliding.

So my question to you guys, is how do we development ultra-reliable software, quickly with minimal manpower?

What does the software do?

The software we wrote controls the winch towing the paraglider pilot into the air, and as the pilot on the end of the tow line you want to know that the software is going to perform reliably and not do anything unexpected.

We only had a short time to implement the software and very limited manpower, this creates a problem as high integrity software development techniques significantly increase the development time / manpower required. So we had to get smart to develop highly reliable software in a rapid application development (RAD) scenario. To achieve this we applied these six principles:

  1. Human operator override; this is an essential safety feature in our approach to developing and testing the software. The human tow operator can, at any point, flick a switch to override the software and take control of the towing process. Just like the pilot on modern jet liner who has the ability to override the autopilot when the situation exceeds the conditions the autopilot can deal with. In both systems the human is the final safety backstop.
  2. Keep it simple; don’t over complicate the software.
  3. Build test environment for the control box; this consisted of a set of potentiometers and switches that replicated the inputs of the sensors on the SlingMachine winch. We could set the dials to replicate any given situation on a tow without actually launching a glider.
  4. Split the software into small self contained functional elements, each of which can be implemented and tested separately. We would complete each element and lock it off before moving onto the next.
  5. Test, test and test again… structured edge case testing allows us to repeatedly test situations that may only occur once in a thousand tows. This means that when that 1 in 1,000 case occurs the software will handle it.
    To achieve this we built a static test environment for the control box, which mimicked the input from the sensors on the towing winch using potentiometers and switches. The test environment allows us to set up those 1 in 1000 scenarios on the bench rather than in the field.
  6. Good old fashioned debug text output; the Arduino micro controller, on which the software was built, can output a constant stream of debug text over the serial line to a PC which records the data. This gives us a text log of each line of code the Arduino runs. We can then analyse the test log after each test run to verify that the software operated as expected given the inputs from the tow operator and the pressures exerted on the tow line by the glider pilot.

Our strategy delivered ultra reliable software in a very short time with minimal manpower resources. However this does pose a very important the question; was the quality of the software we produced improved by the fact that we were flying the test flights towed by our own software?

Software Design

The physical design of the SlingMachine is based on a variable friction tow line pay out systems. This design means that when the glider exerts more force on the tow line the winch will increase the rate at which the tow line is released thereby smoothing out towing experience for the paraglider pilot.

In addition the skill and experience of the towing operators Sean and Abe Heward ensures a safe and smooth ride to 3,000 feet every time.

So what does the software automate?

To automate the towing process we needed to capture the knowledge inside the head of SilngMachine’s creator/designer Sean and condense that into software. The objective being to create software that can deliver as safe and reliable a tow as the human operator.
By no means does the software replace the tow operator, as the operator is performing the complex task of monitoring the flight of the pilot and glider to ensure that they are flying safely. The software takes over the monitoring the towing pressure exerted on the glider and adjusting the towing speed to compensate for changes in the wind speed / direction and the effect of thermals.

This allows the tow operator to concentrate on how the pilot is flying; focussing on whether to proceed with the tow or to abort the tow if the pilot gets into difficulties. For instance, during the launch phase while the pilot is running along the ground, verifying that the paraglider wing is flying straight and level above the pilot’s head before applying the additional tow pressure to lift the pilot into the air.

So why is the towing pressure exerted on the pilot important?

Because the air is lumpy; ultra-light aircraft, such as paragliders and hang gliders, are very sensitive to wind gusts, wind shifts and to rising/descending air caused by thermals. The air through which the glider is travelling can change speed and direction relative to the towing force, which is attached to the ground. This causes the force excreted on the glider to change rapidly even though the speed of the towing vehicle and the force applied by the towing winch remain the same.

These two photos show a whiteboard design session where we are discussing the a mild feedback oscillation created when the pilot has several hundred feet of altitude, meaning that there is several hundred feet of tow line between the pilot and the towing winch. The control box detects a change in force exerted on the tow line and alters the towing pressure accordingly, however there is a delay between the change in towing resistance and the resultant effect on the glider. The control box must compensate for this delay otherwise it causes a feedback oscillation, which the pilot feels as a gentle pull and relax, pull and relax motion. What was really cool for me was being the pilot on the end of the tow line, feeling that oscillation and knowing exactly what the software was doing and why. Thinking to myself when I get back on the ground I know how to fix that.

Whiteboard session 1

IMG_20141102_160742

Whiteboard session 2

IMG_20141102_161627

The SlingMachine control box

control-box

The control box has 2 dials to set (1) the target towing resistance based on the pilot weight (2) the target towing force adjusting for wind shifts and thermals experienced by the glider. There are 5 mode switches for the different stages of the tow:

Pre-tension;
Puts tension on the towing line prior to launch

Pre-launch;
Increases the line tension assisting the pilot whilst transitioning from pilot stationary and glider on the ground to pilot running on the ground with the glider flying above his/her head
Launch; once the glider is flying straight and stable, increase the line tension to lift the pilot into the air and gain some initial altitude

Towing;
This is the main body of the tow when the pilot will gain the majority of the altitude

Rewind;
When the tow is complete and the pilot releases the towline the winch automatically rewinds the towing line.

The control box is based on the Arduino Mega 2560 micro controller, which is perfect for the task of constantly monitoring several analogue input channels and setting the appropriate outputs to control devices in the physical world.

What lessons did I learn?

Developing this software was the most fun and the biggest challenge.
We developed highly reliable software in a short space of time with minimal resources, however in my view this was only possible on a small scale project such as the SlingMachine towing software. This is because the software is performing a relatively simple and well defined set of tasks; the software monitors the towing pressure applied to the pilot and adjusting it to maintain the optimum in changeable flight conditions.
The five principles we used to develop the software focused on creating ultra reliable software with the limited resources at our disposal. The principles were based on common sense and 25+ years of developing high integrity systems.

Given my background in high integrity systems the next step for the SlingMachine software is to run extensive edge case testing on the software. To this end we have built a test rig for the control box, with which we can feed in sensors readings as if they came from the SlingMachine winch. The sensor readings can come from 2 sources:

  1. We can dial in sensor readings with potentiometers. This allows us to test the edge cases that may only occur in 1 in 1,000 tows.
  2. We can playback real input sensor readings recorded from actual tows of real pilots. These recordings allow us refine the software algorithms comparing the performance of the new software revisions against the recording of the old software. The advantage of using recorded sensor readings to test the software is that the tests are as close to real life as possible without a real pilot having to leave the ground.

So What Next?

The initial software development was done in 3 weeks, which was the duration of my visit to Arizona, during which the primary aim was to get the software operational before the end of my trip. We are now developing new embedded hardware / software modules to monitor live telemetry from the pilot and further enhance pilot safety.

Tow pilot telemetry pack:
Which monitors the flight of the paraglider pilot and relays that information to the tow operator at the controls of the winch. This gives the tow operator much better picture of whether the pilot is flying well or if things are starting to go outside the norm. This is especially valid when the pilot has gained some altitude and so is further away and the visual signs that the pilot is getting into difficulties are much harder to see.

Novice pilot telemetry logging pack;
Once a novice pilot has released from the tow line they are in free flight under the instruction (over the radio) from an instructor on the ground. The novice pilot has a number of tasks to do on each of their free flights and these tasks would usually be done at the highest possible altitude as this gives the greatest safety margin when trying new manoeuvres. The recorded telemetry allows the instructor to better understand what the pilot did during their flight – pilot position, height, turning forces, rate of climb / decent and lateral acceleration.
This data also allows the instructor to verify that the novice pilot has completed the assigned task when the pilot might be at several thousand feet when the task is performed. It may also be the case that glider has done something the novice pilot did not expect during the flight, either because of external forces (wind or thermals) or because of the over active input from the pilot, instructor can also use the telemetry data to help the novice understand what happened and what to do in the future.

Novice pilot safety pack;
This will be an extension to the novice telemetry pack which will use the input from the sensors such as the accelerometer and barometric altimeter to identify when the pilot gets into unsafe situations. For instance sounding a warning if the pilot performs aggressive turns at low an altitude or if the pilot is performing an increasingly aggressive spiral turn greater than 3600
The development strategy we have used so fare for the development of the SlingMachines control box has worked well so far. We are very open to suggestions for a development strategy that will enhance the security and reliability of pilot safety projects and the continuing development of the control box as we move forward in the development and the software gets more complex.

Thanks,

Martin Emms

$1million Foreign Currency Flaw

Aad raises a good question in his blog post; Why are we using reliability / dependability tools and techniques such as Praxis methodology and Z modelling to identify flaws in the existing EMV payment system?  These tools were intended to be used to in the building of reliable systems, however we are using them to analyse the security / reliability of an existing system post implementation.

Our CCS 2014 paper “Harvesting High Value Foreign Currency Transactions from EMV Contactless Credit Cards without the PIN” outlines the methodology we have developed for analysing the EMV payments protocol.  The methodology uses (i) abstract modelling to identify potential anomalies in the EMV payments protocol (ii) software emulation to exhaustively test real-world implications of the anomaly on credit/debit cards (iii) practical demonstrations of any flaws identified, allowing us to better communicate our findings to the general public and the banks.

In short the methodology we have developed is the scientific contribution that underpins our work, without which it could be argued that we were simply lucky hackers who have stumbled across some interesting bugs in the EMV implementation.

So far the methodology has identified the Foreign Currency flaw (CCS 2014) and the Contactless PIN Verify flaw (FC 2013) both of which stem from the specification NOT detailing what should happen under a given set of circumstances.  This is where we get back to Aad’s question “Why are we using reliability tools for our analysis?”; Leo Freitas’s abstract model is very good at identifying conditional cases that are not satisfied by the specification, highlighting a missing case (which is not handled) rather than an incorrect case or an exception case, something we human are quite bad at seeing.

The system designers and coders are usually focused on making the system work and dealing with the expected exception cases; this is perfectly valid as this is the most efficient route to delivering a working system.  However this may lead to the assumption that a particular set of exception values would not occur together and therefore the exception case is not handled.  This un-handled case shows up as an anomaly in Leo’s abstract model => which leads to testing in the EMV emulator => which leads to a practical demonstration of the flaw=> which leads to a paper at CCS => and eventually ends up on the BBC News.

This year I have found it a little frustrating that the sensational “hack” papers grab the headlines and are easiest to get published at a good conference (we also wrote a “solution” paper and a “methodology” paper this year which generated zero interest and were not published).  However what we learned from the CCS paper reviews was that the best paper combines all 3 elements; good science in the “methodology”, good results in the “hack” and a responsible set of possible “solutions” in the conclusion.

Hopefully my random ramblings have been of some help

Slides from CCS 2014 presentation CCS2014_foreign-currency_v1-2

Designing Reliable Systems versus Finding Security Holes

At various presentations and also in our research on credit cards I came across approaches for security vulnerability research that are based on tools and techniques for building reliable systems.  I am curious about the relation between the two, and thought maybe a blog is a good venue for people to share some thoughts on the issue.

A couple of examples of what I mean:

– Martin is trying to build a reliable emulator for credit card payment. He works with Leo on proofs for reliability. Martin essentially follows the Praxis software development approach, in a light-weight incarnation. But, as a consequence, he and Leo find security vulnerabilities. Shouldn’t we have used a tool/method that aims at finding security vulnerabilities instead of one that aims at building reliable systems?  Or are these somehow the same?

– We recently had a colloquium guest speaker (recently graduated PhD student) from Glasgow who talked about her research in using safety case description languages to describe case studies for security breaches.  Such use is almost contrary to what the language was defined for, but it seemed to work.

I’m interested in the question whether we use existing dependability/safety techniques for security research because (1) we don’t have better ones yet or because (2) they are the best ones imaginable.  I guess the answer is ‘it depends’, but it struck me as interesting to try to understand this issues more generically and discuss on this blog.  So, please comment.

J-PAKE adopted by ISO/IEC standard

J-PAKE is a password-based authenticated key exchange protocol, developed by Peter Ryan and myself in 2008. Over the past six years, the protocol has withstood all sorts of attacks and has started to see some real-world use in providing end-to-end secure communication for Internet users. The full records of discussions on J-PAKE can be found in the previous lightbluetouchpaper blog.

About six months ago, in the ISO/IEC SC 27 meeting held at Hong Kong in April 2014, I gave a presentation on the rationale of including J-PAKE into the ISO/IEC 11770-4 standard. The presentation slides are available here. An accompanying document was officially circulated among the national bodies under ISO before the meeting. It was agreed in that meeting to start a six-month study period on Revision of ISO/IEC 11770-4 and invite all national bodies to comment my proposal.

This week, in its meeting held in Mexico City, October 20-24, 2014, ISO/IEC SC 27 Working Group 2 considered the contributions received under the study period. After some discussion, SC 27/WG 2 unanimously agreed that this standard should be revised to include J-PAKE.

In the same meeting, two security weaknesses of the existing SPEKE protocol in ISO/IEC 11770-4 were discussed based on the findings reported in our SSR’14 paper. (A copy of the paper is publicly available at IACR ePrint and the paper is discussed in a previous blog post.) After some discussion, it was agreed that the SPEKE specification in ISO/IEC 11770-4 should be revised to address the attacks reported in our SSR’14 paper. The revision work on ISO/IEC 11770-4 starts immediately with myself being one of the editors. We expect to provide the first working draft for comment by 15 Dec, 2014.

On a more lightweight subject, while in Mexico, I try to do as Mexicans do: i.e., drink a glass of cactus (mixed with celery, parsley, pineapple and orange) during the breakfast. It was such a horrible taste that I was unable to finish it the first time. However, the more I try it, the more I like it. Now I can’t have a breakfast without it. The way our body treats a new taste of drink reminds me of the way how our mind treats a new idea. A “new” idea usually has a bitter taste in it as it challenges our mind into accepting something different. The natural reaction is to reject it and remain satisfied where we are and what we already know. However, to appreciate the “sweetness” out of the initial “bitterness” of any new idea, it takes time and patience – and in fact, lots of patience. When I return to the UK, I am sure this will be the drink I miss most from Mexico. So, cheers one more time before my flight home tomorrow!

Cactus drink

The SPEKE Protocol Revisited

In a forthcoming paper (to be presented at SSR’14), we (with Siamak Shahandashti) present some new attacks on SPEKE, an internationally standardized protocol. The idea originated from a causal chat over coffee with my colleague, Siamak Shahandashti, four days before the SSR’14 submission deadline. But the idea was interesting enough (to us) that we decided to write a paper. It was intensive a few days’ work, but it turned out to an enjoyable experience. A preprint of the paper can be found here (also in the IACR ePrint).

Background: SPEKE is one of the most well-known Password Authentication Key Exchange (PAKE) techniques. It was first designed in 1996 by David Jablon. Over the past twenty years, it seems to have withstood various attacks, and yet no major flaws has been found. To date, the SPEKE protocol has been included into the IEEE P1363.2 and ISO/IEC 11770-4 standards, and deployed in commercial products (for example, Blackberry).

Our findings: However, in our paper, we identity two weaknesses in SPEKE, which seem to have evaded previous efforts of cryptanalysis. First, we show an impersonation attack, in which an attacker is able to impersonate a user by engaging in two parallel sessions with the victim. Second, we show a key-malleability attack, in which a man-in-the-middle attacker is able to manipulate the session key established between two honest users without being detected. We further explain the applicability of the attack to the SPEKE variants defined in IEEE P1363.2 and ISO/IEC 11770-4 and point out deficiencies in both standards.

Suggested changes to standards:  Finally, we propose concrete changes to both the IEEE and ISO/IEC standards. The changes that we propose not only address all currently known attacks against SPEKE, but also improve the round efficiency of SPEKE as it is currently defined in the standards.

For more technical details, please refer to our paper. Any comments are of course most welcome.

Updates:

  • 2014-10-24: during the ISO/IEC JTC 1/SC 27 Meeting held in Mexico (19-24 Oct, 2014), it has been agreed by the national bodies present in the meeting to revise the SPEKE specification in ISO/IEC 11770-4 to address the two attacks reported in our SSR’14 paper.

Every Vote Counts: Ensuring Integrity in Large-Scale Electronic Voting

Last week, at USENIX EVT/WOTE’14, in the beautiful city of San Diego, I presented a paper that was jointly co-authored with my former colleague at Thales (Mr Matthew Kreeger) and colleagues at Newcastle University (Prof Brian Randell, Dr Dylan Clarke, Dr Siamak Shahandashti, Peter Hyun-Jeen Lee). The title of our joint paper is “Every Vote Counts: Ensuring Integrity in Large-Scale Electronic Voting” (presentation slides here).

In this paper, we first highlight a significant gap in the e-voting research field that many people seem to have ignored: while the End-to-End (E2E) e-voting systems have been extensively researched for over twenty years and have been commonly heralded as a rescuer to many controversies in e-voting, in practice few of those systems have actually been implemented and almost none of them used in real-world national elections.

We are motivated to find out the root cause and to narrow the gap. Our hypothesis is that the existing E2E systems’ universal dependence on a set of tallying authorities (who are assumed to be from parties of conflicting interests, be expert in cryptographic key management and be expert in computing) presents a significant hurdle towards the practical deployment of those systems.

We then show that the involvement of tallying authorities is not strictly necessary at least in some election scenarios. In particular, we focus on DRE-based (Direct Recording Electronic) elections conducted at supervised polling stations. This is perhaps the most common election scenario in national elections around the world, e.g., USA, India and Brazil.  We present a new cryptographic voting protocol called Direct Recording Electronic with Integrity (DRE-i). The DRE-i protocol provides the same E2E verifiability as other E2E voting protocols, but without involving any tallying authorities. Hence, the system is “self-enforcing”. By comparing with related E2E protocols that are dependent on tallying authorities, we demonstrate that a self-enforcing e-voting system is significantly simpler, earlier to implement, more efficient and has better usability – all of this is achieved without degrading security.

We welcome interested readers to scrutinize our paper, point out any error or discrepancy that you can find, and feel free to write your feedback in the “Comments” below.

CFP: Special issue on security and privacy in cloud computing

The following is a CFP for the special issue on security and privacy in cloud computing, to be published by the Journal of Information Security and Applications (Elsevier) in 2015.

Submission deadline: 15 Jan 2015 (changed to 15 April, 2015).

http://www.journals.elsevier.com/journal-of-information-security-and-applications/call-for-papers/special-issues-on-security-and-privacy-in-cloud-computing/

Research works that contain “new” ideas and are driven by tackling “real-world” security/privacy problems in cloud computing are especially welcome.

How many years it takes to publish a new idea

While the original idea could be traced back to a chapter in my PhD thesis, the actual work on large-scale e-voting started in 2009 when I was still working in Cambridge. With my colleague Matthew Kreeger, we began to critically examine the basic theory underpinning the 20 years research on End-to-End (E2E) verifiable e-voting, and attempted to design a new category of E2E systems that did not rely on any trustworthy tallying authorities. We called the new category “self-enforcing e-voting”.

We first released a technical report in IACR (2010), and then tried to publish it at a conference.

http://eprint.iacr.org/2010/452

Until its recent acceptance by USENIX JETS (Vol. 2, No. 3, 2014), the paper had been repeatedly rejected by top conferences in the field. The final version of the paper is in the open-access domain (below). The technical protocol in the paper remains unchanged from its 2010 IACR report.

https://www.usenix.org/jets/issues/0203/hao

This has been an interesting personal experience, from receiving consistently harsh reviews and repeated rejections from top conferences, to getting surprisingly positive feedback from the ERC panel and a €1.5m starting grant to support my further work, until the final acceptance of the paper just recently.

Getting rejections is always a frustrating experience, but in the end, I feel I learned most from the rejections rather than the acceptance. Today’s top security conferences have developed an extremely rigorous reviewing process, which is good. But perhaps, the process could be slightly adjusted to give a little bit more tolerance to “new” ideas, albeit they may be controversial or have all sorts of shortcomings in the beginning.

Acknowledgement: The co-authors of the paper are Matthew Kreeger, Brian Randell, Dylan Clarke, Siamak Shahandashti and Peter Lee. We especially thank several dozens of anonymous reviewers – who liked or disliked the paper – for the feedback and for helping us improve the paper.

Radio interview with Ehsan Toreini about private browsing

Ehsan was interviewed on a radio show last Thursday (17 July, 2015) by an Australian radio station LifeFM, on the security issues of private browsing in modern browsers. It was related to a recently published paper which Ehsan co-authored: “On the privacy of private browsing – A forensic approach” (2014, ScienceDirect).

The interview recording can be found here.