Types for protocols

Types for secrecy

Cryptyc

Types for authenticity

What is a type system? Why?

What do the types for the lambda-calculus look like?

What might types for the pi-calculus look like?

What might types for the spi-calculus look like?

History:

Pi-calculus sorting (Milner)

Pi-calculus typing (Pierce and Sangiorgi, ...)

Spi-calculus types for secrecy (Abadi and Blanchet)

Spi-calculus types for authenticity (Gordon and Jeffrey)

Take the pi-calculus :

P,Q,R::=

0

outxy;P

inx(y);P

P|Q

!P

new (x);P

Add lists of messags as primitives:

P,Q,R::=

0

outMN;P

inM(y);P

P|Q

!P

new (x);P

splitLis (x,y);P

L,M,N::=

x

()

(M,N)

Allow bad states:

P,Q,R::=

...

FAIL

with dynamic semantics:

split (L) is (x,y);PFAIL (Lnot of the form (M,N))

outLN;PFAIL (Lnot of the formc)

inL(x);PFAIL (Lnot of the formc)

A process is *safe* if
there is no *Q* such that *P* ^{*} *Q* | FAIL.

Are the following safe?

out

*c**d*;**0**out

*c*();**0**out ()

*d*;**0**out () ();

**0**in

*c*(*x*); out*x*();**0**in

*c*(*x*); out*x*();**0**| out*c*(*d*);**0**in

*c*(*x*); out*x*();**0**| out*c*();**0**

Add types:

S,T,U::=

chan (T)

()

(T,U)

(Recall is a
lookup table of types for variables *x*:*T*.)

Rules for messages saying when
*M* : *T* is true:

If

*x*:*T*then*x*:*T*() : ()

If

*M*:*T*and*N*:*U*then (*M*,*N*) : (*T*,*U*)

What are the matching type rules for processes saying when
*P* : ok is true?

Can we find types for *c* and *d* which make the following ok?

out

*c**d*;**0**out

*c*();**0**out ()

*d*;**0**out () ();

**0**in

*c*(*x*); out*x*();**0**in

*c*(*x*); out*x*();**0**| out*c*(*d*);**0**in

*c*(*x*); out*x*();**0**| out*c*();**0**

Results:

Type safety: if

*P*: ok then FAIL*P*.Subject reduction: if

*P*: ok and*P**Q*then*Q*: ok

Plug these together and we get that well-typed processes are safe!

Example RPC call:

!inrpc(return,arg); ... outreturnresult;0

new (return); outrpc(return,arg); inreturn(result); ...

What types do we give *rpc*, *return* to get this to typecheck?

Assume *arg*:*Arg* and *result*:*Result*.

Add message tags:

P,Q,R::=

...

caseLis inl(x)Pis inr(y)Q

L,M,N::=

...

inl (M)

inr (M)

Dynamic semantics:

caseLis inl(x)Pis inr(y)QFAIL

(Lnot of the form inr(M) or inr(N))

Add types for message tags:

S,T,U::=

...

T+U

If

*M*:*T*then inl (*M*) :*T*+*U*If

*N*:*U*then inr (*N*) :*T*+*U*

What is the matching rule for case?

What types can we give to *c*, *d*, *e*, *x*, *y* and *z* here:

Example | outc(inl(fred)); outc(inr(wilma));0

where:

Example =

!inc(x);

casexis inl(y)

outd(y);0

is inr(z)

oute(z);0

(Assume *fred*:*Boy* and *wilma*:*Girl*.)

Types for spi are different from types for pi, because:

- We care about dishonest agents (not just honest agents).
- We care about
*robust*safety, not just safety. - Dishonest agents don't play by the type rules.

The type system for pi does *not* give us robust safety,
because of attackers who don't play by the type rules.

Example =

!inc(x);

casexis inl(y)

outd(y);0

is inr(z)

oute(z);0

This process is safe, but not robustly safe. (What is the attacker?)

Introduce a new untrusted type for the dishonest agents:

S,T,U::=

...

Un

satisfying *opponent typability*:

- If
*x*:Un for every*x**M*then*M*: Un. - If
*x*:Un for every*x**P*then*P*: ok

We switch off the type system when we hit type Un.

In particular, FAIL : ok, unsurprising, since attackers don't play ball with types!

Introduce a new trusted type of private secrets:

S,T,U::=

...

Private

In particular, we have:

net: Un,s: Private outnet(s);0: ok

We use crypto to keep secrets!

P,Q,R::=

...

decryptMis {x};_{N}P

L,M,N::=

...

{M}_{N}

Is this example robustly safe for secrecy of *s*?

Example_{1}= new (key); !Sender | !Receiver

Sender = outnet{s};_{key}0

Receiver = innet{x};_{key}0

We use crypto to keep secrets!

P,Q,R::=

...

decryptMis {x};_{N}P

L,M,N::=

...

{M}_{N}

Is this example robustly safe for secrecy of *s*?

Example_{2}= new (key); !Sender | !Receiver | !Oracle

Sender = outnet{s};_{key}0

Receiver = innet{x};_{key}0

Oracle = innet{x}; out_{key}net(x);0

Types for crypto:

S,T,U::=

...

Key (T)

Typing encryption:

If

*M*:*T*and*N*: Key (*T*) then {*M*}: Un._{N}

What is the matching rule for decrypt?

What types do we give for *s*, *x* and *key* here:

Example = new (key); !Sender | !Receiver | !Oracle

Sender = outnet{s};_{key}0

Receiver = innet{x};_{key}0

Why doens't this typecheck:

Oracle = innet{x}; out_{key}net(x);0

Result:

Ifnet: Un,s: PrivateP: ok

thenPis robustly safe for secrecy ofs.

Cryptyc (Gordon and Jeffrey) is a spi-calculus based protocol verification tool, based on type-checking.

To run cryptyc:

java -jar cryptyc.jarfilename

for example:

java -jar cryptyc.jar secrecy.cry

produces output:

Type checked OK!

but if you uncomment the oracle, you get:

Type error!

Cryptyc syntax is like the pi-calculus, but it uses a client-server model.

This is just syntax sugar:

serverSatAis (socket:Socket) {P}

clientCatBis { establishSatAis (socket:Socket);Q}

translates into pi as:

!inputS@A(socket:Socket);P|

new (socket:Socket); outputS@A(socket);Q

The action is in the types, for example:

type MyKey = Key (Private);

says a lot about this protocol!

Cryptyc also supports Struct and Union types.

Authenticity is declared using *correspondences*:

Abegins (Sender sentM)

(1)AB: {M}Kab

Bends (Sender sentM)

Recall, this protocol is *not* robustly safe. (Why not?)

Example is coded in Cryptpyc as fail-auth.cry.

Solution: nonce challenges!

We need to track the *effect* of a process: these are the ends without matching begins.

What are the effect of the following:

begin

*hello*; end*hello*;**0**begin

*hello*; end*world*;**0**end

*hello*; end*world*;**0**end

*hello*; begin*hello*;**0**

Calculating the effect for straight-line code is easy:

es,fs,gs::=

endL_{1}, ..., endL_{n}

If

*P*: [*es*] then end*L*;*P*: [*es*+ end*L*]If

*P*: [*es*] then begin*L*;*P*: [*es*- end*L*]**0**: [ ]

Which of these have empty effect?

begin

*hello*; end*hello*;**0**begin

*hello*; end*world*;**0**end

*hello*; end*world*;**0**end

*hello*; begin*hello*;**0**

Revisit fail-auth.cry.

Types for nonces (simplified: the real thing makes sure each nonce is only used once):

S,T,U::=

...

Nonce (es)

with:

If

*M*: Un and*N*: Nonce (*es*) and*P*: [*fs*]

then check*M*is*N*;*P*: [*fs*-*es*]

Still doesn't quite work: fail-simple2.cry.

Need to allow nonces to start at type Un, then later on be converted to Nonce type:

P,Q,R::=

...

castNis (x: Nonce (es));P

at run-time this is a no-op:

castNis (x: Nonce (es));PP[N/x]

but when we type-check, we make sure we can justify the effect!

If

*N*: Un and ,*x*:Nonce(*es*)*P*: [*fs*]

then cast*N*is (*x*:Nonce(*es*));*P*: [*fs*+*es*]

Hooray, now it works: simple.cry.

Result:

Ifnet: UnP: [ ]

thenPis robustly safe for authenticity.

Usual collection of examples is bundled with the Cryptyc tool...

Midterm.