ProVerif Based Task. Here is the pv file:

type FINMarker.

type ID$.$

type Nonce.

type Key.

table ltks$($ID$,$ Key$).$

free psk:Key $[$private$].$

free ch:channel.

free aMessage:bitstring $[$private$].$

fun KDF$($Key$,$ bitstring$)$:Key.

fun MAC$($Key$,$ bitstring$)$:bitstring.

fun enc$($Key$,$ bitstring$)$:bitstring.

reduc forall k:Key, b:bitstring; dec$($k$,$ enc$($k$,$ b$))=$ b$.$

free FIN:FINMarker.

event evIRunning$($Key$).$

event evRRunning$($Key$).$

event evIComplete$($Key$).$

event evRComplete$($Key$).$

event evReachI.

event evReachR.

$(*$ client $*)$

let Idummy$($ltk:Key, id:ID$)=0.$

let I$($ltk:Key, id:ID$)=$

new nI:Nonce;

out$($ch$,($id$,$ nI$))$;

in$($ch$,($nR:Nonce, mac:bitstring$))$;

if mac $=$ MAC$($ltk$,($nI$,$ nR$,$ id$))$ then

let k $=$ KDF$($ltk$,($nI$,$ nR$))$ in

event evIRunning$($k$)$;

out$($ch$,($MAC$($ltk$,($FIN$,$ nR$,$ nI$,$ id$))))$;

event evIComplete$($k$)$;

$(*$ Section $4$: Addition of transmission of an encrypted and MACed message.

$*$ Three parts are needed: this sending, the receiving code in R$,$

$*$ and the new properties attacker $($aMessage$)$ and that R received

$*$ the aMessage.

$*$ In all three places the relevant code is encapsulated in

$*$ BEGIN$/$END comments.

$*)$

$(*$ BEGIN $*)$

$(*$ Write your code here $*)$

$(*$ END $*)$

event evReachI.

$(*$ server $*)$

let R$()=$

new nR:Nonce;

in$($ch$,($id:ID$,$ nI:Nonce$))$;

get ltks$(=$id$,$ ltkPeer:Key$)$ in

let k $=$ KDF$($ltkPeer$,($nI$,$ nR$))$ in

event evRRunning$($k$)$;

out$($ch$,($nR$,$ MAC$($ltkPeer$,($nI$,$ nR$,$ id$))))$;

in$($ch$,$ mac:bitstring$)$;

if mac $=$ MAC$($ltkPeer$,($FIN$,$ nR$,$ nI$,$ id$))$ then

event evRComplete$($k$)$;

$(*$ Section $4$: Addition of transmission of an encrypted and MACed

$*$ message.

$*)$

$(*$ BEGIN $*)$

$(*$ Write your code here $*)$

$(*$ END $*)$

event evReachR.

$(*$ Sanity $*)$

query event$($evReachI$).$

query event$($evReachR$).$

$(*$ Session key secrecy $*)$

query secret k$.$

$(*$ Key Authentication

$*$ The idea is that I and R shold agree on the output key from the KDF

$*)$

query k:Key; event$($evIComplete$($k$))==>$ event$($evRRunning$($k$)).$

query k:Key; event$($evRComplete$($k$))==>$ event$($evIComplete$($k$)).$

$(*$ Section $4$: Addition of transmission of an encrypted and MACed message.

$*$ The "attacker query" is used to check secrecy of built up terms.

$*$ The "secret query" is used to check secrecy of bound names or variables.

$*)$

$(*$ BEGIN $*)$

$(*$ Write your queries here $*)$

$(*$ END $*)$

process

click on the verify button and examine the output in the text$-$box at the bottom. Pay special attention to the lines beginning with RESULT. These show whether the queries verified or not. Note the two queries event$($evReachI$)$ and event$($evReachR$)$ that evaluate to $$not false$,$ i$.$e$.,$true$.$ Find where in the model they are emitted.

Q$1$: What can we conclude from that these two queries evaluate to true? Consult the manual to understand queries of this form if necessary

Go to the end of the model and look at the process definition. In the process definition, replace the sub$-$process I with Idummy. The result is that we use an I$-$process that does nothing. Press the verify button once more and examine output. The following will appear in the output:

RESULT event$($evIComplete$($k$\_$xy$))==>$ event$($evRRunning$($k$\_$xy$))$ is true.

Q$2$: Explain how this query can still evaluate to true even though the Idummy$-$process does nothing. Use the ProVerif manual if needed. HINT: consider at which point the evICommplete event is emitted in traces from this updated model.

This shows the importance of always ensuring reaching the points in the model that are important for your properties. Now switch the process definition of the I$-$process back to I in the process at the bottom of the file. Recall that $!$P means infinite replication of the process P$.$ The process is defined as:

$!($new ltk:Key; new id:ID; insert ltks$($id$,$ ltk$)$; $!$I$($ltk$,$ id$))|!($R$)$

This runs two sub$-$process in parallel, separated by the pipe$-$operator $(|).$ The first process creates a key and a client identifier, inserts these into a long$-$term key$-$store and finally executes an infinite number of I$-$processes using this key. Because the just described process is replicated an infinite number of times, it models an infinite number of initiators executing an infinite number of I$-$processes each. The second process runs an infinite number of R$-$processes. Suppose the process was instead defined as follows:

$!($new ltk:Key; new id:ID; insert ltks$($id$,$ ltk$)$; I$($ltk$,$ id$))|!($R$)$

Q$3$: What is the syntactical difference between the two definitions? If you were to model a protocol for MIT students logging in to Canvas and I models the student and R the server, which of the two process definitions would you use? Motivate your answer and consider limitations of the definitions.

$-$Key Authentication

The model tries to capture key authentication by verifying that I and R both derive the same session key k$.$ This is reflected by the $2$ queries:

query k:Key; event$($evIComplete$($k$))==>$ event$($evRRunning$($k$)).$

query k:Key; event$($evRComplete$($k$))==>$event$($evIComplete$($k$)).$

Q$4.$ why does the $2$nd query evaluate to false?$($Hint: it has to do with the fact that queries must hold for all traces and that events are scheduled in the trace like any other action, such as ex$.$ in$,$ out or get$)$

Q$5.$ correct the $2$nd query using a more appropriate event and verify that it now evaluates to true. explain why your change works better