The pdf has 6 questions, mainly is fill in the blanks, multiple choice questions and so on.. Its mainly related to Security Protocol verification/ security related. To someone who knows it can do it in 20minutes.
CST 3160, Security – Resit/Deferred 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. reduc 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 below 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 $ blackmail1 100K $ threaten 60K $ bribe 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