Notes

documentclass[a4paper]{article}
usepackage[english]{babel}
usepackage[utf8x]{inputenc}
usepackage[T1]{fontenc}
usepackage[a4paper,top=3cm,bottom=2cm,left=3cm,right=3cm,marginparwidth=1.75cm]{geometry}
usepackage{amsmath}
usepackage{graphicx}
usepackage[colorinlistoftodos]{todonotes}
usepackage[colorlinks=true, allcolors=blue]{hyperref}
usepackage{soul}
usepackage{float}
usepackage{color,soul}
definecolor{grey}{rgb}{.8,.8,.8}
sethlcolor{grey}

title{
Empty subject\
Large Lab Session}
author{SABOUNI Med Amine}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
begin{document}
maketitle

section*{Exercise 1:}
1)\
> Result of the Avispa test\
OFMC : SAFE becuse of bounded number of sessions\
ATSE : SAFE because bounded number of sessions and typed model\

2)\
> The protocol happens as follow :\
Alice send nounce1 with her idenditiy to Bob using Kb\
Bob decrypt nounce1 and generates nounce2 that he sends using Ka\
Alice decrypts both nounces and send nounce2 to Bob using Kb to prove knowledge\
> The attacks happens as follow :\
Alice initiate a session with the intruder, trusting him, using his key.\
Intruder can get nounce 1 and cipher it to Bob impersonating Alice\
Bob send a second nounce to Alice using her public key.\
Intruder cannot read the answer with Alice's key but forward the message to Alice who responds thinking it's Intruder's nounce and send the nounce 2 to the intruder.\
> Remarks\
Bob thinks that Intruder is Alice while Intruder conduct a honnest session with Alice\
Intruder's objective is to get Bob's nounce.\\
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO11.jpg}
caption{}
end{figure}

3) \
> The protocol is the same that the previous question\
> The attack is almost the same as the previous one, the only difference being that :\
In question2 the objective is only to get knowledge of nounce2\
In question3 is to impersonate Alice using the actual nounce2\
> The result is that Intruder impersonate Alice, and Bob thinks is talking to Alice. Intruder uses a honnest session with Alice to get the messages ciphered to Alice in the 1st place\
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO12.jpg}
caption{}
end{figure}

4)\
The solution might signing instead of (or used after) ciphering.\
> The fist solution is to sign all the message before ciphering them to the recipient, that way all messages are authenticated.\\
> The second solution, is simply to add at each message the identities of Alice and Bob for instance, send(Na,Nb,A,B) instead of just (Na,Nb): \
hl{
%A -> B: {Na,A}_Kb\
%B -> A: {Na,Nb,A,B}_Ka\
%A -> B: {Nb}_Kb\\
Alice\
0. State = 0 / RCV(start) => \
State':= 2 / Na' := new() / SND({Na'.A}_Kb)\
/ secret(Na',na,{A,B}) \
/ witness(A,B,bob_alice_na,Na')\\
2. State = 2 / RCV({Na.Nb'.A.B}_Ka) => \
State':= 4 / SND({Nb'.A.B}_Kb) \
/ request(A,B,alice_bob_nb,Nb')\\
Bob\
. State = 1 / RCV({Na'.A}_Kb) => \
State':= 3 / Nb' := new() / SND({Na'.Nb'.A.B}_Ka)\
/ secret(Nb',nb,{A,B}) \
/ witness(B,A,alice_bob_nb,Nb')\\
3. State = 3 / RCV({Nb.A.B}_Kb) =>
State':= 5 / request(B,A,bob_alice_na,Na)
}
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO13.jpg}
caption{}
end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
section*{Exercise 2:}
1)\
> The goal is to check the secrecy of the generated key.\
Alice provides a nounce Na and Bob provides a nounce Nb and the key is the concatenation.\
If an intruder gets both of Nounce then the key is compromised.\
> Intruder initiate session with Bob to get nounces, intercept a nounce generated by Alice for Bob and send the same nounce to Bob to get the nounce concatenated with another one.\
Intruder can use the first nonce with Alice with a different second nounce.\
Alice use the two nounces to encrypt the message (0,nounce3)\
Intruder has knowledge of two nounces and can decrypt nounce3\
> The result is that Intruder can impersonate someone and get nounces
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO21.jpg}
caption{}
end{figure}

2)\
> The solution proposed by the second iteration of the protocol is to not exchange nounces\
Once we receive a nounce we store but don't send it back, and since the nounces are ciphered, intruder can't guess them.\
The two parties then concatenate the nounces they received and sent and directly generate and use the session key.\
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO22.jpg}
caption{}
end{figure}

3)\
> This solution if it hides the nounces that are being exchanged, doesn't protect againt impersonation.\
Intruder can impersonate Alice, intercept messages and replay them to Alice which give Intruder a nounce.\
The identity is not ciphered with the nounce, so the intruder can change them easily.\

4)\
> The solution is to authenticate the nounces and cipher the identity as well.\
To do that, put the identity concatenated inside the cipher part and it's SAFE.\
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO23.jpg}
caption{}
end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
section*{Exercise 3:}
1)\
> The protocol\
Alice sends no nounce at first but send a message authenticated by her identity\
Bob extract the message and xor it ith his own idendity and append it to a new nounce.\
Bob sends the xor result with the noun, Alice knowing Bob and the message can extract the nounce\

2)\
The secrecy is not safe anymore and an attack is not found (but an intrusion is)\

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
section*{Exercise 4:}
1)\
> The protocol\
Alice and Bob share a secret key that they use to exchange messages. Alice first sends a nounce that Bob hashes and send the hash along a second nounce. Alice hashes the second nounce and sends the hash to Bob. Bob generates a session key that he sends to Alice along with a next nounce.\
The protocol allows for two session between Alice and Bob, and doesn't have a protection against impersonnation : an intruder can catch messages for Bob and impersonate Alice and catch message for Alice and impersonate Bob. But the key used is secret and preshared, the intruder cannot actually read the message. The protocol is safe but impersonation is possible (but useless).\
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO41.jpg}
caption{}
end{figure}

2)\
We change the weak authentication property of Alice-Bob-Kpab to strong one, and rerun the simulation and we find that the protocol is still safe but allow impersonation. We can explain this by the fact that a preshared secret key guarantee the confidentiality of the message, but not the authentication.\

3)\ We add 2 new steps verify the nounce :
%hl{5. A --> B : {Nap}_vert Kpabvert \
%6. B --> A : {Succ(Nap)}_vert Kpabvert}\
Verify the strong authentication property of responder to initiator on Kpab, for the new obtained protocol. Explain the results you get.
begin{figure}[H]
centering
includegraphics[width=0.65linewidth]{EXO22.jpg}
caption{}
end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
section*{Exercise 5:}
Translate in HLPSL the Diffie-Helman protocol, where Na, Nb and Secret are nonces of
type text and G is also of type text, but public.
%1. A --> B : G^|Na|, {N}_|Kb|
%2. B --> A : G^|Nb|, {N}_|Ka|
%3. A --> B : {Secret}_|(G^Na)^Nb|
1. Simulate your protocol.
2. Specify the secret property of the variable Secret.
3. Check this property.
4. Simulate the Man-in-the-middle attack.
5. Try to correct the protocol in order to get secrecy of Secret, and verify your corrected
version.

end{document}