PRACTICE MIDTERM SAMPLE SOLUTION
Note that for many of the questions, there's more than one right answer,
this is just one solution!
Question 1 (10 points)
Give a one- or two-sentence definition of:
a) Symmetric key cryptography.
ANSWER:
A cryptographic algorithm, with encryption:
Input: plaintext + encryption key
Output: ciphertext
and decryption:
Input: ciphertext + decryption key
Output: plaintext
such that decryption only succeeds if the encryption key and
decryption key are the same key.
b) Asymmetric key cryptography.
ANSWER:
As for symmetric key cryptography, except that the encryption key and
decryption key do not have to be equal, they have to be inverses of
each other. When an asymmetric key pair is generated, an encryption
key and it's inverse decryption key are generated.
c) Cryptographic algorithm.
ANSWER:
See above. The algorithm should satisfy:
- confidentiality: without the appropriate decryption key, the
plaintext cannot be determined from the ciphertext.
- integrity: without the appropriate decryption and encryption keys,
any modifications to the ciphertext will cause the decrypt to fail.
d) Cryptographic protocol.
ANSWER:
A cryptographic protocol uses cryptography and an underlying network
layer to achieve security properties without trusting the network.
Example security properties are:
- secrecy: some data (e.g. credit card numbers or passwords) must be
kept secret from anyone other than the principles authorized to know
them.
- authenticity: if A believes that B sent message M, then at some
point in the past, B did send message M. (This can be strengthened
to include freshness: B sent message M in the recent past.)
e) Safety property.
ANSWER:
A program never reaches a "bad" state at run-time. The notion of bad
state depends on the particular safety property, for example secrecy
is a safety property since a bad state is one where an unauthorized
principal has access to the secret.
Question 2 (10 points)
Consider the following coding of message tags in the lambda calculus:
inl = ( \x . \f . \g . f x )
inr = ( \x . \f . \g . g x )
case L is inl(x) M is inr(y) N = ( L ( \x . M ) ( \y . N ) )
Show that:
case inl (L) is inl(x) M is inr(y) N ->* M [L/x]
case True is inl(x) M is inr(y) N ->* FAIL
ANSWER:
case inl (L) is inl(x) M is inr(y) N
= ( ( \x . \f . \g . f x ) L ( \x . M ) ( \y . N ) )
-> ( ( \f . \g . f L ) ( \x . M ) ( \y . N ) )
-> ( ( \g . ( \x . M ) L ) ( \y . N ) )
-> ( ( \x . M ) L )
-> ( M [L/x] )
case True is inl(x) M is inr(y) N
= ( True ( \x . M ) ( \y . N ) )
-> FAIL
Question 3 (20 points)
Consider the following programs:
1. ( \x . \y . x y ) True False
2. ( \x . \y . x y ) ( \a . True ) False
3. ( \x . \y . x y ) True ( \b . False )
4. ( \x . \y . x y ) ( \a . True )( \b . False )
a) Give the dynamic semantics of each program.
ANSWER:
1. ( \x . \y . x y ) True False
--> ( \y . True y ) False
--> True False
--> FAIL
2. ( \x . \y . x y ) ( \a . True ) False
--> ( \y . ( \a . True ) y ) False
--> ( \a . True ) False
--> True
3. ( \x . \y . x y ) True ( \b . False )
--> ( \y . True y ) ( \b . False )
--> True ( \b . False )
--> FAIL
4. ( \x . \y . x y ) ( \a . True )( \b . False )
--> ( \y . ( \a . True ) y ) ( \b . False )
--> ( \a . True ) ( \b . False )
--> True
b) For each program, either give types for a, b, x, y, and the whole
program, or give an explaination as to why no such types can be found.
ANSWER:
1. No typing: x must have type bool (because \x... is applied to True
and function type, sincce x is applied to y. Contradiction!
2. x : bool -> bool, y : bool. a : bool
3. No typing (same reason as 1)
4. x : (T -> bool) -> bool, y : T -> bool, a : T -> bool, b : T
for any type T.
Question 4 (40 points)
Consider the following protocol (a broken version of Abadi and
Needham's simplification of the Otway-Rees protocol):
(1) A -> B : A, B, Na
(2) B -> S : A, B, Na, Nb
S begins initKey (A, B, Kab)
S begins respKey (A, B, Kab)
(3) S -> B : { Kab, Na }Kas, { Kab, Nb }Kbs
(4) B -> A : { Kab, Na }Kas
A ends initKey (A, B, Kab)
B ends respKey (A, B, Kab)
(5) A -> B : { M }Kab
a) Show that this protocol is not robustly safe for authenticity.
ANSWER:
Lots of attacks, one is:
(1) A -> I : A, B, Na
(2) I -> S : A, I, Na, Ni
S begins initKey (A, I, Kai)
S begins respKey (A, I, Kai)
(3) S -> I : { Kai, Na }Kas, { Kai, Ni }Kis
(4) I -> A : { Kai, Na }Kas
A ends initKey (A, B, Kai)
(5) A -> I : { M }Kai
At this point, A believes Kai is shared with B, when in fact it
is shared with I.
b) Fix this protocol, and give an informal justification for why the
result is robustly safe for authenticity.
ANSWER:
(1) A -> B : A, B, Na
(2) B -> S : A, B, Na, Nb
S begins initKey (A, B, Kab)
S begins respKey (A, B, Kab)
(3) S -> B : { inl(B, Kab, Na) }Kas, { inr(A, Kab, Nb) }Kbs
(4) B -> A : { inl(B, Kab, Na) }Kas
A ends initKey (A, B, Kab)
B ends respKey (A, B, Kab)
(5) A -> B : { M }Kab
Fixes: include A and B's names in ciphertexts (avoids above attacks).
Message tags (avoids type confusion attacks).
c) Translate your protocol into the spi-calculus.
initA =
new (nA); new (m);
out net (A, B, nA);
in net { inl(B, kAB, rA) }kAS;
check nA is rA;
end initKey (A, B, kAB);
out net { m }kAB;
0
respB =
in net (a, B, nA);
new (nB);
out net (a, B, nA, nB);
in net (ticket, { inr(a, kAB, rB) }kBS);
check nB is rB;
out net ticket;
end respKey (a, B, kAB);
in net { m }kAB;
0
ttpS =
in net (a, b, nA, nB);
new (kAB);
begin initKey (a, b, kAB);
begin respKey (a, b, kAB);
out net ({ inl(b, kAB, nA) }key(a), { inr(a, kAB, nB) }key(b));
0
d) Give types for your spi-calculus process, showing that it is
robustly safe for secrecy of M.
ANSWER:
net, A, B, a, b, nA, nB, rA, rB : Un
m : Secret
kAB : Key(Secret)
kAS, kBS : (Un, Key(Secret), Un) + (Un, Key(Secret), Un)
Question 5 (20 points)
The spi-calculus has types for authenticity as well as secrecy.
a) Give a definition of the additional types used to show authenticity.
ANSWER:
S, T, U ::=
... as above ...
Nonce (es)
es, fs, gs ::=
end L_1, ..., end L_n
b) Give a one- or two-sentence explaination for your definition.
ANSWER:
The new type is for a response to a nonce challenge, where the nonce
is allowing the recipient to end sessions named L_1 ... L_n.
c) Give types for Kas and Kbs as used in your answer to 3(d) which
shows robust safety for authenticity as well as secrecy. Note: you do
not have to copy the whole protocol out again, just give the types for
Kas and Kbs. You may use Cryptyc notation if you like.
ANSWER:
net, A, B, a, b, nA, nB : Un
rA : NA(A, B, kAB)
rB : NB(a, B, kAB)
m : Secret
kAB : Key(Secret)
kAS : K(A)
kBS : K(B)
where:
type NA(a, b, kAB) = Nonce (end (initKey (a, b, kAB)));
type NB(a, b, kAB) = Nonce (end (respKey (a, b, kAB)));
type K(a) = (b:Un, kAB:Key(Secret), rA:NA(a, b, kAB))
+ (b:Un, kBA:Key(Secret), rA:NB(b, a, kBA));