Thursday 7 November - 3:30PM, Amphitheatre B at the IUT


Pascal Lafourcade of LIMOS:
How to trust digital applciations?
Formal methods can help you.

Security has become one of the main priorities in the development of new applications.  In this presentation we will show
how certain formal methods can help with the analysis and conception of secure protocols in the areas of
electronic voting, auctioneering, and electronic testing.

VIDEO TRANSCRIPT


Hello everyone, thanks for coming today.

This is the first seminar of the Digital Chair dealing with the theme 'Digital Confidence' - we are going to have two presentations today;

Let's get started.

My name is Pascal Lafourcade, 

I am a professor/research at LIMOS, member of the Universitι d'Auvergne.

and Jean-Marie Tirebois of the company Almerys,

who will make the second presentation.



So I'm going to try to explain how we can trust our digital applications, and the approach that has been applied for the last few years is to apply
formal methods.

So to begin, I think I am speaking to a group who knows this subject relatively well,

'Digital trust' means overall security, something which we can find all around us

These days WiFi is generally accessible, everyone uses secure wireless connections

We can pay for purchases online with our bank cards or our mobile phone

Why not be able to pay, with certain apps, your metro or public transportation ticket with your mobile phone?

We can connect to secure sites and in certain countries, will be able to vote electronically

For example in Estonia, voting and identification cards are electronic, all being done via internet and wireless connections

So on to Crypotography - security using crypotgraphy, in my opinion, is the use of cryptographic protocols which are based on basic components, which we know as 'Cyphering Primitives';

certainly the best-known, and a number of you should have already heard about this

RSA, which makes up roughly 80% of applications on the market 

so this is the most common cyphering found today

But, other Primitives are availble to the public, such as Elgamal, or symetrical key-cyphering,

or even signature functions like SHA-3, which was the last one released by the NIST, the American National Institute of Standards and Technology

And once we have these basic components, we've now got to develop algorithms which put them to use?

This is what we call 'distributed algorithms', which will have cryptographic protocols

These are algorithms which each component will use in the hopes that it will comlunicate with the right person.

'Security' is also about various properties

Which properties does one want to have what level of security, so that the data that you wish to share remains secure.

So for example, if you are in a transaction with your banker, and you send the codes to your bank card, this code must remain a secret,

so that it's not visible to everyone else

Another property is that you are able to communicate with the right person

So this is what we call the property of authenitification

Am I sure that when I communicate with someone that I am doing so with the right person?

And, now that we've got these two basic properties, which are the two most studied, there are other properties,

such as restrictions to personal privacy - if I were to vote electronically, can someone discover how I voted?

If I travel and I use a GPS, is this information secure, can someone find out where I am at any given time, etc...

And finally, the last piece, when faced with a breach in security, how can we protect ourselves?


In my opinion, these are the three components for a security protocol,
in order to have a minimum of security,

use the right basic components and protocol, which is for the designer to do that

define on which properties we are going to develop these various basic components,

and finally, what is the strength of the security breach?

Has someone simply listened in on a message which you have transmitted,

Is the breach capable of blocking communications, replay messages?

Can someone imitate someone else, etc, etc...


So it become very important to define these three things.



And so, developing a cryptographic application, which uses secure cyphering methods,

is etremely difficult.

Those that do this earn the trust of the users if it works well

It is very easy to lose the trust of the users the moment someone has detected a security breach

It's not necessarily your everyday user that will make you lose the trust of all of your users, but rather if someone publishes information about your protocol,

and then everyone knows that your security system is vulnerable

And that situation the trust in your system can completely fall apart in a matter of minutes

So earning the trust of your users can take years, and losing it can take only a few moments.

If, for instance, tomorrow, someone tells you that there's a document containing the information of every bank card in your system, it's finished,

no one will ever want to use their bank card, they'll be too afraid to lose their money



So, how can one be convinced that their protocol is secure?

This is what I am going to try to explain during my presentation

One possibility is to do what is written here, to help you think more about it,

You publish the protocol, and you wait for just one person to discover a security breach,

So you can wait, and the question becomes, 'How long should you wait?'

6 months?  1 year? 2 years? 3 years? 4 years?

In 2012, myself and a colleague of mine, we broke into a protocol with had existed for 17 years.

So we cracked a cryptographic primitive, we found a flaw in the protocol which had been used for 17 years

So, it's not necessarily easy

Wouldn't be better if we could prove, mathematically, that a protocol has not been breached, under certain assumptions?

And so, to prove this, it's difficult, we could do it by hand, ok, that takes time, and is labor-intensive

but we would still have the same problem, how long will we wait and be convinced that we have indeed proven the security of the protocol?

This is pretty much the same process as this one, 

You publish your proof, and you wait until someone finds a flaw in your system,

and you hope that no one will.

And the so the approach that I'm arguing for is to say that, rather than doing this one here,

why don't you use computer assisted security?

What does that mean?  That means the proofs will be performed automatically

So it's not us who will perform the security checks, but they will be done automatically

and this with help of formal methods


So, if we take a look, here we have the cryptographic protocols,

which will have to be developed,

so there are designers that develop them,

and employ cryptography, mathematics, distributed protocols, communciation channels, etc...

on the other side of things, we've got our attackers who try to break into this, in order to have access to information, services, redirect money, etc...

And, the security team, using formal methods, if we are using the formal approach,

we are both thinking about the designer, because we will want to understand what he has done so that we will be able to produce a proof,

but at the same time, we want to understand the perspective of the attackers, but not necessarily the evil one, but moreso those that are trying to uncover flaws to improve the system, and not benefit from them

So sometimes we've got this dual-role, and each time it's rather difficult because we have to understand what the designer is doing as well as try to put yourself in the shoes of the attacker who is looking for the flaws

So, back to the beginning of the story, how are formal methods used to create security?

It all started in '95, thanks to this gentleman here

This gentleman developed formal methods under the checking model and developed tools, and took one of these tools,

and used it to discover an attack on the protocol of these two individuals

and these protocols had had 17 years of use

so he found out about the attack 17 years after the fact

and this was a real revolution because these two gentlemen here

Schroder and Lowe, they had developed a proof, stating that their protocol was secure

however, they had only developed a proof that their protocol was secure for a single attacker, with one user session,

in fact he discovered an attack usingtwo sessions,

which I will try to explain next 


So the first hypothesis we're going to make, in using this approach,

is the 'perfect encryption' hypothesis

The only way to decypher a message is by using the key

so if you don't have the key, you aren't going to be able to access the cyphered message

And we're going to take a closer look at the properties of secrecy and authentification

What type of breaches are there?

Active - where the attacker is able to block messages, change protocols, and control the entire system

so the attacker can see every message

So the protocol introduced by Needham Schroder - 

A => B : {A,Na} Pub(B) Alice, who sends to Bob, her name, any given number, which she has just generated, cyphered with a public key from the recipient, Bob

This person, therefore has the cypher key, they can open the message, and get the information

they say, I'm going to confirm to Alice that I received the message,

so I put the given number, and I share a new secret number which I have chosen, Nb, which I send to Bob, excuse me, which I send to Alice

All of this cyphered, with the public key from Alice

What does Alice do?

She decyphers this message, and she verifies that the random number that she has sent here is the same that she had received from Bob

that she knows that Bob was able to decypher, and so it is Bob that returns the message to me

Right, that works

Alice confirms to Bob that she has in fact received this message by resending the random number that Bob had originally resent, cyphered with the public key

So it's this protocol here, proven 'secure' by these two programmers, and they proved this under the assumption that there would be only one protocol session done

Which is not necessarily the case, and the attack done by Gavin Lowe, discovered by an automatic utility, has shown that there was indeed an attack on the system

So, the attack is found on Bob's end

This side here

Bob is going to play exactly by this protocol here

In fact he's going to think that he is communicating with Alice,

but he will actually be communicating with someone other than Alice

He's going to be speaking with the attacker

And, Alice will participate in another session with someone else, who is the attacker

But she doesn't know it's the attacker; she will then communicate with someone else other than Bob

Bob thinks that he is speaking with Alice, but in fact he isn't

How does this breach work?

So Alice starts a session, here, from this protocol, with the attacker

Alice sends her name, a name which she has just generated, cyphered with the key of the attacker

All that has to be done is replace B with it here

The attacker can then decypher the information, get A and Na,

and send to B using the public key

It's a public key, to which everyone has access, and there's no problem

What does B do?

B follows the protocol to the letter, they receive a message, cyphered for them, sent by Alice,

They decypher it, they take the first part, a random name, and they generate the new session key (Nb) which I send back cyphered with the public key from Alice

It's exactly what is written here, and they send it back

They send it back to 'I', which intercepts it, but 'I' cannot decypher it,

So what does 'I' do?

'I' tranfers this message to Alice, Alice decyphers the message, which is exactly what she was expecting, using the secret key, which she has,

and from this message, verfies that it's right, she sees that it's ok,

so it is indeed 'I' that decyphered it, and 'I' that cyphered it as well, so I'm going to respond; 'Nb', which is the content of the message in question,

and so she's going to respond with Nb cyphered with the public key of 'I'

so then 'I' gets Nb, decyphers it, and sends it back to Bob,

for Bob, it is exactly this protocol which has been performed,

Bob believes that he is communicating with Alice,

but it is not the case

He is in fact communicating with someone else

and so this attack here made a sort of revolution,

to say that we are able to analyse correctly a protocol of three lines

and to prove it, it went unnoticed for 17 years

and so today we have developed formal methods in order to be able to analyse these protocols

So starting from that year, '95-'96 (depending on which moment we consider the attack was discovered - the publication of the attack or the development of the tool, which was slightly beforehand)

We have a real success story concering the formal verification techniques

So what I have put here in red is either the proofs that a protocol is secure, or the attacks

So in 2001, it was able to be proven, with another tool, that the sending of certified email was secure, that there hadn't been a breach

In 2003, a breach was discovered, such as Kerberos 5.0, which was quickly rectified, but was one of the most used protocols used in Communications

And, in 2008, a breach was detected on a Google application,

where you would connect only one time, with a login and password,

and which would give you access to every Google service

rather than having to enter in your information for each service


And so thanks to a tool, they were able to find a breach

and, in 2008, the first proof of TLS, another communications protocol, used in SSH, something we use often, as soon as there is a 'https' 'scp', etc...etc... was made in 2008

And so here in purple you can see each of the tools that have been developed,

with totally different approaches, in order to be able to perform verifications on these cryptographic primitives,

and which continues, in 2012, there was another one

Among this list of tools, there are those which are more or less effective

faster or slower, more or less long-lasting, more or less easy to use

The most interesting of these is the one proposed in 2010,

which is the tool TOOKAN, developed by Graham Steel

while he was working at the LSV Laboratory

This tool takes a USB security key, it is plugged into the computer,

and with reverse engineering, is used to propose a formal model, launch a checker model, and detect any attacks on your USB key

In his research on these API, these USB keys, he analysed every single one of the keys in the literature, and the great majority of them,

nearly every single one of them, had been breached

So he contacted the individuals, and certain individuals among them, nearly all of them, responded, 'That's not possible, we don't believe in your findings'

Ok, very well

And one or two companies, decided to contact them in order to solve the problem

So, I don't want to speak poorly of our friends in the industry, but 'sticking your head in the sand' , I'm not sure it's the best policy...

So here we are, a little reminder of what we had before


So my contributions in the field of security, are summarized in these three points:

I developed automatic techniques to analyze basic primitives,

which are methods of cyphering

there exist many of them, and I studied a number of those,

then I was very interested in wireless receiver networks,

and I proposed a secure routing algorithm for wireless communciations

and, lastly, on which I am going to speak today, I developed formal methods and definitions, for the protection of personal privacy and security

and this for electronic voting, auctioneering, and e-testing

So I am going to speak to you about these three subjects today

If you any questions, don't hesitate to ask



Ok the first subject; electronic voting

So I'm going to speak here about two things, the analysis of weighted voting, and prove to you, or explain to you, that one person under attack is all it takes

So first of all, online voting, which is already used in Estonia, it is also used in France, for those who are living abroad;

expats can vote online, so they have to have a certificate, a password, etc, etc...

but they can vote online,

In Switerland, here is a screen capture of an online voting system,

and the Swiss vote very often, they've got a very involved democratic process,

they are asked to vote once or twice a month, for say, the building of a school, or something else,

And so for the Electronic voting protocol, we've got multiple properties that we will want to verify,

For example 'Fairness'; it wouldn't be fair if, say one day at lunch, on the news, they were to broadcast how many votes one candidate received over another 

so that wouldn't be 'fair'

or if it was always the same person that won the election

You also want to make sure that only those inscribed on the voter lists, under the notion of 'Eligibility', can vote

Another property is that each of you want to be able to verify that your vote was in fact counted; 'Individual Verifiability'

Another property is that you want to be able to verify that the sum of the votes corresponds to the actual result - this is known as 'Universal Verifiability'

You want to make sure that the result is right, that it can withstand system problems, survive system breakdowns, 

and here we've got three properties which deal with personal privacy

which we will study a little closer; respecting privacy, absence of receipts, and resistance to coersion

When we started on this, we looked at the different models which existed on respecting privacy,

and it seemed to us that it wasn't necessarily easy to be able to take a literature protocol and to verify if it had this or that property

And so what we came up with was a definition a little more focused than this notion of privacy, the respect of privacy,

an analysis of votes, while taking into account their weight, as we don't always calculate votes according to the same weight systems, in certain situations,

and finally, we showed that attacking one single person was sufficient  to breach the system

So just let me go over these two last points quickly:

Concerning the results on respecting privacy, how can we prove that no one can obtain your voting choice

What we will prove: we have two voters, Alice and Bob

and we'll suppose that Alice will vote 'Red', in a situation in the first vote, and in the second vote, Alice, I mean Bob votes 'Blue'

And we're going to swap the situations

and if from the outside, it is impossible to discern one situation from another, we'll be able to say that their privacy is intact

We can't know if Alice has voted for 'Blue' or for 'Red', even if we swap them

There's no way of knowing

This is what we have called the 'Privacy' property, and which was studied in the literature, by mutliple authors, under this form here

Now, if you take weighted voting, and if you say that Alice has 66% of the vote,

and Bob, 34% of the vote

Well, necessarily, the result will be distinguishable in this situation here and here,

and you're not going to be respecting their privacy any longer

You know here for which she voted, Alice, she voted 'Red', 

and here, Bob, voted for 'Blue'

so in certain situations, with weighted voting, we can't gurantee the respect of weighted voting

However, in other situations, like this one here, it is absolutley possible to find a situation, where we can switch the votes, and thus respect their privacy

And so, here we see easily that there is 50% for 'Red' and 50% for 'Blue', and we don't know who voted for what, neither Alice, Bob, or Carol, despite the different percentages


And so here we have offered a definition a little more general, which can be applied to weighted voting, which states,

'If the results between the two votes are indistinguishable, are equal, excuse me, so here, therefore, we want it so that the two situations are indistinguishable

But only in the case where we have the same result


And so, it follows as such, if the two results are equal, we want therefore that the two vote results for Alice and Bob, even if we have switched them, are indistinguishable

So that is the first definition for privacy


Now, another interesting property is here; what I have drawn here, which depicts receipt-freeness, the absence of a receipt

Why would you want the absence of a receipt? So that you selling your vote can be avoided

Imagine if there would be political party that wanted to give you €1OK if you can prove that you voted for my candidate, and as such you could buy all of the votes in an election

And so, in order to avoid that, the voting protocol has to respect the receipt-free property (absence of a receipt)

So what is this property?  It means that the voter shouldn't be able to produce a receipt which indicates for whom they voted

So that's what we want

So what we have here is that Alice gives her secret information to the attacker, and in the second situation, gives false information to the attacker

And so with this, we can prove that a protocol doesn't generate a receipt, and therefore is secure

We can then extend this to multiple malicious voters, either it's Alice, or it's Bob who gives his information to the attacker

And the question becomes, how many malicious voters must there be in order to prove the security of the system?

If it's Alice that has been corrupted, is that enough?  Do we need to have both Alice and Bob corrupted to know?  Alice, Bob, Charlie, etc, etc...

How many people need to be corrupted?  Do we have to consider every possible case?

What we have managed to show, is that in having one single person (S = Single Person Corrupted), or mulitple corrupted persons, is the same

So under any reasonable hypothesis, corrections to the protocol, and thanks to the modularity of certain parts of the protocol,

we were able to show that having one single person which was attacked, is essentially the same as having multiple attacked people

Which considerably reduces the number of cases studied for a formal proof

So we created this definition for weighted voting and for classic voting, and so we showed that one single person under attack, 

was all that was needed



So now I'll go to the second part, which will focus on auction sales

and in these auction sales, we're going to speak about this property here,

23 MIN

which are similar to those of the voting properties

After that we will speak about verifiability, which is an important property

I'm going to show you an example of protocols that have good properties

And finally, we have developed a system which which validates these properties, and which can be understandable in your language

That is to say without any technology other than physical tools

So are going to in fact physically build a box to do that

So e-auctions have been developed over the last few years

You might be familiar with this one here in the middle

But, we can buy things on online auctions for example like here, wine

We can buy all kinds of things online etc. etc.

There really is an online auction for just about any product that you can imagine

And of course each of them uses a protocol which guarantees security

If we take a look a little closer at online auctions

Every transaction implicates three parties

First of all it implicates the buyer, here the people who want to buy at auction

So of course you're going to have winners and losers in this transaction

There will be the seller the owner of the goods, and often you'll have a third-party who is usually the one to organize auction

So this party here doesn't have the same interest as this other party nor the third-party

So each of the three parties have different interests, and will come back to that later

Why because, this person can finance themselves based on the number of participants

Or they can take a percentage of the sale price etc. etc.

each of the business models behind these transactions are are are totally different each time


And so there are multiple types of different online auctions in the literature

Each of them being more or less complex

Let's imagine each of you want to go to online auction and for example by this beautiful Apple laptop computer

I'll sell it on online auction, so each of you have an envelope you write on a piece of paper what you want

You put it in the envelope, you seal it

Of course you put your name next to the price that you've offered

I collect all the envelopes, I hope in all of them I think the highest bidder, and I decide who the new owner of this beautiful Mac is

So that is how a "Sealed Bid" auction works

So another way to do things is to operate the auction from highest bid to the lowest bid

This is known as the English auction

Another idea is what is done at the tulips market in Denmark,

In Holland excuse me

So how do they sell tulips in Holland has at work

The price is set at the highest price possible

And the price descends based on clock and as time goes by the price goes down

And the moment someone in the auction house raises their hand, he buys the tulips at the price for the clock stopped at the moment he raises hand

So that's how that works, we've got the same thing it's called a Dutch auction

We set the prices highest possible and as the price descends the moment someone says yes they buy the product

We could imagine that the one that proposes the highest price buys the product

But psychologists have obseverd that we could do something called the Vickrey auction

Which is a situation where you win the product as the highest bidder, but you only have to pay the second highest bid

So that allows the auctioning to the go higher

Solid you think about that, that's kind of interesting I think, being able to go to 'what' price

So there are many systems, and all of these protocols here exist in electronic format

So were going to take a good look into all of the properties for online auctioning

Fairness, verifiability, the fact that we shouldn't be able to cancel transaction

The secrecy of the bidding price, the absence of a receipt, resistance to coercion, and the anonymity of bidders

So to get started here we will have to define a couple of ideas

So we need to define events, so the event 'bid' (p, id)

So this identifies bidder 'id', who makes a bid at price 'p'

Okay following that, recBid (p, id) - this represents price 'p', which is made as a bid by bidder 'id', has been received by the one organizing the auction

And so the model used is a bulletin board

Which means a sort of whiteboard or blackboard on which we post everything that we receive

So the one which has won, as soon as it is received, it's posted up on the board

And finally, won(p, id) - this means that the bidder 'id' has won the auction at price 'p'

So here the first property is "non-repudiation"

You don't want someone to be able to say that he hasn't made an offer (in the event that they have)

So you have to impose on every trace of your protocol, each time you've got someone who wins and auction

That they are in fact held to their commitment

That is this property here

so you want to be sure that at every step and trace of your algorithm, that every time someone has made a bid and won a bid you can record the name of the bidder, and the price

Secondly, let's imagine that Alice makes a bid and it is greater than that of Bob's

And in this situation it's imperative that no trace exists

So that Bob could win the bid as it was Alice in fact who made a higher bid

Even if Alice were to give all of her information all of her keys to the attacker

Another property is that you want to be sure that the highest bidder in fact wins

So in the situation Alice has bid more than Bob

sorry Chuck, it is imperative that Chuck does not win the auction

And finally two other properties, are both 'non-interference'

Here, you don't want one auction process to influence another auction process

You need there to be level of fairness between the two

So here we have defined two principles

A strong principle and a weak principle

Because in the strong principle, we don't even want the number of participants to change

We want to do the least amount of participants to change

So this is a property that's very difficult to obtain

So we've also proposed a version of this principle that's much weaker

Because is not very realistic to insist on having the same exact number dispense at each auction

So we have developed one or we can change the number of participants

So now we come to properties dealing with the respect of privacy

A proposal that was made in 2010, it's imperative that these two situations are indistinguishable from one another

Alice has bid €20, Carol has bid €100, and we want Alice to be able to counter bid but so that both situations are distinguishable

What does that guarantee? It guarantees that no one can learn what has been bid by Alice

Because in many auctions, we know how much the winning bidder pays

We don't want to be able to make a connection between who lost and how much they lost by

So we add a third person, and we want to make sure that each situation is indistinguishable from the other

So if Alice in this situation bids €20, and Bob bids €50, it's again necessary to guarantee that we don't know which one bids what price

Just like voting situations, but in this case it's applied to auctions

We could also expect a much stronger property

A 'strong anonymity', but this one can also include the winner

Which means if we swap the bid of the winter and change the lowest price, these two situations remain indistinguishable

So this is a stronger property

And a property in the middle, so the bid of the loser doesn't change

But this one is a little weaker

Because here it's the same price

So with this we were able to construct a 'hierarchy of privacy'

So the one which we had before shown here

We've added something, we've made a connection with the notion of privacy as I've told you earlier

And we extended that to the absence of a receipt

And this is how we have a whole range of properties

So we were able to look at this and analyze many different protocols

So it another property, which we spoke about earlier, is the property of 'verifiability'

In auction protocols, each of the three actors have different interests

This person (the winner) has to be sure that they have won

This person(the loser) has to be sure that someone else has won

And not if someone one but someone else ends up with the item

And this person (the seller), wants to be sure that they have made as much money as possible

That is to say, that they are being paid the highest bid, the auctioneers

And so for this we defined multiple properties

Which we referred to collectively as 'verifiability' properties

The first property in verifiability is the property of authentication

So in this situation we want to ensure that every party's bid, the loser, the winner, has all been recorded

So here we have a proof of authentication

We also want to ensure that the offers that have been made are integrated in the auction process

If you bid €10, it's not the same as if you were to bid €1 million

So it's important that your offer isn't changed

So this is called the 'integrity' property of an auction

Another property is that the loser wants to be sure that has indeed lost

He wants to be sure that his bid is in fact lower than the bid of the winner, but without the others seeing the bid of the winner

And finally, the winner wants to be sure that he won with the highest bid, and that is in fact his bid which one

And that there wasn't someone else to one ahead of him

And also the one who is selling the goods, wants to be sure that the calculation of the winning bid was done, and not the one who bid the least who was declared as the winning bidder

Because in such situation he could lose money

So here we can see we have put forward some definitions, we have proposed five definitions for this

The properties of authentication linked to the registration of the person, the properties of integrity, and the properties of verifiability following the results

To be sure that either you have in fact lost or in fact won


And now I'm going to present to you the Sako protocol

Who, whom we spoke about with a formal proof, uses the majority of these properties here

So the Sako protocol is very intuitive and quite elegant

It was presented in the year 2000, and it supposes that you've got a lock and a public key for each of the prices proposed in the auction

So 1, 5, and €10; everyone's got access to this

So the authorities publish the keys here we see the keys and the public has access to the locks so everybody can use my locks, and everyone has access to the public keys for every price

The authority distributes a constant C, and if you'd like to bid a certain price you take this constant, and you cipher it with the lock

So for example I want to bid five euros, I take the five euro lock and I cipher the constant which I was given

If Jean-Marie wants to bid one euro, he takes the public constant he takes the lock at one euro, and makes a bid

The authority collects all of the offers made by the participants

After each of us have put our signature so Jean-Marie has signed; so Jean-Marie has signed to show that it was indeed he who made the bid, by electronic signature, and I have put my signature as well

So how does this work? First step, we need to make sure that each of the signatures are valid

To make sure that it's only the people who are registered to bid, so we so we make sure that

Second step, were going to decipher; in order to do that, and to and to ensure that we don't reveal the bids of the losers, or going to start by using the highest key

So we take this key here and we try to decipher everybody

If we manage to open it, then that is the €10 key

Do you remember the highest key?

So if it's for €10, and here it's why fine for the constant, then I'm sure that somebody made a bid for €10

But here it's not the case, I bid five,Jean-Marie one

So that doesn't work so of course it's the second key

And the second key this person here who signed, is one who won because they bid five euros

And so this allows only the highest bid to be revealed

The lowest prices or the lower prices, will not be revealed at all


So how can we verify all of the properties? The first property, were going to verify the signatures, so it's only the people who are going to be registered, so the authentication is going to be verified

everyone's also going to verify that it was indeed the winner who was registered

because once he's won here, we can verify that he was in fact a registered bidder and they didn't cheat

So that's two properties

So the authorities as it goes along publish the locks, which means everyone after-the-fact, can redo the calculations

To be sure that this lock goes with this key and if I don't find it then it doesn't work

We can verify the results, because we are able to perform ourselves all of the calculations

So that's what guarantees the property of verifiability for everyone

So all of the participants can verify that the winner is indeed the right one, and they can also verify that it wasn't their bid that should have won

Don't we also had some fun working with two other protocols that we found in literature, for which we had more problems

We found breaches for each of these properties here

We found these with formal tools, ProVerif, and CryptoVerif, which are two of the tools

So now I'd like to move on to the part destined for my grandmother

In order to propose a protocol for auctions without using cryptography but secured, with the guarantees as here, the Sako protocol

So this was strongly inspired by Sako, and the idea comes from using a a cryptography protocol is good, but perhaps is to complicated for everyday users

So we wanted to do something simple

And this is rather accessible for a non-expert

You really have to be an expert in cryptography to understand how certain protocols work

And so the idea was to use physical properties to ensure the existence of the security properties

And so we have proposed two protocols

The protocol Cardako, and the protocol Woodako

So Cardako, because it comes from Sako, and it's done with cardboard,

And Woodako, because it's made with a wooden box

So these are two physical applications of the 
Sako protocol

And we have proven this, I'm going to prove this to you to show you that it works, if you were my grandmother,

But I'm also going to prove it to you, we have proven it using formal methods to show the protocols are secure

So the Cardako protocol is very simple;

So each of you have a bit of card stock and envelope marked so that you don't have it upside down,

On this card you've got some designs to show you the different prices, P1, P2, PM,...

The various prices for which you can bid

And you punch a hole in the card with a whole pleasure like you've got in your office,

So you make your bid here

I'm what you done that, you put this in the envelope

You close the envelope, you put your stamp or signature on the envelope and then you close it

And you sign the envelope

So I'm organizing the auction, I collect all of the envelopes

I mix them up, and what I do is I try to punch a hole with a needle the highest bid

If this is the highest bid; if I go through the envelope that's okay it doesn't matter, if I go through the card with the needle then I know that a whole has been punched

If I can't go through it that means there is no hole

And so I do this for all of the envelopes at the highest price bid

If I can't pass through, I know that nobody bid the highest bid

I start this process over with the second price, I try to pass my needle through the envelope without opening the envelopes for anyone

And the moment where I come to a card that my needle passes through I know that someone has made a bid

So that's exactly how we see the locks from before

So here I'm sure the summit is one, and I open it and I see the signature on the card

So here we have the Sako protocol transposed onto a physical procedure

So we verified with all of the properties; there's just the issue if the voters are dishonest they can open the envelopes, and know for whom other voters have voted

Excuse me, bidded rather

So in order to avoid that, in order to create something more secure

Where you see all of these green X's, we've got the Woodako protocol

This is a version it would in a box, so this is based on the problem, on the following physical property,

We've got marbles, and the marbles are going to pass through holes

But these big marbles cannot pass through these little holes

So this is the idea that we had, marbles passing through holes

So the highest bid will be the smallest marble, the smallest bid will be the biggest marble

So here's the box that we built, we took some tools and we built a box, 

Here see the different levels, and you see these marbles and they won't pass by here but the next one and this one will pass by this hole, and all the others pass through this one, etc. etc.

So we've got levels with different holes; why are there 4? So to avoid if the marble Falls doesn't go into the whole, we have four holes to make it easier for the marble to pass through each level

So how does it work? Once we've constructed the box, where you got the different prices based on the holes, or you've got a sheet of plexiglass, and at the top you've got an individual panel for each person

So I'm going to make my bid in this column here

Jean-Marie in this column, and Michel in that column there

So how this works, at the beginning everybody verifies the box

We close it here, and everybody puts their locks on the box

Everybody puts locks everywhere, to ensure that no one can open the box if we are not all present at the moment of opening

And that we cannot open each level, that we cannot take out each level of the box unless everyone agrees

So this is for three participants

So here the boxes closed, and no one has bid for the moment

So I come into the room I go to bid, I put my marble here, and I cover the box with my personal panel and I lock it here,

I leave the room, the second person comes in, he puts his marble, his lock, and he closes it

Once everyone has done this, we all come back in, and we put this piece of sexy glass here

what does this piece of plexiglass do for us? This is to avoid potential cheater down the line who might try to open his lock, remove his marble, and change his marble

So this way no one can change their bid

And so this plate of plexiglass is put here, and everyone puts their lock on

So now no one can change after this point

It's as if we had sealed the bidding at any e-auction

And so how does this work to find out who won the bidding?

The first step, we remove the first level, and remember that the first level are the smallest holes, excuse me the first level is full

We remove it, the marbles fall, and at the level underneath, the smallest holes

If the smallest marbles fall, they fall to the bottom of the box they 
they make their way from here, and they come out here in the box

if a marble comes out here we remove the panel it means that someone bid with the smallest marble

and so they won

and how can we verify that that person one?

The losers can verify individually that they have in fact lost, by opening their box and looking to see if there marbles are still there

And the person who won the auction can look underneath, and verify that there is indeed a place where there are no marbles and that in his box there is a marble

So we've got the property of verifiability as well, for the person who won the auction

So what can happen here is that you get to marbles the fall at the same time, and in this situation just like in auction, you've got a tie and of course we have to start over, so we start the bidding again with the two who tied

That can happen, but this can also happen with the Cardako protocol

Were we can have two bids of the same type, the first lock can be found by two people

And we have verified formally that there exists the good properties

And now, onto the E-exams; so many of you are professors here, and we often have amphitheaters full of students taking exams that takes time, it's long, etc. etc.

And so there are those who have proposed E-exams

So these are exams where we can, in fact the exams can be in the program, but at least we can enter in the results electronically

This can be done on the Internet,

And so I put it, and these days it's in fashion for the 'MUC', many certificates are done on the Internet

Tell universities don't yet deliver diplomas, but they do allow exams to be taken online

So I've put the principle 'MUC', I've also put ones for language, we can take the TOEFL exam online

Cisco as well, there are exams online that we can take to be certified on using Cisco materials

And this will probably the further developed because that implicates a large number of people

And so the various roles and exam, there is the test taker, the test takers, the authorities who administer the exam, and the professors who will grade the exams

We have identified four phases, test takers have to register, who will take the exam, then the test takers take the exam, then the exam is graded, and then the test takers are notified of their grade

And here of course we have several types of ways to cheat, for example looking over the shoulder of your neighbor, cheating with a mobile phone, cheating by copying or having notes with you,

Or even worse, would be to pay off the professor, to buy a diploma

But we did see recently in Atlanta, Pascual did this a little differently

The school bought their reputation

This school had fictitious students take an exam, in order to increase their success rate

Huh...

And the school delivered fake diplomas to be better ranked, to be better classed, so an institution can cheat just as well as a student

So here we see that there are three or four E-exam online protocols,

Which already exist, and we have taken the first one to verify the example

And here what seemed important to us was to define the properties

So we defined eight properties, the property of verification, and the property of privacy

So only the testtakers who are registered have the right to participate in the exam

That would be a shame if someone who was a registered was able to take the exam

We've got to make a link between the answers and the exam

But not all the time, we've also got to verify the authentication of the grades

Whether it's the grades given by an administrator or not

And we have to verify the connection between the person who gives the grades and the test taker

The there are many types of connections that need to be established, and many phases to be established

We have established these four here

We also have privacy questions, the exam must remain secret

Before the grade is made public

The grade has to remain anonymous, however in France it's not the case, anyone can go down the hall at the IUT, and all of the grades of the group are on the wall

There are however countries where grades are kept confidential and sent to each person individually

And they're not made public

We also have to guarantee that the exam administrators remain anonymous, so that they cannot be corrupted

If, for example, it's me who grades the baccalaureat, I might receive some checks in the mail, someone who thinks that if they send me a check, I will remember that when it comes time to grade and of course grade in their favor

And finally, the results have to be private

So the Huszti protocol, it's got six phases, they've put a phase so that those who grade the exams register the grades, and that there is a key distribution phase,

Which is detailed here, and otherwise it's the same phases that we have earlier identified

The protocol follows 28 steps, I'm not going to explain all of them now,

It uses a lot of cryptography, each of the various steps in the cryptography, there is 16, 22, 28, 29 steps, each of them very complicated,

Based on cryptography, so that's what we studied

And here are the results which we obtained

We passed this through formal methods, and this is what we found

We found attacks everywhere, except for the respect of the exam questions

Even though the title of the paper is "secure exam whatever"

So it's a paper that really announces that it is secure

You want to know why? Because the most of the time, the proof that was done was done by hand, we verified this because we use cryptography

But using cryptography isn't enough, as I told you at the beginning of the presentation

It's not because you use cryptography that there aren't attacks

So this brings me to the conclusion of my presentation

I hope that you have been convinced that security comes from the design of the protocols, while taking into account which properties we want to defend

And what type of intruder model we have after that

So these are the three keys of security

And we applied this to electronic sales transactions, E-auctions, and E-exams

And each of these applications have their own particular characteristics

And finally, the take-home message of this presentation,

Building a cryptography protocol is difficult

And building a secure cryptography protocol is even more difficult

So using cryptography is a good idea

But it is not enough

So what I would like to recommend is to try to prove that your protocols are secure by using formal methods

By using the tools which exist to prove that your protocol is secure

Once you have defined your properties

Thank you for your attention, and I'd like to answer any questions you might have.