Name:

SE547 midterm exam: Practice exam

Answer all questions.

Time allowed: 2 hours

Total number of points: 100

Lambda Reference

Lambda calculus with booleans:

L, M, N ::=
    x
    M N
    x.M
    True
    False
    if ( L ) { M } else { N }
    FAIL

Alpha equivalence = generated by consistent renaming of bound variables.

Dynamic semantics generated by:

  1. ( x . M ) N ( [N/x]M )
  2. if ( True ) { M } else { N } M
  3. if ( False ) { M } else { N } N
  4. if ( x.M ) { M } else { N } FAIL
  5. True ( M ) FAIL
  6. False ( M ) FAIL
  7. If P = = Q then P Q.
  8. If L M then L N M N.
  9. If M N then L M L N.

A program M can fail if:

M * N and FAIL N

A program is fail-safe otherwise.

Lambda Reference

Types for lambda with booleans:

, ::=
    bool
   

Program typing M : generated by:

  1. If x : then x : .
  2. If , x : M : then x.M : .
  3. If M : , and N : , then M N : .
  4. True : bool
  5. False : bool
  6. If L : bool and M : and N : then if ( L ) { M } else { N } : .

Note: in these rules, we assume no variable name clashes.

Spi Reference

Syntax:

P, Q, R ::=
    0
    out M N; P
    in M (y); P
    P | Q
    !P
    new (x); P
    split L is (x, y); P
    case L is inl(x) P is inr(y) Q
    decrypt M is { x }N; P
    check M is N; P
    begin L; P
    end L; P
    FAIL

L, M, N ::=
    x
    ()
    (M,N)
    inl (M)
    inr (M)
    { M }N

Alpha equivalence = generated by consistent renaming of bound variables.

Structural equivalence generated by:

  1. If P = Q then P Q.
  2. P | Q Q | P.
  3. (P | Q) | R P | (Q | R).
  4. If x Q then (new (x); P) | Q new (x); (P | Q)

Spi Reference

Dynamic semantics generated by:

  1. (out x M; P) | (in x (z); Q) P | Q[M/z]
  2. split (M, N) is (x, y); P P[M/x,N/y]
  3. case inl(M) is inl(x) P is inr(y) Q P[M/x]
  4. case inr(N) is inl(x) P is inr(y) Q Q[N/y]
  5. decrypt { M }N is { x }N; P P[M/x]
  6. check N is N; P P
  7. If L is not of the form x then out L M; P FAIL
  8. If L is not of the form x then in L (y); P FAIL
  9. If L is not of the form (M, N) then split L is (x, y); P FAIL
  10. If L is not of the form inl(M) or inr(N) then case L is inl(x) P is inr(y) Q FAIL
  11. If P Q then P Q.
  12. If P Q then P | R Q | R.
  13. If P Q then new (x); P new (x); Q.

Garbage collection equivalence =gc generated by:

  1. If x P then new (x); P =gc P
  2. new (x); in x (y); P =gc 0
  3. new (x); !in x (y); P =gc 0
  4. new (x); out x M; P =gc 0
  5. new (x); !out x M; P =gc 0
  6. P | 0 =gc P

A protocol P can fail if:

P * Q | FAIL

A protocol is fail-safe otherwise.

A protocol is robustly fail-safe if:

for any O P | O is fail-safe

Spi Reference

A protocol P violates the secrecy of M if:

P * Q | out net M; 0

A protocol is safe for secrecy of M otherwise.

A protocol is robustly safe for secrecy of M if:

for any O where M O, P | O is safe for secrecy of M

Traces of processes generated by:

new (x); P --gen(x) P
begin (L); P --begin(L) P
end (L); P --end(L) P

A process P is safe for authenticity if:

for any trace of P, the number of end Ls is less than or equal to the number of begin Ls.

A process P is robustly safe for authenticity if:

for any O, P | O is safe for authenticity

Spi Reference

Types for secrecy in spi:

S, T, U ::=
    Chan (T)
    ()
    (T,U)
    T + U
    Un
    Private
    Key (T)

Equivalence on types:

Un = Chan (Un) = () = (Un, Un) = Un + Un = Key (Un)

Message typing M : T generated by:

  1. If x:T then x : T

  2. () : ()

  3. If M : T and N : U then (M,N) : (T,U)

  4. If M : T then inl (M) : T+U

  5. If N : U then inr (N) : T+U

  6. If M : T and N : Key (T) then { M }N : Un.

Process typing P : ok generated by:

  1. 0 : ok

  2. If M : Chan (T) and N : T and P : ok then out M N; P : ok

  3. If M : Chan (T) and , y:T P : ok then in M (y); P : ok

  4. If P : ok and , y:T Q : ok then P | Q : ok

  5. If P : ok then !P : ok

  6. If , x : T P : ok and T is either Un, Private, Chan(U) or Key(U) then new (x); P : ok

  7. If M : (T, U) and , x:T, y:U P : ok then split M is (x, y); P : ok

  8. If M : T + U and , x:T P : ok and , y:U Q : ok then case M is inl (x) P is inr (y) Q : ok

  9. If M : Un and N : Key (T) and , x:T P : ok then decrypt M is { x }N; P : ok

Since we are only typechecking secrecy, we give simple rules for the following:

  1. If M : T and N : U and P : ok then check M is Nl; P : ok

  2. If L : T and P : ok then begin L; P : ok

  3. If L : T and P : ok then end L; P : ok

Note: in these rules, we assume no variable name clashes.

Question 1 (10 points)

Give a one- or two-sentence definition of:

a) Symmetric key cryptography.

b) Asymmetric key cryptography.

c) Cryptographic algorithm.

d) Cryptographic protocol.

e) Safety property.

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

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.

b) For each program, either give types for a, b, x, y, or give an explaination as to why no such types can be found.

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.

b) Fix this protocol, and give an informal justification for why the result is robustly safe for authenticity.

c) Translate your protocol into the spi-calculus (you may assume a function key(x) which returns the key Kxs shared between x and S).

d) Give types for your spi-calculus process, showing that it is robustly safe for secrecy of M.

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.

b) Give a one- or two-sentence explaination for your definition.

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.

Worksheet

You can use this sheet as scrap paper.

Worksheet

You can use this sheet as scrap paper.

Worksheet

You can use this sheet as scrap paper.

Worksheet

You can use this sheet as scrap paper.