CST 3160, Security – Resit/Defe
ed CW2
student name: student number:
Due date 10th August
1. Modelchecking is a technique that allows protocol verification, for example
with the tool Proverif.
Which three of the following statements are true? (1 point)
(a) A modelchecker, for example Proverif, runs all possible executions of the
model thereby it finds an attack if there is one in the system model.
(b) Modelcheckers are a very popular technique in industry because they are
“push button”.
(c) Modelchecking is equivalent to a mathematical proof that the query is
true in the model.
(d) If the modelchecker cannot find an attack it is very likely that there is
no attack in the model.
(e) A modelchecker, for example Proverif, tests certain runs of the model
and produces an output if there are bugs.
2. In this simple protocol A sends a message to B confidentially using crypto-
graphy. In Alice Bob notation this was expressed as follows:
A → B : {M}KB
B does : {{M}KB }K−1
B
= M
To implement this in Proverif, we first add cryptography for public keys.
type pkey. (* public keys *)
type skey. (* private (secret) keys *)
(* Asymmetric key encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
educ forall x: bitstring, y: skey; adec(aenc(x, pk(y)),y) = x.
Now, implement the actual protocol by filling in the gaps. (1 point)
1
free c : channel .
free s:bitstring [private].
query attacker(s).
let clientA(pkB: pkey) =
out(c, ...).
let clientB(pkB: pkey, skB:skey) =
in(c, x: bitstring);
let y = ... in
0.
process
new skB: skey;
let pkB = pk(skB) in out(c, pkB);
( (!clientA(pkB)) | (!clientB(pkB,skB)))
Answer the following questions: What is the meaning of the following result
of the query? (1 point)
RESULT not attacker(s[]) is true.
3. Consider the simple Access Control Matrix below. Use the table to specify
the security policy of the system based on
• capabilities (1 point)
• ACLs (1 point)
tax.doc fun.exe exam.pdf
Alice {read, write} {execute} -
Bob {read, execute } {read, write, execute } { write }
2
4. A common security policy is: “information may only flow up” which implies
“no read up/no write down”. On what level must a subject be such that
he/she can . . .
• write on two objects at level (public, {PER}) and (private, {ENG})? (1
point)
• read from two objects at level (private, {}) and (public, {ENG})? (1
point)
Give all possible levels that answer each question.
5. Generalizing the two examples given above, answer the following questions
using the meet u and join t operations (the meet aub is the greatest element
elow a and b; the join a t b is the least element above a and b):
• Given two objects o1, o2 at different security levels s1 and s2 what is
the maximal security level Lmax a subject u can have to be allowed to
write both objects? (1 point)
• Given two subjects u1, u2 at different security levels s1 and s2, what
is the maximal security level Lmax an object o can have so that both
subjects can still read from it? (1 point)
3
6. Attack Trees
learn
combo
…$
pick lock
130K $
find written
combo
75K $
get combo
from target
…$
listen to
conversation
20K $
get target to
state combo
30K $
open safe
…$
install
improperly
100K $
cut open
100K $
lackmail1
100K $
threaten
60K $
ibe
200K $
eavesdrop
…$
Fill in the dots into the internal nodes of the above attack tree and thereby
infer the minimal cost for the root attack “open safe” (1 point).
4