Answer all questions.
Time allowed: 2 hours
Total number of points: 100
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:
A program M can fail if:
M ^{*} N and FAIL N
A program is fail-safe otherwise.
Types for lambda with booleans:
, ::=
bool
Program typing M : generated by:
Note: in these rules, we assume no variable name clashes.
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:
Dynamic semantics generated by:
Garbage collection equivalence =_{gc} generated by:
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
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
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:
If x:T then x : T
() : ()
If M : T and N : U then (M,N) : (T,U)
If M : T then inl (M) : T+U
If N : U then inr (N) : T+U
If M : T and N : Key (T) then { M }_{N} : Un.
Process typing P : ok generated by:
0 : ok
If M : Chan (T) and N : T and P : ok then out M N; P : ok
If M : Chan (T) and , y:T P : ok then in M (y); P : ok
If P : ok and , y:T Q : ok then P | Q : ok
If P : ok then !P : ok
If , x : T P : ok and T is either Un, Private, Chan(U) or Key(U) then new (x); P : ok
If M : (T, U) and , x:T, y:U P : ok then split M is (x, y); P : ok
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
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:
If M : T and N : U and P : ok then check M is Nl; P : ok
If L : T and P : ok then begin L; P : ok
If L : T and P : ok then end L; P : ok
Note: in these rules, we assume no variable name clashes.
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.
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
Consider the following programs:
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.
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.
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.
You can use this sheet as scrap paper.
You can use this sheet as scrap paper.
You can use this sheet as scrap paper.
You can use this sheet as scrap paper.