Real World Crypto conference 2020: session 11

all right so we already just ready to start the third day of real-world crypto and our first session today is on wireless protocol security and our first speaker is David Basin who's gonna talk about 5g security so David all yours thank you so I need a clicker is this the just the right one somebody took the clicker I'd love to give a talk but we need new tactics occur did you take it okay it's a pleasure to be here and to talk about work on model checking 5g security this will actually be a talk within a talk the outer talk will be on the importance of formal methods and particular model checking for security protocols and I'll introduce some techniques that may be new for some of you that I think can be very important for the real world crypto community the talk inside the talk will be an application of these techniques to 5g and the security standard within 5g the work I'm talking about is a large collaboration it involves different teams also international across countries one is the team of researchers who have worked together with me on the tamarin project and I listed them here tamarin is a model checker and I'll tell you a little bit about it and it's been under development for over eight years the second team which I'll talk about and there's some overlaps are those who have worked with me on the 5g on modeling and reasoning about the 5g specification v t is a huge specification we took a number of years to follow the formalization of that and that also took a fair amount of manpower so big thanks to those people who worked with me also I just like to mention that for some of the sites I'm Tamara and I'd like to thank calves because their slides that I bought borrowed from him let's begin with security protocols and the need for formal methods this isn't 5g this is from the internet key exchange it's one of the faces it's one of the modes the details don't matter you don't need to understand it but I just point out a few features for example we have keys that are being used for encryption and these keys are being derived from various other keys so there's a key and then there's a driving key than an authentication key an encryption key etc so we have all these nested hashes and you might ask yourself clicker okay there we go we might ask ourself why all of these nested hashes and well there are good practices and one good practice is you use different keys from different things for you begin by driving a lot of keys then if you look carefully you might see for example that these diffie-hellman public keys these GD x g the y's are sometimes written another order and these cookies against denial of service or sometimes also change and you might ask yourself this argument order matter and there might be some people in the audience would say yes it's a good idea to change the order of things because this will prevent certain types of attacks like reflection attacks where you play a message back to a party and he accepts in a different step I would argue these are not the questions we should be asking the fundamental question we should ask are what does this protocol actually do what does this protocol actually achieve and in what environment so and our environments have adversaries so against what adversary does that have the properties who would like these are the real questions not these questions that somehow motivate best practices about how to organize protocols but nevertheless protocol design today is typically approached as an art there are these best practices there are committees within the IETF w3c and other organizations that build protocols they often have to reuse existing protocols and the whole thing reminds me a little bit of the following story some of you may know it so I have here a picture of a roast that's a big piece of meat and the story goes as follows when I made a roast I always started by cutting off the ends just like my grandmother did someone wants to ask me why I did it and I realized I had no idea it never even occurred to me to wonder it's just the way it was done eventually I asked my grandmother grandmother why do you cut the ends of a roast and she answered because my pan is small and otherwise the roast would not fit so this is to some extent how I see how I think protocols are being designed we have these best practices we carry things out sometimes we don't even question why the alternative would be protocol design as a science and here I mean in the root sense of the word science so that is discovering and knowing something that you can demonstrate and verify within a larger community and formal methods is one way of doing this it's a way to build better protocols where we have very precise specifications of the system so the protocol of the environment ie the adversary which with which it interacts and also the properties and if we do this well and we have supporting tools than we can debug verify and explore alternatives and I'm happy to say that there's been a lot of progress over the last 20 plus years in formal methods for security protocols and tools have advanced to the point where we can apply these protocols with reasonable effort to protocols that really matter and here I've listed in yellow some of the protocols that my team has worked on so protocols for entity authentication 5g I'll be talking about that today there are some great work at Oxford with cast cash Kramer's on TLS 1.3 and this is very exciting and slowly companies are becoming tool users I hope by giving such a talk I might motivate those of you who come from industry to consider whether such tools might help you in your work so where is the difficulty I mean the problems were not easy it's not just like you snap a finger and you verify protocol so this is kind of a standard picture from verification 101 what we do is we have a specification of the system that sometimes called the model because you're making a model of the system at some level of abstraction and you'd like to show that it satisfies certain properties and why is this difficult to do well for security protocols we have to first specify how the system operates and if you look at a typical standard whether it's an IETF standard some other standard often you have the problem that before formalization comes you must be precise and protocol design documents are often incomplete and imprecise often it's unclear what the adversary model even is so protocols are given without adversary models or there are statements like this protocol should not be subject to replay attacks that's like saying his program should not suffering from a buffer overflow yes that's true but it doesn't tell you what the program actually does another problem is from the security properties what shall be achieved and here properties are often implicit or imprecise so example authenticate what is authenticate really mean their various ways you can make that precise and finally of course the notion of satisfaction does a system meet its its requirements here ideally we have proof and in the best possible case machine check proof because humans can get lazy or make mistakes and here we're up against undecidability so I'll be talking about verification of symbolic model and here even for very simple classes of protocols basic properties like as a key a secret is undecidable and even if you restrict yourself to restricted cases where you can only have for example finitely many interleaved runs of a protocol you still have a problem intractable problem so the weapon of choice that we've been working on that I'll tell you a little bit about is tamarin so tamarin is not an acronym it's actually a monkey kind of acute monkey and tamarin is basically our tamarin is basically a constraint solver that solves constraints about what the adversary could do in a particular situation and then we turn that constraint solver into a few improver so it's a constraint solver disguised as if you're improver I'll say a little bit about what tamarin does I won't say really how it works I want to talk about the algorithmic background to it there would be a different talk for a different community but I'll just tell you a little bit about how you might use such a model checker and then we'll move to 5g so as is often the case in model checking you have the specification of the system this doesn't work all that well the specification of your system that's called your model you have the property you negate your property and you would like to have a behavior that's consistent with the system so it's a system behavior that false applies your property or property and in our case with tamarin we use constraint solving define that and if we find such a behavior that's an attack and we get a representation of it you could present that to the user for example as a message sequence chart if you would like and importantly if the constraints are inconsistent then no possible attack can exist and this means no matter how you into leave runs the protocol arbitrarily many runs with the adversary there cannot be an attack and that constitutes a proof of course since the underlying problems are undecidable you might run out of time memory patience etc and then tamarin allows you to go into an interactive mode where you can work with this theorem prover constrained solver to interactively construct a proof or to provide hints so sometimes you need exhilarate invariance or even possibly change the underlying proof strategy being used that's called Oracle's okay how do you actually use this in practice so protocols are specified using a specification language called multi set rewriting multi set rewriting is a little bit like term rewriting for those of you who know it but rather than changing one term to another you change a multi set which you can think of as a bag of facts into another bag of facts and these bag of facts represent the states of the different protocol participants think of them as each having a little protocol automata so what state are they in what do they know and also for example the state of the network which might contain information on messages being sent out received but the adversary knows etc so here's a little example so in multi said rewriting our rules transform a left-hand side to the right-hand side and it can also be labeled with actions these are it gives rise to a labeled rewriting system a label transition system there's a typical example of a rule the left-hand side says if we have input to our network so n represents input to the network of some K think of it as a key and in our multi set some a protocol automata with some thread ID thread ID is in some step is in its first step then in that case our protocol would say well advance your step two step two and output on the network and acknowledgment and also in your state record that you receive this key K okay so this would very person to transition from taking input off the network to recording and outputting a response and this would be labeled with a threat ID have accepted que se as a key so this gives rise to transition system with the tre semantics so now imagine we have a state of our system says this bag this multi set of facts and this multi set we have many facts but among them are that key is input to the network and some thread ID 3 is in step 1 then we can match that with the left-hand side of this rule so key would be instantiate K would be instantiate with key thread idea would be instantiate with tid 3 etc then this rule would say we can take these facts out and replace them with instantiated right hand side of the rule so we match the left-hand side we replace it with instantiating right hand side so we get a new state with AK output on the network and this thread ID has advanced its state and recorded that it's gotten the key moreover this transition is labeled that thread ID has accepted the key and this gives rise to a label transition and you can continue this because you'll have other rules available and you get a trace which is a sequence of transitions and in particular the trace we entered what we understand by a trace the trace amman --tx is the sequence of these red parts here and that trace is important because we specify properties over traces so we can say for example somebody is accepted a key and the adversary doesn't know it that might be something that we would specify that may be a security property so I showed you an example of a rule and in general in protocols you'll have multiple rules so for example I have multiple roles in each role will have a role automata there might be a initiator role or responder role a key server role this would be an example of the role automata for the client state machine for TLS 1.3 and here for each of these arrows here we would have a multiset rewriting rule okay so in general you'll have quite a lot of multis head rewriting rules for complicated protocols we also have to specify our adversary so for our adversary what we want a network adversary who's active sometimes this is called a dual of yao adversary historically at least in the symbolic setting but as cryptographers here know a network adversary you know seems strong they see everything they can they can interfere but actually we want to that are even stronger adversaries who can for example corrupt long-term secrets corrupt around a number generator corrupt session state this would correspond to different Oracle's in the computational setting so here's an example of how you might specify session reveal yeah excuse me right so you can specify these adversary capabilities also by multi set rewriting rules so here's how you would specify a session reveal so if there is a state where some thread ID has learned a key then that key can be output to the adversary and that transition will be labeled with thread IDs key has been revealed to the adversary okay so again so we spent we have rules for all the different protocol automata and we can also have rules for the behavior of the attacker now the question is how do we specify properties the properties themself are specified in a guarded fragment at first-order logic with time points it's essentially morally like a past time first-order temporal logic you can say if something has happened and something can't happen before or at other points in the trace so here is an example of how you might specify that a key is secret it would be for all threaded e's for all keys it's a two sorted logic so one of the sources over time points for all time points I if a thread ID tid has accepted a key at time point I then there isn't another time point J where the adversary knows the key so K here means the adversary has learned the key at time point J okay so in this way we can specify properties and the property will hold if all possible traces of the protocol satisfy that property okay so you specify good properties and then you want to see if when you negate them you can find traces that violate the properties that's how model checking works and again these are interpreted over the red bits over the traces okay then at the end of the day there's a question of well what does tamarin really do what's the magic of tamarin so tamarin takes these specifications of the role automata of the adversary of the security properties and then it uses various constraints all VL gorillas which I will not go into which I will not describe further to try and see if there is a way that the different protocol automata can somehow be run together with the adversary to attack the protocol and if it's not the case then we will have a proof that no possible attack can exist at all so let me now move from tamarin that was kind of a quick high-level bluffers guide to what a model checker my - to analyzing 5g I'm gonna use my phone as a little prop so 5g of course as you know is the new standard for for wireless communication it's standardized by the 3gpp the the first full release of it at least that the first full relief release of the basic 5g protocol was last year June fourteenth two thousand eighteen this is a protocol that is going to have massive uptake so right now most of you are using four G so LTE maybe in some places of the world even 3G but for current cellular services we have about five billion mobile subscribers and we can expect that and more for 5g because 5g will also be used enable the Internet of Things and things like this and you can expect that a large portion of the world's population will eventually have 5g axis so the question is okay very good this is a protocol it's used for communication communication is critical how is it secured and there are various parts of it that are security relevant and here I'll be talking about aka authentication and key agreement and what I'll be describing here you can find more about in a CCS paper so how does the thent occation key agreement work within 5g so the idea is we have user equipment there's a bunch of acronyms here so the UE the user equipment which has a sim now called au sim a universal subscriber identity module I want to be able to use this for for telephone calls and so I am Swiss and I have a phone registered in Switzerland with Swisscom so Swiss come is my home network and I come here in New York and according to my phone phone my serving network is t-mobile so I don't have any security association with t-mobile but I have my home network I would like to set up an association in a secure channel with a serving network and 5g aka is about how you do that how the subscriber and the serving network authenticate each other and set up a key okay now of course some security you typically don't get security from nothing so we have some set of assumptions namely that on my use sim my my user subscripting user equipment in the home network will share a symmetric key it will I'll have a permanent identifier called the su p we also had su piece in previous versions of 5g like 4G that's a subscriber permanent identifier the su p is privacy relevant and in 4g there were problems with MC caches because as you go around say in New York your phone is often transmitting your su p so you can you can hear that at various places if you if you're listening for it and you can track me as I go through New York so in 5g they said we want to get that right so we're going to conceal the soupy and something called a tsuki we're gonna see that later so the su p will be used to drive a tsuki and that'll be derived in a randomized way such that that changes so presumably I cannot be traced as I go through New York there's also a sequence number so it's the sequence number based protocol and I will also my use we couldn't we'll also have the public key of the home network ok sets the set up let's look at how the protocol works I will give you the main ideas I won't go into through every little micro step because there's a lot of detail here but I'd like to give you the main idea of how it works first I will send to the serving network say here in New York my supey but I will mask it I will encrypt it using the home networks public key so here this is just my terminology for asymmetric encryption is randomized using some random value that I generate it's encrypted with the public key of the home network and I tell the serving Network also what is the identity of the home network case we heard I have a little message sequence chart this shows the little setup assumptions who knows what and I'm going to send the tsuki from the subscriber to the serving network and then the serving network now knows who the home network is so it says I am the serving network and here is the Sookie and then the home network can choose an authentication method there are several and I will tell you about aka and here on this slide I have the successful case of aka and I'll also show you a couple failure modes and again I don't want to explain every little line of this but I still want to give you the main ideas so it's a kind of a challenge response protocol where the home network will generate a random number now just so you know these various FS are keyed a keyed one-way functions and there are also various other one-way functions such as challenge and the like in PC which is used for key derivation function some of these have slightly different properties but I won't go into those details for now so what would would be what we do here is we use this shared key shared with sis with subscriber to make a Mac of the home network sequence number and also this random value and then we use another one-way function with two with this random value and the key to produce a random string and this random string will be used as a one-way function to conceal excuse me excuse me a one-time pad effectively to conceal the the home network sequence number so we don't want to send sequence numbers in the in the clear and the pair of this for this encrypted sequence number and the Mac is called attend that will be sent over and then unpacked on the other side and then we calculate various responses that the different parties can expect and then from all of this data this key the randomness and the sequence number and the the serving networks name we generate a key seed and this will be used eventually by the serving network in the subscriber to derive a common shared key and we increment our counter for the home network ok this various data then is sent this is a secure channel between the home network and the serving network so the randomness this authentication information an expected response in this key seed function for driving a key then the randomness and this authentication information is sent over to the subscriber and what is the subscriber do it first of all it unpacks the information then it generates this one-time pad itself because it's given the randomness and it has this shared key then it generates what it believes to be the sequence of for the home network then it can also compute you have little explanations here then it can also compute the Mac itself with this data that it generated and has and then it performs two checks and these checks are important the first check it does is that the Mac it calculated is the same as the maket received so in other words it checks the authenticity of the information god over-the-air whose the communication between the serve and the subscribers over-the-air so it checks that it got something authentic that this was authentically generated by the home network and then it checks recentness it checks the it's sequence number of the user equipment it shouldn't be greater than the sequence number of the home network as otherwise we would have a replay attack so it's important to remember these two checks authenticity and freshness if both of the checks succeed then there are some steps where it updates its sequence number to that of the home network it computes a response it can compute now this key seed because it has all of the data that the home network used for this key seed so it can compute the same key seed so it in a serving network and later on drive a common key it sends the response to the to the serving network who checks that it's legitimate and if it's legitimate it sends it to the home network and the home network also checks that everything is legitimate and if everything succeeds so here we had the serving network sending this Sookie to the home network than the home network says I now give you the serving network the soup P so you know really which subscriber you're talking to because until then the serving network hasn't authenticated the subscriber it just has a sookie which is a pseudonym but now it really has a soup P so it can use that for billing and for other functions okay there are two failure cases the first thing we thought is that there's a failure mode where the mac checks so that's i the mac checks but the counter but the message is not recent we have a problem with checking the counter this would happen when a message is being replayed now if that's the case and we have to synchronize and this is a problem with with protocols involved counters you have to effectively send your counter to the home network so the counter can read so the home network can resynchronize its counter so to do that what you do is again you want to take your sequence number you want to one time padded so you have to generate padding information and then you can pack that together and send information on the synchronization to the home network now an important thing for you to remember is that this synchronization information is sent when there is a Mac failure and it's sent with information that only the subscriber can generate because it depends on the subscribers key so please keep that in mind so this was the case that we had we have to resynchronize whoops and then the second failure is when there's a Mac failure and we simply send an error message that there's a Mac failure in the protocol aborts okay so that was a high-level view of how the protocol works this is the type of thing that what I've described here is actually spread out over seven hundred and twenty two pages in in 3gpp documentation but now we can ask ourselves the question of is the protocol secure so stepping back and model checking first we make things precise and after we made things precise may have a precise understanding we can make things formal and check so here are questions you might ask is the home network talking to a subscriber talking to user equipment with the ballade you sim or to an imposture privacy so for G had the problem with in CMC catchers but am i traceable as I roam through New York and if so how would that work so here we use Cameron but I have to say verification was really challenging often it's the case where we have problems from practice and we're not ready to handle them at some point in time this motivates a lot of work so in particular it's a challenging protocol because it has state it has sequence numbers the state is fairly complicated it uses X horse an operator so we have to be able to adequately model different cryptographic operators and XOR is fairly difficult to handle we formalize that equation Lee and it makes it very difficult to integrate XOR is very difficult to integrate into our constrained solvers are constrained for solvers work well it's something which is called sub term convergent theories and this isn't one of them so we had to go off and develop theoretical basis for integrating XOR privacy requirements are also quite tricky so to see if you're being tracked those are not trace properties they're hyper properties there are two hyper properties so you formalize privacy typically by observational equivalence and that's not a trace property for those of you who know about things like hyper properties it's a hyper property that's required extending our tool notches to verify protocols with respect to trace properties but also observational equivalence and of course there can be unbounded lis many sessions that are interleaved so this required a lot of work and we were able to use some very recent tamarin extensions which are published in other papers for example observational equivalence an XOR okay so how the formal analysis worked we formalized RAF 1.0.0 of the standard and this required following the standardization body for about a year building based models and augmenting them with their different changes so keeping up with them and this is a methodology that seems to work fairly well for example the Oxford team with the Cass Kramer's did this for for TLS 1.3 and you can really you know as verification engineers so to speak follow standardization committees and give them feedback we had to work with the documents of the 3gpp and that was over 722 pages of documents and it required a little bit of interaction to make things precise to understand them and the tamarin model for the protocol was 500 lines of multi set rewriting rules the specification of the desired goals plus some additional lemmas which were needed to make that the the verifier terminate was over was roughly around a thousand lines with 124 lemmas so the specification didn't really it wasn't very clear about the adversary so what we often do with tamarin is if you don't tell us the adversary will figure it out for you namely will first verify the the protocol with a fairly weak network adversary and then we'll add different compromise capabilities you can actually have a partial order of adversaries we'll try and find the strongest adversaries under which the properties hold and said another way we try and find out what compromise capabilities break the protocol okay so that also took a bit of work to find the strongest adversary models and it was computationally intensive doing a verification would take over five hours okay would we find out for authentication so what properties should hold well the standard itself specifies surprisingly few and weak attenti keishon goals so we had to guess for ourself what authentication goals should hold and certainly what's important is that the subscribers and the serving network so here I am using a serving network in New York we agree on a session key so we have authenticated keep the key cumin I know who the serving network is they know who I am we have a common view of the key that wasn't explicitly stated but when you state that it actually fails it fails for kind of a trivial reason that's actually pretty embarrassing namely the last message sent from the home network to the serving network whereas here the sukiya sent and then the soupier sent doesn't bind the supey to anything at all so in a in a world where interleave messages are possible it's possible for the serving network to get the wrong supey and if this were to occur this would be a real problem it could result in building the wrong subscriber for services what's interesting is the previous version of the standard did not have this flaw earlier versions did not have this flaw but at some point somebody just left out some message and this very simple mistake came into the standard so protocols can help you with simple mistakes they can also help you with very subtle mistakes here is a case of caching a simple mistake it's almost like type checking this type of stuff shouldn't happen there are a number of other problems which you could debate if they're really problems or not the standard aims at only implicit authentication so implicit authentication as well we we have agreement on the Keen we know who each other are but only after the key is used so whether or not that's good or not depends on how the protocol will be composed with other protocols if it's always going to be composed with other protocols in the future where you use the key before you rely on knowing who the partner is and that's okay otherwise it's not okay I would argue you should always try to have explicit authentication it turns out it's very easy to get in this protocol with very minor modifications no additional cryptography I would argue that that's an improvement whether it's an improvement or not depends on how you actually plan to use the protocol but also interesting is Sookie is security and privacy so here are some good things the session key is secret assuming there are no corrupted long term keys which i think is a fine assumption and you have a secure channel between the serving network in the home network there is no weak forward secrecy for the key seed function but you wouldn't expect it because it's a symmetric key cryptography also that's okay the long term key will remain secret when running the protocol this is all fine but there's something which wasn't fine and this was a real shock the supey remains secret so this common MC catcher attack won't work assuming no corrupted SN or serving network or home network but and this was really surprising that wasn't sufficient to ensure untraceable ax T so please remember the first failure mode when the Mac was correct but a message was replayed so you have an active adversary who replays a who hears a message from the serving network to my user equipment and can later replay it then I will always have a response that you can identify and you can associate with me because only I can produce it and that can be seen by an external party I will always give the same response where I Reese where I resynchronize the the sequence number and this is a response that only I can give so by looking at the response that I give in this failure mode you can actually track me as I go through New York and as I go through the world okay so the problem is so they got right the fact that the supey isn't being sent in the clear but the error messages are actually enough to trace absque rye burrs and this is this is a shock right this is one of the features of 5g is that it should have improved anonymity properties privacy properties and this absolutely fails and unlike the previous issues that that I mentioned there is no easy fix to this to this problem so the current version of 5g has this problem and there are still ongoing discussions it's not clear yet how to fix this so one of the nice things with working on formal methods is you can find attack the tacks are real the attacks matter it generated a fair amount of media here I have just some of the media in English in German in French etc I had lots of interesting calls with handset manufacturers and liked the ideas that I mentioned are very general I focused here on 5g the story within the story but the outer story is you can really use this for many protocols that matter here are some examples of the types of things that we can analyze in fact rather easily with with the tamarind tool let me draw some conclusions for the outer story art versus science I think we can improve the way protocols are built understood and analyzed in particular the community has come a long way the formal methods community twenty years ago we were doing very simple Alice and Bob exchange a key now we can handle protocols at the scale of a TLS 1.3 and 5g and I think standardization efforts should really be doing this they should be following the development of the protocols using these tools either themself or together in collaboration with groups that that that enjoy working with formal methods doing so as good hygiene it forces you to be explicit about your protocol your adversary in your property as I indicated you can find errors or produce proofs and that this is really a realistic effort to do of course the game isn't completely completely won we're always up against the problem of complexity complexity complexity the underlying problems are still undecidable it's always a question of how we improve the scope of our protocol of our of our tools what kinds of protocols can we model and how accurately how faithfully we can model them and finally an important point and that's one of the reasons I'm here is education I think it's very important to get the message out let engineers know you can use these tools and to work together in training engineers thank you [Applause] we have time for one question okay so I am one of the user of Tamra improver and you said about different kinds of adversary so how can you modify the capability of Dolloff yarr so I gave you an example of sessions tape reveal you just add rules right so we add rules that okay because I was trying to have a Vickie heat diffie-hellman model and yeah so for diffie-hellman you would want to have perfect forward secrecy perfect forward secrecy is just secrecy where you have a long term key reveal a long term key reveal could be formalized as a rule that after a session key has been established the long term key can be output to the network okay thank you can we just throw away those 700 pages and just use your 500 lines to understand the I I would say you should use both together so so the seven the 722 lines contain additional things for example hey Giselle things for example data type definitions so so you know how big are strings and things like this there's some justification arguments for things you get some history referenced others to answer I think you need both so I think that that it's in formal or semi-formal documentation should be complemented with formal models this model denial service attacks to dad that's not in the scope of this model and we would have to discuss what what we mean so I mean you can do some kinds of analysis of denial of service of service like say can they get you to perform can the adversary get you to a point in the protocol to perform expensive cryptographic operations you can analyze those types of things with these tools but that wasn't here [Applause] okay that was a fantastic talk and I guess we're gonna move on to another wireless protocol wg3 which was actually not on the list of protocols analyzed and so we're gonna hear about dragonblood okay good morning everyone thank you for the introduction so I will be talking about dragonfly and how it is used in wp3 ants EEP PWD so I am motif on oof and I did this work together with AOL Rowan Ronan who will do the second half of this talk so let's first do a very quick introduction this is all related to Wi-Fi security and if you look at the history we first had web which is quite horribly broken in response data find WPA based on a draft over the I Triple E standard and finally we have the latest I Triple E standard of wpa2 but wpa2 is vulnerable to offline dictionary attacks and recently there were also key reinstallation attacks against it and in response to all this they recently standardized WPA 3 um they decided to use the so called dragonfly handshake on the dragonfly handshake is what we call a pig meaning a does authentication based on a password on dragonfly previously was also used in the EPW deep protocol and this is a protocol you use in certain in a low amount of enterprise networks where you authenticate using a username on the password this handshake provides the usual properties you have mutual authentication you negotiate a session key but the more important thing is this does defend against offline dictionary attacks in contrast to wpa2 so how does the protocol work well let's say we have a client here that wants to connect to an access point then the first thing needs to happen is that both parties need to convert their shared password which is for example in ASCII or Unicode they need to convert it to a group element P and this element can then be used in the actual cryptographic calculations and once this is done the handshake can execute the actual first phase of the messages this is called the commit phase and to simplify it the commit phase essentially negotiates a new session key in the second phase of the handshake we have the confirmed phrase aunt and a high-level this confirms that both peers negotiated the same key and they prove to each other that they indeed possess the same password but the big question here is how is the password converted to this group element P and here the first remark is that the handshake can operate using both mod P crypto groups on elliptic curves but we will focus on elliptic curves here so the question becomes how can we convert a password into a point on the elliptic curve so this is often called a hash to curve algorithm and how can you do this well a naive way would be to take the shared password to combine it with the MAC addresses of the client and the access point and we can then take the resulting output from the hash function and interpret it as the x coordinate of the point on the curve now there's one problem here and this is that not all x coordinates are actually on the curve because some of them do not have a corresponding Y value in fact half of the X values do not have a solution here for the Y coordinates so that's a problem so how did they decide to handle this well they decided to add if test here where there were they first check does this square root have a solution and if not they will execute extra iterations they will include the encounter into the hash function here that calculates the x-coordinate this means an every new iteration we get a new point X on the curve so probably quite of you already see the problem here the problem is the password now the number of iterations now depends on the password being used and it also depends on the public MAC addresses what's actually quite surprising here is that the ietf on TRG the in fact warned about this timing leak but the designers didn't consider this series enough they thought ok this is a bit of a theoretical attack and we don't think it actually leaks the passphrase unfortunately we can abuse this side-channel leak to do a dictionary attack and I will now explain how this works so our threat model here is that either we can set up a rogue access point on induce the client into connecting to us and we can also do it the other way around we can act as a malicious client and try to attack the access point so both of these threat models are valid for our attack so let's assume that we are for example attacking the access point and we're going to assume that we can use timing measurements to determine how many iterations the access point needs to convert the passphrase into a curve on the point in particular I'm going to spoof the client MAC address a and I will measure that the access point needs two iterations and of course what I can do is I can take my dictionary of passwords I go through them I execute this algorithm on my own computer and I can then compare my offline computations with the one I measured and I can use this to exclude passwords unfortunately making one single measurement is not enough to include to exclude all possible passwords so we need more information and our example here two passwords still remain possible so how do we get more information to uniquely identify the password well if we go back to our algorithm here we can see that the MAC address of the client influences the execution of this algorithm so what we can do is we can simply spoof a different client MAC address and we effectively get an independent execution of our algorithm so to come back here we can spoof a client MAC address B we can again measure how many iterations does the target execute we compare this to our offline results and we can keep doing this until we uniquely recover the password to give you an idea about the complexity of this attack if we want to brute force the RockYou password dump we would need on average about 17 MAC addresses to uniquely determine the password the takeaway message here is that the number of iterations that are executed for a set of MAC addresses forms a signature of the password so one thing I haven't touched on yet is can we indeed measure these timing differences in practice so here we did an experiment on a raspberry pi 1 and the reason why we picked a raspberry pi 1 is because it's CPU is similar to a common home router and even some professional access points in this case we attacked the EPW D protocol so this is for example used in I would say about 3 to 4 percent of a neural networks yield attack was surprisingly effective when we make around 30 measurements per MAC address ant we filter out noise using Crosby's box test then 30 measurements is enough to recover the number of iterations so that covers the case for a PWD which was defined already several years ago when they standardized WPA 3 they did realize that they finally listed to die if I TF ones here for G at least partly ant they included countermeasures so what I did with WPA 3 they try to prevent leaks by always doing 40 iterations here on simply returning the first point that has a valid solution for the y-coordinate now that's not everything they did on top of it they also implemented this in blind that constant time to again try to prevent side channel leaks on top of that once the real password has been converted into a group element here they will execute the extra iterations of these total of 48 aerations using a random password again this was done to defend against possible side channel leaks now the question is does that solve everything the answer is unfortunately no the reason why is if we take the resulting outputs here of the hash function this needs to be truncated to the size of the prime P so if we use it 256 bits curve the the what is returned here are the first 256 bits of the hash output now the problem is if we use brain pool curves then there's actually a high likelihood that this output here even when truncated will still be bigger than the prime of the curve on that we do introduce a small theoretical base in the calculation so we want to avoid that and how did they decide to avoid this well they simply used rejection sampling sampling unincluded an if test here so the question is is it our our side channels now really soft and some of you may already see it we have a problem here this code may now be skipped on the amount of times that this code of escaped depends on our share shared passphrase now can we exploit this because we still because the extra iterations are executed based on a random password and the answer is yes because the variance now depends on when the password element here was found to illustrate this if our point P is found here in the first iteration then all the extra iterations are performed on a random password on the variants is high while if this is found in the very last iteration then there are no extra iteration based on a random password on the variants 0 on top of that the average execution time also depends on on which iteration the password was found as well so both the variants on the average execution time still leak information about the passphrase and if we then again try to execute this attack in practice on a Raspberry Pi against an open-source WPA 3 implementation we notice that measuring this is a bit more difficult but still by performing 300 measurements per MAC address we can still determine we can still recover enough information to brute-force the MAC address so that covers my part and now here we'll talk about some more vulnerabilities ok thank you so now we're going to talk about cache attacks and we're going to use a relatively similar similar type model but now we've only going to target the client and here we're going to assume that we act like a malicious access point and we're going to add the extra assumption that we are able to run some code on the client device now this code is going to run in user mode it doesn't require any special privileges or permission so basically for example any app that you download on your smart phone it might be sufficient and it's only required to be able to measure such a macro contextual sectionals so why do we need this and if we want to be able to attack any step of curves the previous attack that was mentioned is not applicable the lesson is that it needs to use the prime number that is very very close to a power of 2 and then there's the negligible chance that we'll see this random this rejection sampling okay so what can we do we're now going to use a cash attack called flashing reload this is an enabler us to detect the exact point in time where a specific code line was executed in this case and the code line that stores the recovered point inside the valuable now this is going to happen in any and check that we make and we want to know in which iteration does it happen so in parallel we'll also going to monitor the code to the hash notion and this is supposed to give us a kind of time doing different iterations now as this type of a text is usually very noisy and we will only want to we have a one bit of information many if this first iteration was successful or not and to do it we use and what's called the cache template attack and we're going to run several measurements and we're going to give a specific idea or number to each possible resort and then we can look at the distribution of the results that we get in both cases if the first iteration was successful or not it is easy to see that those distribution are very distinct and basically all we need is about 20 measurements in a very simple linear classifier to be able to lick this one bit of information now we see that we are able to leak information and password both with cache attacks and which time in the text but the question is can we actually exploited to recover the original password so to try to test this what we did was to provide a full probabilistic analysis of the amount of different measurements and computational steps that are required in order to recover the unique password out of different size of dictionaries we then continued to implement this type of attack using GPU code and then try to see how much money it will cost us on AWS instances to actually recover the password and we can see that for example for and they have I been point database of password which include all of the password dumps ever linked to the internet it will cost us about 2 cent in the worst case which is the recovery of password for the missed curves and even if we go over a very large personal domain Archaea nate symbol it still suffered that's relatively cheap for an attacker to do and again if this is your day job you'll probably buy your own GPUs and it will cost you much less than that okay so we are able to recover a password and now we went ahead and tried to look at more implementation specific vulnerabilities and now this might come as a shock to some of you but we were able to see several implementation that has better randomness and for example one implementation uses the system tank as the only entropy sauce and interesting fact is is that for wpa2 this doesn't really matter it doesn't even affect the security over for WPS so this is catastrophical and allow us to actually recover the password element another shocking finding is that we are able to perform invalid health attack several implementation didn't verify the point that they received in the handshake and this basically enabled us to recover the session key in by president dedication there are also several Wi-Fi specific attacks and the simplest one is denial of service and doing the entire fourth iteration is something that's very computationally expensive and it's relatively easy to saturate the access point CPU and then cause it was monthly spot to stop responding there is also the danger of downgrade attack basically in transition mode above WP to in WP network share the same password now this is something that has been handled by their standard and doing the handshake this done great will be detected and the connection will be dropped however this will only happen after a partial completion of the WP toe and check and this actually provides us all of the information that we need to do the previous dictionary attack and offline and recover the password and there are also several issues with the support for multiple curves it's relatively easy to downgrade their chosen curve so we can foster and the client an access point to use curves that are ideal and we cook in perfectly Oh easier to attack using sectionals so after we've had all this funding we started a very nice and interesting process of disclosure with the Wi-Fi lines we try to notified all of the involved parties as early as possible because we wanted to be able to try to influence the WPA standard direction was as followed we started with a privately backward-compatible security guidelines and several patches that were distributed between the different vendors after we looked at those patches we were able to find the baneful side channel that was shown previously and this led to another round of disclosure and that also includes several patches and recently about two months ago they were they updated the guidelines and enough for hibbett the use of curbs all together and if we look at the latest guidelines in the way we try to mitigate this type of attacks so there are several guidance that we try the Wi-Fi Alliance provides to the different vendors and one of the guidelines is a very simple straight fault please implement your code without any satchels another guideline says that if in some case the WPS three transition mode does not meet the security requirements then please separate your passwords and in the end what you say is that if you fail to implement those guidelines this might result in an attack and copies of the network and what I am virtual is how this can be checked for matrices not very easy to find such channels in a different codec for many different implementations but I'm not sure if this is going to be part of the certification process or not even after all of this there are still some fundamental issues that were not solve the main one is of course this is something this kind of protocol is very hard to implement in constant time without any state units and no matter what device is doing this 42 version is something which might be too costly and we actually saw several implementation they didn't do the whole 48 directions fortunately and I Triple E is now updated a draft of the standard which several of the our recommendations the most important one is to exclude the MAC addresses from the hash to curve calculation or together and incorporate it in a later part of the protocol this allows the password element to be computed offline and it does not only make the protocol much safer it also makes it much more more efficient to implement more well and this switch from this hash to curve that we shown with was called hunting and pecking to a constant time hash to curve solution they explicitly prohibit the use of many different groups and they have no oppose position how to prevent a cryptographic group downgrade attack and there are some remaining issues in the new standard and I think maybe the most notable one is that unlike many modern protocols they do not hush in the transcript of the messages in in propagated in the key derivation this has many issues it makes it much much harder to actually write a formal proof the protocol and it raises many risks of implementation issues for example the way that they prevent the cryptographic group downgrade attack is now dependent on different checks that Pokemon should make and if we simply incorporate the transcript in the Kindle evasion it will be made implicitly another problem is the way the dumb go to WP aw pay - this is something that's currently not addressed in the standard at all there is a possible solution what we call trustful first use which basically means if I connect to a network can you see that is WPA I will never agree to try to connect it with with WEP to wpa2 protocol this is actually done by both Android and the network manager of Linux but as long as there's one single device that doesn't follow these guidelines we can always attack it and use it for the offline mode force attack another remaining issue is that those new solutions are not backward-compatible this question how can they be adopted today maybe there will be a WPS 3.1 but we're not clear how the why freelance is going to end this and how they can prevent for example the risk for Dan we detect to the current which will WPC after all this you might ask yourself should we use wb-3 the question fight now think is yes w2 is trivial to attack so anything else is probably better and in conclusion we can say wp3 is vulnerable to stir channel attacks that like might lead to password recovery the current control measures are very costly and very hard to implement there is a new draft for that solves many of the issues we are not we don't know if it's going to be adopted or not but maybe most importantly those issues could and should have been avoided in the first place if the standardization process would have been more inclusive and for example we just seen one example with FFG and there's the TLS 1.3 err process we feel that we could've ended avoided all of these little problems and in that we'll be happy to answer any questions thank you great we have time for one question it's more of a request than a question and so currently CFR G is running a pig selection process I don't think side channel analysis has really been considered as a first-class security concern yet in this election so please would you guys get involved and give us some of your cycles and take a look at the proposals thank you yeah I know that they're also using the hash to curve Draft on there they're really looking at but you're not the handshake itself me exactly thank you okay really cool work and then now we're gonna move on to the third talk of the session which is gonna be on navigation security so really looking forward to the talk and not GPS actually but on Galileo security Tomer is gonna give a talk all right so that's my slide nope good so this is a joint walk with a long list of capable people whose names are projected here so I won't read them cuz I'll probably butcher their names in the native language and the talk is about Galileo authentication Galileo and for those who don't know is global navigation satellite system or GNSS operated by the European Union and even if you're not familiar with the term GNSS there's at least one such system that you are familiar with and that is the u.s. GPS so bluntly put Galileo is the European GPS and in fact there are full deployed systems like that the US GPS the Russian GLONASS Chinese Baidu and the European Galileo in addition to two regional systems the Indian narvik and the Japanese michibiki and I take that in this educated crowd everyone knows the principles of GPS navigation you stand somewhere with your cell phone there are satellites floating around the earth sending the location periodically in a reference time for when the message was sent your phone collects mesh messages like that it records the time in which the message was received and once it has enough of those four in the case of satellite navigation it substitutes the values that it has into these equations which solving them then gives you your location and you'll use GNSS I came here using by using Google Maps many cars come equipped with satellite not the onboard satellite navigation systems and for my mother tones I use devices like this to track my progress but actually GNSS is not only a consumer's technology it is heavily used in infrastructure in aviation in Mali navigation synchronizing power grids doing things in the financial sector it is really a part of the modern-day infrastructure which is why it's so shocking how is it is to spoof signals in Genesis in preparing this presentation about a week ago I searched YouTube for GPS spoofing and filtered out all results older than one week still there are hundreds of videos explain how to spoof Genesis data and what I find most insulting in this is the motive that the motivation doesn't seem to be hijacking an airplane all crashing down the power grid it is to cheat in a game played with your cell phone called Pokemon go so what we have is a critical piece of infrastructure originally designed by the US military that can be spoofed by people playing Pokemon go now there's no disrespect towards these people I am one of them I play pokemon go and I spoof Genesis data but I still find the risk unacceptable and so do the people at the Galileo project at the European Commission which is why they decided that their service will offer a public authentication and that means that when you use your device to determine your location based on Galileo satellites you will have assurance that this information is true so what we need is a system that we want an open system anyone can start their cell phone get the data and start navigating but we we want only legitimate satellites to be able to send the signatures for this data so that obviously puts us in the domain of public key cryptography but actually that comes with a problem due to the frequency in which Genesis operates the bandwidth is extremely limited it's between 50 bits per second and 200 bits per second it's 120 bits per second in Galileo and if you need context for this number about 20 years ago when I was 16 and I got my first home modem it was 43 times faster than this 20 years ago and on top of that due to legacy support the part allocated for authentication in Galileo is only 40 bits every other second of 20 bits per second on average so public key cryptography is out of the question because the signatures would just be too long and that doesn't leave us too many options right we only have two types so we probably should be using symmetric ography but this also still comes with problems symmetric key cryptography is called that way because the keys to all parties are the same all parties are indistinguishable with respect to the role in the protocol so suppose we use the same secret key for all receivers if I receive a message which I can verify using this key it means that I can also sign another message and send it to someone else who won't be able to distinguish between me as a sender and a legitimate sender so using the same key for all the server's is not an option how about using a different key for each user well first it's unclear how we would do the key exchange here right what I'll just talk to the satellite tell him okay we'll call it if he held it alight so not that and even if there was a way to disseminate these keys there's still the problem that the satellite would have to sign the same information using different keys and send them to all the receivers on a channel that I've already told you that is extremely limited which leaves us with the question of what can we still do so I will now present the system developed at Cal Leuven and just to clarify I'm not this is not a proposal this is the system that Galilei will be using it has been approved on all levels already implemented and testing should commence sometime soon I'm not exactly sure when and the system is based on key hierarchy I use the pyramid because I'm not sure in the hierarchy whether the bottom of the pyramid is the top or the bottom of the hierarchy we have several layers of kill and I'll go into each of them hopefully then you understand how the system works so at the bottom of the pyramid we have the route of a medical tree a medical tree for those not familiar with the concept and this is a bit awkward to explain what medical trees and medical is in the audience I hope I do it well amiracle tree is a way to provide a short commitment to multiple values what you do is put the values you want to commit to in the leaves and in the first step you have each of them separately that's this layer and then you have two values at the time to create a tree like structure then the commitment is the of this tree now I want to authenticate a value sorry I want to reveal one of the commitments so I provide the value I want to reveal along with the authentication pad which are the nodes with a circle around them and what the verifier does is to hash this value and they get this value and then they hash these two values and they slowly rebuild the tree and compare the route they get with the commitment they received and if they match it means that the value sent was part of the original commitment otherwise it means that someone found the collision in a collision free hash function also this doesn't expose any other value because let's say that I have this value when backwards in the tree means that you can find a pre-image in a pre-image resistant hash function which we assumed to be hard in our case what we put in the lives of public keys not too many of them and those will be used to out the lifetime of the system which should walk for I know 10 20 years and we really hope that we would never need to replace any of those kids but just in case we have a few others the root of the tree is hard coded into your device so what we have again is a medical tree used to authenticate a public key and the public key is used to verify a digital signature for a wood key I know that I said that there's no room in this protocol for digital signatures well I lied as long as you don't have to obtain the digital signature to every message you send we can once in a while infrequently sending a new root key we can probably fit in a digital signature and I say probably but we know that we can because we're testing the system now what is the root key a load key is the end of a hash chain the hash chain is built by selecting a secret key and hashing it and then the output is hashed again and each output is hashed and we have now a chain of hashes and the last value in this chain is the root key the root key can be made public because it's the output of hash function so you cannot go back in this chain and it is authenticated using a digital signature then the wood key is used to authenticate an effective key an effective key is another link in this chain now I'll tell you in two slides one what's effective about it meanwhile I'll I'll tell you that having one of those keys let's say the one before last it's easy to verify that it's called by hashing it once if it maps to the root key that we've authenticated using the digital signature it means that it was sent by the original generator of the chain because no one else can find a pre-image but for me as the person who generated the chain it's easy to provide three images I just hash forward and finally the effective key of an effective key is used to authenticate our payload the message or the location data M and for that we use the Tesla protocol developed by Reagan others in 2005 and it was walks in the following way the time is split into discrete components and I guess you can say it but it's I minus 1 I plus 1 etc each link in the chain is associated with one time frame and that's the an effective key is the key associated with what we think of is now later this key will no longer be effective it would be obsolete and we will have another less active key now how do we authenticate a message he'll in the first time frame and every subsequent time frame we get three data items we get em I'll call it n minus one which is the location data for that time frame and a message authentication code which is the symmetric key analog of a digital signature so a map of the location data mi minus one with the effective key ki minus one I don't have this key so I can check the Mac I take these two values and just stole them some well for the later use the third that item is KL the root key which as I said is verified by means of a digital signature so far I don't have my location and I haven't authenticated any location that's fine moving on to the next time step I again I get the location data M I and the message authentication code mi sorry the message authentication code for mi using the effective ki KI and I don't I can't verify that so I just store it I also get a I minus one that's an obsolete key that was effective in the previous time frame what I do is to hash it and see if it matches a kid have already authenticated in this case KL if it does I fetch the two data items from the previous time frame now I can now check the Mac if it checks out I know that I can trust mi minus 1 that was authenticated using this Mac moving on to the next time frame the same thing happens played at items mi plus 1 and Mac of mi plus 1 with the effective key I store those and I get ki and obsolete ki KI is hashed and if the output matches ki minus 1 ki minus 1 I know to be authentic so now I fetch these two data items with the previous time frame and I authenticate them and this is done over and over until the chain is exhausted a chain should last for about three months and then it's replaced and that's how our 10th occasion protocol works what we see here is an is an authentication scheme that authenticates values in with a certain delay in this example the delay is one time frame but the Galileo protocol actually allows different time frame so it supports multiple delays up to five minutes for different use cases and this is it then we also had to make some changes to the original protocol if we would use them it in the naive way we would need a hash chain for each satellite right we need we have a constellation of about 24 satellites so 24 chains each of them requiring a different wood key means also that we each of them requires a different digital signature and that would very quickly eat all of our bandwidth so instead we found a way to use one chain in all satellites another change we made is that in generating the hash chain it's not only the effective key that is given as an input we also add an AI value this is a reference to the time frame in which this key will be effective and it's like salt in password hashing for that particular key and an alpha value which is sold for the entire chain and also some random stuff because why not this is an actual system and it should be working for a really long time and we don't know whether sha-256 will be secure for the entire duration of the system so for each of the primitives we use we have several options and for hashing we use sha-256 but we also support sharply 224 and sharply 256 for mac macking we use h moksha 256 but we also support Simic AES and for digital signatures we use ECDSA with these curves all of these parameters you get from the satellite in the header of the message telling you which primitives are being used for the particular instance all security parameters unfortunately even after building this complicated system with the keyhole key we can't fit all the data we need to send into a message so have to plant eight some values and I hope this is not too outrageous it should be I hope to survive this we truncate the effective keys to 90 some of between 90 and 128 bits and we translate the message authentication codes to someone between 10 and 32 bits now I'm I don't recommend using max of 10 bits not even 32 bits but in our particular use case we have a security analysis showing why this is secure I don't think I have time to talk about it but maybe in the questions phase so to conclude Galileo will be using solid gelila will be offering a way to authenticate publicly the navigation data you receive from it so that you can play pokemon go without fearing that someone will cheat and steal your pokemon gym thank you [Applause] let me ask one question so these kind of systems they're very difficult to change once you deploy once you deploy them they're gonna be out there for decades so aren't you worried about quantum attacks like in 30 years 40 years ECDSA who knows where it's gonna be so I agree these decisions are made above my paygrade we actually discussed the possibility to include so I this would probably they should be here in the digital signatures I know that they've considered adding post quantum signatures as supported mechanism and decided not to and again I don't get this a vote in this okay maybe I misunderstood something it sounds to me like you have relying on very long chains and you only sign the very first up message what happens to a day GNSS system which is turned off for the first month I think comes on and then it starts hearing it how does it how is it going to get the verified case of I values yeah so the root key is sent constantly by the satellite as the we have time for a slightly longer question on each packet you receive from the satellite has the base information that I just explained and some management at minimal use is the root key and it's digital signature so if you get this key for example you also know what your time reference is you just hash it multiple times and see that it matches the root key that you also received from the satellite with a digital signature so how long is the chain actually is it like a million hashes or it's about well it's three months about three times three keys every 30 seconds someone who is probably a bad mathematician than I am but three six keys every minute for three months okay so okay yeah huge number of hashes okay so how do you prevent an attacker from taking the signal from the satellite delaying it amplifying it slightly and then the receiver locks onto the amplified signal and can't decode the original signal it's authentic but it's been delayed so now there's a shift in the position satellite but yes so first of all this system does not prevent someone from just jamming the signal that's not what we offer heal the receiver know has loose time synchronization with the satellite so it knows which key since the time reference is part of the key you won't be able to use it after the time frame ended so if you're using the rapid authentication you can delay it by 10 SEC maybe even less satellite navigation is even less accurate than that so that's not really a problem and beyond that the satellite can detect that the message is arrive too late and cannot be used you don't see it I mean we're talking you know a microsecond delay is a 100 meters a millisecond away is several kilometers so I'm not sure about these numbers possibly I don't have this slide here the error correlated when the satiric sandy the signal is anyway larger than this set a satellite navigation is less accurate than what we think what we use again not my field been explained that is assisted satellite navigation so your question comes from the assistance part anyway and not from the satellite but I think the cryptography is not designed to detect to defend against those kinds of attacks I mean this there are other mechanisms in the systems or more physical mechanisms that are designed to defend against that against German but German replaying he's referring to re playing attack well no so the cryptography does prevent a plane as long well with within the delay of the loose time synchronization you have with the satellite okay well this is a good topic for an offline offline discussion fantastic thank you this has been fantastic a really really very pop all right so we have a break coming just before we break quick announcement there's a clicker that's been found so if anybody wants a clicker there'll be a clicker up here on the on the stage and so we have a break now and we're gonna resume at 11 a.m.