Cryptographic protocols

Spi calculus

Proverif

Secrecy

Authenticity

The pi-calculus contains enough features (processes, communication) to model communications protocols.

What features need to be added to model cryptographic protocols?

What properties could we check of these cryptographic protocols?

History:

Pi-calculus (Milner)

+ Dolev-Yao model of cryptographic protocols

= Spi-calculus (Abadi and Gordon).

Other models (all late 1990s-early 2000s):

Strand Spaces (Guttman).

Communicating Sequential Processes for crypto (Roscoe, Lowe, Schneider...)

Multiset Rewriting (Scedrov, Cervesato, Mitchell...)

...

Take the pi-calculus:

P,Q,R::=

0

outxy;P

inx(y);P

P|Q

!P

new (x);P

Add messages as primitives:

P,Q,R::=

0

outMN;P

inM(y);P

P|Q

!P

new (x);P

... other stuff will go here ...

L,M,N::=

x

... other stuff will go here ...

Add lists as primitives:

P,Q,R::=

...

splitLis (x,y);P

L,M,N::=

...

()

(M,N)

Example program:

!inc(x);

splitxis (head,tail);

outd(head); outc(tail);0

Dynamic semantics of lists:

split (M,N) is (x,y);PP[M/x,N/y]

What is the dynamic semantics of:

Example | outc(fred, (wilma, ()));0

where:

Example =

!inc(x);

splitxis (head,tail);

outd(head); outc(tail);0

Add message tags as primitives (just 2 tags are good enough):

P,Q,R::=

...

caseLis inl(x)Pis inr(y)Q

L,M,N::=

...

inl (M)

inr (M)

Example program:

!inc(x);

casexis inl(y)

outd(y);0

is inr(z)

oute(z);0

Dynamic semantics of message tags:

case inl(M) is inl(x)Pis inr(y)QP[M/x]

case inr(N) is inl(x)Pis inr(y)QQ[N/y]

What is the dynamic semantics of:

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

where:

Example =

!inc(x);

casexis inl(y)

outd(y);0

is inr(z)

oute(z);0

Add symmetric-key cryptography:

P,Q,R::=

...

decryptMis {x};_{N}P

L,M,N::=

...

{M}_{N}

Example program:

!inc(x);

decryptxis {y};_{key}

outd(y);0

Dynamic semantics of crypto:

decrypt {M}is {_{N}x};_{N}PP[M/x]

What is the dynamic semantics of:

Example | outc{msg};_{key}0

where:

Example =

!inc(x);

decryptxis {y};_{key}

outd(y);0

Add nonces:

P,Q,R::=

...

checkMisN;P

Example program:

!inc(x);

checkxisnonce;

outd(x);0

Dynamic semantics of nonces:

checkNisN;PP

What is the dynamic semantics of:

Example | outc(nonce); outc(other);0

where:

Example =

!inc(x);

checkxisnonce;

outd(x);0

Derived forms:

- Pattern matching.
- Lists of any length (not just zero or two).
- Any number of tags (not just two).

Example:

new (nonce);

outnet(nonce);

innet{msg,nonce'};_{key}

checknonceisnonce';0

Andrew Secure RPC:

(1)AB:A, { msg1(Na) }Kab

(2)BA: { msg2(Na,Nb) }Kab

(3)AB: { msg3(Nb) }Kab

(4)BA: { msg4(SK,SN) }Kab

What does this look like in spi?

Proverif (Blanchet) is a spi-calculus based protocol verification tool.

(It's written in O'Caml, so you need to get ocaml from www.ocaml.org if you want to recompile proverif.)

To run proverif:

analyzer -in pifilename

for example:

analyzer -in pi pi-simple-secr

produces output:

RESULT goal unreachable: attacker:s[]

Proverif is trying to find an attack, so this is good news for the protocol!

Proverif syntax is like the spi-calculus, but includes constant declarations, for example:

fun hostA/0.

private fun kAS/0.

fun hostB/0.

private fun kBS/0.

fun hostI/0.

fun kIS/0.

and function declarations, for example:

private reduc

key(hostA) = kAS;

key(hostB) = kBS;

key(hostI) = kIS.

The syntax is also slightly different, for example:

new s; out(net, sencrypt(s,kAB)); 0.

in(net, m1); let s = sdecrypt(m1, kAB) in 0.

rather than:

new (s); outnet{s};_{kAB}0

innet(m1); decryptm1is {s};_{kAB}0

Some examples of secrecy:

Some examples of failed secrecy:

A protocol *P* violates the secrecy of *M* if:

P^{*}Q| outnetM;0

A protocol is *safe* for secrecy of *M* otherwise.

A protocol is *robustly safe* for secrecy of *M* if:

for anyOwhereMO,P|Ois safe for secrecy ofM

Examples:

out

*net**M*;**0**new (

*kAB*); out*net*{*M*};_{kAB}**0**new (

*kAB*); out*net*{*M*}; out_{kAB}*net**kAB*;**0**

Which ones are safe for secrecy of *M*?

Which ones are robustly safe for secrecy of *M*?

In proverif:

query s.

checks if the protocol is robustly safe for secrecy of s.

RESULT goal unreachable: attacker:s[]

*the protocol robustly preserves secrecy*pi-simple-secr.RESULT goal reachable: attacker:s[]

*there is an attacker which violates secrecy*pi-stupid-secr.... or the tool may run forever ... pi-flawed-secr.

We want to verify:

AgeneratesMforB

(1)AB: {M}Kab

BbelievesAgeneratedMforB

we need to turn this into a formal statement!

One formulation of authenticity is as *correspondences*. Add session markers:

Abegins generated (A,B,M)

(1)AB: {M}Kab

Bends generated (A,B,M)

Now check correspondence:

For any session markerL, the number of endLs is less than or equal to the number of beginLs.

In the presence of an attacker, does the above protocol satisfy correspondence?

Extending spi for authenticity:

P,Q,R::=

...

beginL;P

endL;P

Example processes:

Sender =

new (m);

begin generated (A,B,m);

outc{m};_{key}0

Receiver =

!inc(x);

decryptxis {y};_{key}

end generated (A,B,m);0

Record a *trace* of a process, generated by:

new (x);P-gen(x)->P

begin (L);P-begin(L)->P

end (L);P-end(L)->P

For example, what are the traces of Sender | Receiver:

Sender =

new (m);

begin generated (A,B,m);

outc{m};_{key}0

Receiver =

!inc(x);

decryptxis {y};_{key}

end generated (A,B,m);0

A process *P* is *safe* for authenticity if:

for any trace ofP, the number of endLs is less than or equal to the number of beginLs.

A process *P* is *robustly safe* for authenticity if:

for anyO,P|Ois safe for authenticity

Is Sender | Receiver safe? Robustly safe?

Sender =

new (m);

begin generated (A,B,m);

outc{m};_{key}0

Receiver =

!inc(x);

decryptxis {y};_{key}

end generated (A,B,m);0

In proverif:

authquery generated/3.

checks if the protocol is robustly safe for authenticity (for session marker `generated').

For example, pi-simple-auth.

Proverif also supports *many-to-one* correspondences, which check
the weaker property:

For any session markerL, any endLs is preceded by a beginLs.

Note that begin *L*; end *L*; end *L*; **0**
satisfies this weaker property.

Other failed examples of authenticity:

These can be fixed, for example:

Homework sheet 4.

Types for cryptographic protocols.