Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/98 Thanks!
Involved, so I'm going to define the
special notion of
equality just for a bit.
Oops.
So this is a violation.
This is again a genotype
that takes two bits.
And then there is there is two ways.
Two bits can be equal easily.
Both are equal to zero.
They both are zero.
So then
they're going to look like that.
So you can read this as kind
of rules.
So there is one rule that says that zero
is equal to zero.
So basically, when there is this endless
calls, this is this what we call mixed
fixed notation, where
basically the arguments goes, where
it goes. So I can write this, this syntax
where the the wall name is
bit brackets equal bracket
and and then it's use like like
it's like on a like for zero here,
then same thing for one
that one can be.
It can be equal
to is equal to one
here. Here you go.
Also in in incognito.
We like Unicode.
That's why there is all this.
OK, so I got
tricked by this indentation thing.
OK, now I can use this crucial predicate
that I've just defined the special
relation that says when two bits
are equal.
OK, great.
OK, so now I do
a case analysis on X
and then I then I and there is a special
thing that will refine when this is
obvious which one to pick.
Oops.
And this is
OK.
So here is a proof that
that not not X is equal to X
when X is zero.
The reason for why it's zero,
it's because of computation.
The X is zero. So on, so not will compute
to one and then not we'll compute
again to zero.
And then I just have to say that that,
yeah, zero is always equal to zero.
OK, so does this proof
is so, so sort.
If it's so easy that
there is the yeah,
I can ask the kind of auto mode
to find it for me.
This is not necessarily that impressive,
but generates
this. This is good.
OK. So,
OK, let's have another
example with with bits, but let's let's
move on to the next bell.
Then I have not shown no.
Usually I use Unicode everywhere, but
I'm not going to
push myself into too much
typing
in this sitting.
Yes.
All the typos I do.
This is again, some annotation
thing. OK, so there is an natural
numbers, right?
Zero one two.
And they are they are.
They are defined with this data dove that
is there zero, then six zero zero, then
then this one and six zero, then it's
two extra oops.
Then this is not your numbers.
What I want
is addition.
I'm going to need it later on.
OK, so addition takes
to natural numbers.
Yes, trade.
Eggs, my.
Yes.
Can I have this?
It's.
OK.
So for this,
I will do a case analysis on the first
one. It is either zero or successor,
then zero plus why I know it's
why that's fine.
And and if I knew that
the first argument is made of a successor
and I know that the result is made of a
successor, so I go for
that.
I can build a program incrementally
and then I make do it yourself.
Call on the rest.
So here you have to really think of this.
This one is being turned to this
like that.
And Soledad, the recursive call
of the plus function is made on something
smaller.
So that's why it's it's accepted only
accepts this terminating functions
that are defined everywhere.
If I if I miss one case,
then it says that it's time is one case.
OK,
OK, no. Now list,
or maybe I go directly OK, I
have the time for list and
then maybe I
I show it on the
complete fine.
Then I will load this.
When load is complete fine, I will do the
magic trick again.
OK. So this is sort of the same thing
that we've seen and used to be different
names. But anyway.
OK, so there is the natural numbers
and additional natural numbers.
And then
here is where we can define list.
They are either empty or
they are made of one element, followed
by a list.
OK, this is the case,
and on this list we can define the lens
function that is basically, if you think
about it, it's going from a list to
natural numbers and it's actually sort
of forgetting about elements of the list.
But preserving the structure.
Its maps need to zero.
And it maps comes to sick.
Then on this list, one can
build a crooked initial function
up and function of two list.
And one kind of proof that we can have
is to show that the
sum is improved, that we can have this we
should add
the the length
of the of the
coordination of two list is the same
of the length and the
proof collegues as this two line
function that is defined by my case.
And that's this.
And this is a proof.
And at the same time, if you read that as
a function, it's it's also as as
a function. That's that's what I that's
what I mean by it, by one system.
We have a sort of the two
are the proofs and programs are
consistent
in unified.
OK.
OK. And then then to finish
with this, we have this
demo victors.
So Viktor's is some kind of the first
basic example that we have of dependent
types inside on the side
of programing because dependent types
we actually use in all the proofs
here.
So the Typekit Viktor's is a bit like the
dipole list, except that it tracks
the length of of it, of this
vector in as a as
an index. This is the second
thing there is, for instance, the empty
list A. Victor is off size
zero and the
Combes case takes a victory of size
n and makes a vector of size six
zero. So one plus n,
obviously we can turn vectors into list,
sort of forgetting the the
static knowledge that we have of the of
the length.
We can also prove that when we when
we take the length of
of this, of this,
of this target, of this conversion
of vector from vectors to list, then
we get n.
This is the this was the original size of
the list showing that we have not
followed any elements when we were
converting this function.
So this when you might get this function
wrong, if you, for instance, forget
this path here,
but then then then the proof will will
complain on.
So some parts are crucial
because you can.
This other specification is under the
the meaning of things.
And then and and then the proofs
on the fact that if it's accepted, then
it's then it's it's
OK.
OK. And finally, the
you can happen to vectors
and here this is where the
dependent types truly shines as
the first vector is off size M and
the second is of size N and the
resulting victor is off size M plus
N. And this is the place that we defined
earlier. This was on program side
and now it's in the times.
And when you define this function, it's
still exactly defined.
I don't know if we can f both on the same
screen, but it can be
defined exactly in the same way that the
apon function on list.
So the fact that this function is
is precise about the length of things
is really sort of free.
Here we have the same code
that we add for upand it
really relies on the on some kind
of engineering of the definition.
So there's that append function that we
define work from the left on
the first document and the plus function
works on the on the on the first document
as well. That's why.
Everything sort of works works out
nicely.
And yeah, that's the that's the end of a
of the deal.
OK, so let's get back here.
OK, now and this was kind of general
ag thing.
And now let's let's go more into security
and
and. OK, so OK.
Briefly, everyone knows about public
key encryption. I hope here soon we
have just a brief
recap of the notation I use to
ask for the private key public
PDA for the public key.
And so we have an encryption function
going, and I don't put
any parentheses to pass arguments to a
function like to.
And PEKWM
takes the public key in a message and
produce the cipher taxi and the
decryption can do do the reverse
and needs the the private key.
OK, so this is pretty
straightforward.
Then you have to know this.
This picture is not as nice as I wanted
to to be. This is the
an important notion.
This is the security notion,
and this is defined as some kind of a
game that which works as
follows.
There is there is two participants
the the challenger and the adversary.
So the challenger represents the the the
good guy and and also the, let's
say, the the host system, the
the network and all the all the
console that we trust, let's say.
And the adversary here represents
all the the bad guys colluding
between the each other.
OK, and the game works
as follows the the challenger starts by
generating a key pair
of ESC and piquÃ© and
then sends the public key to the
adversary.
Adversary can now encrypt
as many messages as you want because
as we know, you only need the public key
to encrypt then the adversary
as to send two messages and you add
one to the challenger.
You can pick the the messages
as he as he wishes.
This is chosen plaintext
attack.
Then the the challenger
will encrypt one of the one of the
two messages with the with the encryption
function.
And so let's let's say
that encrypts and b where b
some kind of secret bit.
So it's either in zero and one that gets
encrypted and sends this cipher
like C to the adversary, then the
adversary is to tell
which one has been encrypted.
OK. And we say that if
if the adversary can do
can guess
in a sufficiently often,
then we can claim that the encryption
has been has been broken.
So formally only this is defined that
there is the probability of the adversary
of winning.
So if guessing the right bit
and we want to see the distance
of this probability to one half, that
is what we call the advantage.
So if if you get really,
if you guess, always
good and then then you have
a good advantage and a good advantage is
being is being away from one half
and one half is when we interact on them,
when you answer, always the same thing.
So the worst is advantage zero and the
best is advantage one half.
OK,
so so we,
we we we can model this, this
adversary, and there is this way
of doing so. But one way would
be to say that the adversary comes
into to bat
the parts that that computes.
There's two messages and you win em
one. This is the this is then
modeled as a as a record here and
off to bounce em and be primed.
And the first path takes
the public key. As I say, some randomness
in this the I'm going to speak
a bit more, but they're running this
later.
Let's keep that for for now, and that's
to return a pair of messages, then
be prime and take some takes.
The basically there is no stage
for this adversary, so we pass him back
all the all the all what he got
before.
So. So it gets the same public
key again and it gets the ciphertext
and he gets to to pick two to decide
which which bid was
OK.
And it doesn't does anyone a
and doesn't does this game previously
sounds trivial to break,
though it is that it's supposed to be
defined so that all the trivial attacks
do not work and that all the
all the remaining depends on the way to
the encryption works.
So there is one trivial attack
that is emerging that you
and encryption. Function is
deterministic, then
then it's pretty easy.
And my adversary can pick
any two messages and one in one
as long as they are different.
And then the my test to the full
to be prime would be to simply compare
the ciphertext I receive with my
own encryption of M1 because I
choose the message and I can encrypt them
so I can. I can compare and live.
This encryption function is
deterministic. Then this works, and
the the proof sketch would be sort of
as follows that the
encryption, if it isn't deterministic,
then it means that number is equal to M1.
Therefore, that being equal to one and
therefore that that I guess be
two. Why is this game
still used if there is this?
The point is that we are not supposed to
to have an encryption function that is
deterministic. I mean, at least then it
will fulfill different security
criterion, but not the semantic security
of in s.p.a and all what
is above it.
So, so does the
encryption should be randomized.
But if you think of it of the what
do we call now? Text book RSA,
it's defined like that.
That is the public keys as
a pair of E the exponential,
the encryption exponent and end the
modulus and then encryption
is just added to the
module end.
This is completely deterministic.
This thing.
So yes, RSA, if
it's implemented like that, it's not
secure. According to this
in s.p.a definition.
That is, you can have an adversary that
can pick the two messages and that can
have a clue about which one you encrypt
it.
The thing is that RSA is not
good at encrypting and encrypting
particular messages.
It's only good at encrypting random
messages, then it's fine if
Em is picked out on them.
So that's why now it should.
RSA should be used as
you encrypt, you pick
em at on them. And this this.
This is not your message, but
is some kind of secret key for some other
encryption. Let's say a symmetric
encryption scheme
anyway.
So randomness is paramount.
Okay, so now we can see.
So this way, I sort of eden
this one on this thing before and
now that is made explicit.
So the way we can, we can represent this
game with the two boxes.
We going to represent it in with this
expert function that takes
the baby and
we can choose the mode where
be zero in the mode where B is one,
then it takes an adversary.
This is a and then it takes
all the randomness that is necessary in
this game.
So
one one, one point of this
of this exercise is that usually the
randomness can be made a sort of implicit
in the in the discourse.
But here we really make it explicit
as we think it's a it's
it's it's really necessary
to to clearly
see things.
So anyway, so this this game's policy,
like there is this full lines, PCA is
created out of the generator, then
it's sent to the to the adversary,
to empath, then
the end, the message is encrypted and
gets called C,
and then we can pass C to the adversary
again to get the resulting
bit.
Then then the little B in the game
function just below.
Now it takes part, becomes part of
the randomness. We pick this B at random
and and then we obtain the the game
I was I was mentioning,
OK, so there is another trivial attack
that that is what if
what if the size gets to,
uh, the size gets to
lick?
So basically, if you want one
any messages as they are different
size, then
then a way of of seeing
which one has been encrypted is just to
look, is this the the size
of the ciphertext I get of the same size
of the encryption of M one?
So even if i m one with a different
randomness, then then
it will usually
keep two schemes that preserve the size
and the size do not depend on the runner.
So. So this would work.
So that's why in the actual definition of
of of
NCBA is actually to
where the two messages to be of the same
size.
Right. So the of course, they knew about
that. So the the the real definition of
s.p.a that M01 in one of the same
site
and that we only consider
on Thembi's encryption.
OK to define this to trivial attacks?
OK, so now let's let's speak about a bit
a compression
together with encryption.
OK, so what if both are good and
we want privacy?
We want to save some bandwidth
on this storage.
So let's put them together.
So first attempt we come, we
encrypt and then we compress.
This is useless because
compression after basically
encrypted data looks like on them.
And there's one thing that
compression can't always
do as well encrypt random.
This is a matter of entropy.
It's so basically
it works, but it doesn't compress much.
So let's do the opposite.
So encryption after compression and one
way to think of it is to say that
you take we take an encryption scheme and
then you produce a new one that will
systematically just before encrypting.
We systematically compress the message
like, like, you don't
think it always you compress and then you
encrypt.
OK, so we get this information,
and that's the part that is broken.
So this is the this is what
the where the conversion
oracle comes in.
So basically,
the pair of messages can be any two
messages that have the same size
right to fulfill the requirements of this
game, but will compress off a different
site.
And I bet that any,
any pair of any, any kind
of compression scheme better
be able to to compress better so messages
than some others because we know that it
comes, compress all of them.
So. So basically, one miss NGO
could be sort of plenty of zeros
and an M-1
could be some random bits
string of that's of that same site.
One will compress very well and the other
will not.
And so,
so that way we can write the adversary is
just to look at the size of this
ink function.
So, so this is well known for for a long
time as some kind of a surgical attack
that because in S.p.A
is not predicting the length
of the message.
If you can and could, if you can
make the length depend on the
on the on the content, then
then the intrusion plain text that I can,
then then wear it again.
And this works basically for any
compression compression scheme
and this assume from any encryption
scheme, which is you can can even
be in situ.
The biggest one?
Yeah.
And we limit the size of the
plain text message by encrypting.
And basically that the cipher takes does
not depend on the anonymous.
That's a technicality that that's usually
OK.
OK, so now we get closer to this
breach at that is
that was first was clear.
It was the.
In 2012, it was the crime attack
which was targeting
the competition that was building in
as was not widely used.
So this just got turned off
and this was mitigated.
OK,
bridge.
So and so
it's an improvement on the.
So so what we saw is that in theory, this
was this was broken since the since the
beginning. Each time you countries,
whatever you do, each time you compress,
then you encrypt
in CPR, it doesn't help you.
It's an
injury and it is considered kind of the
the lowest surgical
security solution for an encryption
scheme.
So it works full and this bridge attack
works. And so what?
I mean, so the so this kind of attacks
that they they go further, they they they
use a lot of ingenuity and and
and tricks to to not
only make this work in theory,
but works in fact practice
and not only to recover yourself one
bit in the case where you repeat the
messages, but recover all the secret.
That's that's what gets interesting.
So this bridge attack works on the
on.
It should be responses and
can get secrets
like CSI of tokens
because they are, they are.
They appear into responses and they
usually reflect part of the
part of the input.
OK, so from the from the paper, we can
explain the ODIs
this year
and make it bigger.
This this attack works is that
the first thing is is, is, is,
is a you al where there
is, where you get, you have.
In the perimeter zoo, you can
you can put something that looks like
this can areas is as
could be CSI if token
equal. This is something that that is
just the prefix before the secret
that that is known.
Then you put your guess and
then you, you will get
you will get as the response, something
that includes your guess.
And that also contains the secret
below this canary
the sick.
So the secret is these six three four
zero.
And the thing is that if your guess is
good, then the competition
will work better.
And so just by looking at the size
of that, because you don't get this, this
this this response in clear text, this is
not meant for you.
The set up works like that.
And there is.
So there you have a real man in the
middle. You can just sniff the
the the resulting
from the resulting responses
encrypted and just the size of it.
This is what you need.
So you will make a request
that you can do either by forcing the
the victim to do it or
while in Syria, you can do it because you
have the public key. So if it's if it was
just a matter of public encryption, then
you have the public keys or you can send
messages to the to the server.
In practice, there is
enough stuff that makes
makes this difficult.
So let's say that that you fall the
victim off to send a particular
request and then all of the
responses, you can only get the length.
But
but when you get when your
guess is when the first bite of
your guest is right, then it will likely
to compress better then
than when it's not because there is there
is patterns that repeat and that's what
compression is here for.
So you can then therefore recover bye
bye bye buys all the all
the secrets in this way.
So there is technicalities
that I will mention a bit later
on.
OK, so this was the set up.
No, I need something similar.
Yes.
So
so basically, it is.
This would be some kind of a
mock up. This is some kind of a mock up
of what is of what the base version
of of breach would look like in
in regard to this.
So this this
so I use this this
for this presentation.
I thought it was more fun to speak about
an attack mode and speak about
an encryption scheme on
the construction.
Yeah,
it's more fun to see to see an attack
than to see why something is secure.
And usually it's more technical and
to see why the proof of when something
is so in the end, this
is what I have about breach.
Really, Nanda is basically just a just
a mock up, but
and also this compression
rifle that we saw before, that was
the theory behind it.
So in the real bridge, there is lots of
technical challenges that they are to
overcome the fact that there is not
only the compression works
in in two layers and there is some of
my encoding that that makes the
difference this this the
the basic version.
So then there is this to transmit it.
So I just want to to to
in case in case you don't know bridge
well that that don't get confused
by this simple knock.
This is more advanced than this
is.
So block ciphers, can I the length, but
not totally.
Sometime you, you can only make
a guess on the smaller
pair of time. Or
anyway. So yeah, we have plenty
of time for creation.
So as a as a, as a future work,
so this we we work on,
on
or end goal would be to verify
a voting scheme based
on on on cryptography.
Examples of that he'll use or
put out, they are somehow based
on the mixed net.
And to do this, we need to
sort of verify all the all the basic
blocks of offer of encryption
before there is emblematic encryption on
interactive zone knowledge proofs,
things like the now transform.
There is plenty of roadblocks
before that, but we we are we are getting
we are getting closer.
That's the end of my talk, and I we have
plenty of time for four questions.
Thank you.
Are the questions from the internet?
Yes, there are.
Go ahead.
I
do I get this right that, you
know, you have this you are like
structure where you have.
I am a second person from the internet.
Oh, sorry. But you
OK? Question from IAC.
Why did you decide to leave France
for computer science research?
OK, you didn't read them.
So in short, I didn't
left for necessarily for for
long.
This is quite common after Europe ready
to do the postdoc
somewhere else in a in a
in some of our country to get more
international experience.
And and I I hope to get a
position back in France.
But but I'm not that.
I'm mean, the place doesn't matter
much more than like the context on
the team and all that.
But the breach attacks still work.
If this URL includes
kind of randomly created such
an idea because then your guess
compresses together with the secret
or or and the
Session ID.
So you think in the case where
where decision I'd as
some patterns that will repeat with
the with the guess.
Yeah, I think
this is this is sort
of unlikely.
And if the sort of thing is that if
decision it is the same over
request, then I think it doesn't
help it.
It's also the same one of the secret
changes every time.
Yeah. So if the secret changes every
time, this is one of the way off to meet
it. Is this headache?
Yes.
Okay. We have another question from the
internet.
One more question from IAC
typically proving a protocol need
to explore a big database.
How do you prove that your exploration
function is exhaustive?
So there is two to two main
ways of doing this kind of proof.
That is, and
these are relying on what we will call a
model of chicken and the other.
It usually depends on really exploring
that, that space.
And in crypto, we would like
to have huge spaces because like the the
keys are usually not
you can't really explore them.
The idea is that we do more of symbolic
reasoning where we can deal
with this, with this functions that
really do in
that we do explore
everything, I mean, like every of two
power to the two to 256
bit space.
But but we don't run these programs,
we run them only symbolically.
We make them make that they are defined
by induction on their own there.
So basically, yes, we can.
We can do proofs
which will air about programs that
do enumerate a space that
is much bigger than that where we can
compute.
Next question could
be used for reverse engineer
to prove the identity of two different
implementations.
I don't get why reverse engineer
but but yes, I mean this, this can.
This can be useful for this kind of
thing. I mean, it's a if you if you think
of functional programing, it's a bit like
Haskell Plus
plus proofs that that not only
you can write a programs, but you can
also write proofs about it.
Instead of just testing that there's two
functions that are doing the same, you
can also prove that they are doing the
same.
Oh
yes, OK.
And there's a familiar
way for you, sir.
So I like the general idea very much,
but the weakest concept seems to be
that there is no real concept
for entropy in the whole
system of a form of proof.
So can you deal with
weak random generators and
say anything about the complexity?
How long do we have to listen
to this, or how complex an attack
has to be to
give total breaks
a cryptography you as a given probability
or something like this?
This seems extremely difficult to me.
Yeah. So I
expect the thing to be sort of I mean, as
we usually do to be
in mid-July as in when
when you have a particular thing that
requires Londoners would say, Oh yeah, we
pick on the numbers.
And then in practice, we use a
pseudo them generator, which is better
be secure.
So.
So the proof of that, the pseudo on them
generator is secure is when you can't
computationally distinguish it from
real random generator.
So if if the two components where
we're self proof secure with competition
or bounce, then you could merge them
together and get the final
moment. It's true that in practice,
there is always this assumption that you
pick something that's random and then in
practice you begin with a pseudo wonder
narrator and then maybe it's not that
good. I mean, there's always this
assumption that there is there is a lot.
And then there's the security where the
best victor attacks comes in.
This to look at the assumptions that that
we're not really sort
are deeply but.
But this is I don't see it as a
as a limitation. It's a challenge.
Yes.
And then randomness is really paramount
in cryptography.
And I would say to them, the main,
the main thing.
OK, next question again, from the
internet,
there is another follow up question
regarding protocol proofs, is
there any particular reason to
do protocol proofs in Acta rather
than Cocu?
Yes.
So this this this is a good question.
And when we started this project, we were
we knew about the professor
system, but
we're not really experts in it.
And but mainly the
the the two main reasons why we switched
to a two track, the
more light into switch.
OK, so we switched to Wagner
because we like the way the
dependently deprogramming programing is
better integrated.
But then there is why?
Why not reuse what has already been done
in court, like with the
Russian team?
They did this safety kit project
and then this easy crypt project.
So in short, there is there's two things
in in subject him that we didn't
like is that they try
to speak about probabilities.
They have to speak. I mean, we sort of
have to speak about real numbers and
real numbers in this kind of conflict of
logic. It's it's a mess.
And so you end up with ex-roommate,
an axiomatic version of the traumatic
version of your numbers.
And this we didn't like.
So we said we don't get
any need to heal numbers because in
in cryptography, the kind of
probabilities we do, they are only
discreet so, so
screwed at. And let's not delve
into hell, no, we want something
with absolutely no accident.
This was the first reason. The second
reason is that usually these games, they
are represented as as
imperative programs and that
we don't like imperative programs in
particular because we know how difficult
it is to write proofs about it.
So we wanted something that would be more
functional and less dramatic.
So that's that was the main reasons for
for for starting over with,
with different foundations,
then what was in in in such a good?
Could you go to the microphone?
I sorry, if I got you right, said the
result of the compression should be
completely random.
So to have a perfect
encryption after that.
So but I would assume that
the result of compression can never be
completely random because there is no
perfect compression.
So you you
may have got close to it if you
put this compression scheme
into that
piece of data, but then you
you that's not random anymore.
And if you if you don't, where where
would you put the compression scheme?
Because that scheme can't, can't be
random data now.
So so I'm not exactly sure I
get. I get I think I get the idea of.
But I mean, this is this is a fundamental
issue like compression.
If we want to use compression is because
it makes some messages
smaller.
But we know it can't make them all
smaller and they can't compress
messages in the same way.
And some will be compressed well, some we
won't and some won't be compressed
at all. And we led the way with this
dictionary at the beginning that makes
things bigger. So if we go to the worst,
worst case, then you would have
to never. I mean, if you want to pad
the messages so that they all
end up with the same size, then you end
up not compressing at all.
So, yeah, so
I think that there there is the only
way is to sort of to to either
the the length of
off after by adding
some random amount off
of that. But even that is usually not
helping much because then
then it's just a bit more difficult to
see because we are not going to add one
one gigabyte of a fondness
just in case.
Then you can defeat the purpose of
compression again.
This is really the fundamental issue of
that. Combining this to this to
this two features
compression and encryption.
OK, last question.
Anyone?
OK, thank you so much.