### PPTX - [email protected]/* <![CDATA[ */!function(t,e,r,n,c,a,p){try{t=document.currentScript||function(){for(t=document.getElementsByTagName('script'),e=t.length;e--;)if(t[e].getAttribute('data-cfhash'))return t[e]}();if(t&&(c=t.previousSibling)){p=t.parentNode;if(a=c.getAttribute('data-cfemail')){for(e='',r='0x'+a.substr(0,2)|0,n=2;a.length-n;n+=2)e+='%'+('0'+('0x'+a.substr(n,2)^r).toString(16)).slice(-2);p.replaceChild(document.createTextNode(decodeURIComponent(e)),c)}p.removeChild(t)}}catch(u){}}()/* ]]> */

```Chen Chen

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Demo

Comparison

Conclusion

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion
Original
Protocol
Pi Calculus
Horn Clauses
Authenticity
Reserved?
Proverif

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion

Extension of pi calculus with:
◦ cryptographic primitives
◦ “begin” & “end” events

Pi calculus:
◦ mathematical formalisms for describing and
analyzing properties of concurrent computation

Name:

Variable:
◦ Free name: Names globally known (also to adversary)
◦ Bound name: Names local to the process
◦ Free variable: Variables not used anywhere
◦ Bound name: variables used in the process


Equivalence:
Reduction:
Original
Protocol
Pi Calculus
Process P
Horn Clauses
Proverif

A simplified version of Woo and Lam one-way
public key authentication protocol




Create secret key skA & skB
Create corresponding public keys
Distribute public keys
Create unbounded number of sessions

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion

◦ Closed process: Process without free variables
(allow free names)

Secrecy

Authenticity
◦ Non-injective agreement:
 if event end(M) is executed, then begin(M) has also
been executed.

Authenticity
◦ Injective agreement:
 The number of executions of end(M) is smaller than
that of begin(M).

Authenticity
◦ Non-injective agreement:
 if event end(M) is executed, then begin(M) has also
been executed.

Authenticity is satisfied when:
◦ B cannot emit his end event without A having
emitted her begin event.

End(M) => Begin(M) for all cases.
Sarkozy says:
Sarkozy thinks:
Sarkozy agrees:
Authenticity is satisfied when: The other side is indeed Sarkozy!
End(M):
I finish my part of the
protocol.
I think I have talked to
Sarkozy
Begin(M):
I start my part of
the protocol.
I think I would
talk to Obama
Protocol ensures:
Remember: Protocol is lock-stepped!
End(M):
I finish my part of the
protocol.
I think I has talked to
Sarkozy
Begin(M):
I start my part of
the protocol.
I think I would
talk to Obama
Authenticity is violated when End(M) => Begin(M)!

Authenticity is satisfied when:
◦ B cannot emit his end event without A having
emitted her begin event.

End(M) => Begin(M) for all cases.
End(M):
I finish my part of the
protocol.
I think I has talked to
Sarkozy
Here End(M) !=> Begin(M)!
Begin(M):
I start my part of
the protocol.
I think I would
talk to Obama

Authenticity
◦ Non-injective agreement:
 if event end(M) is executed, then begin(M) has also
been executed.
We will be back!

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion

(P1 Λ P2 Λ…Λ Pn) => u

Our usage:
◦ Patterns
◦ Facts
◦ Rules
 Attacker
 Protocol

(P1 Λ P2 Λ…Λ Pn) => u

Our usage:
◦ Patterns
◦ Facts
◦ Rules
 Attacker
 Protocol

(P1 Λ P2 Λ…Λ Pn) => u

Our usage:
◦ Patterns
◦ Facts
◦ Rules
 Attacker
 Protocol

(P1 Λ P2 Λ…Λ Pn) => u

Our usage:
◦ Patterns
◦ Facts
◦ Rules
 Attacker
 Protocol

(P1 Λ P2 Λ…Λ Pn) => u

Our usage:
◦ Patterns
◦ Facts
◦ Rules
 Attacker
 Protocol
Original
Protocol
Pi Calculus
Horn Clauses
Proverif

If c ∈ S, message(c[],M) = attacker(M)

Vo, Vs:
◦ Vo: Set of ordinary variables.
◦ Vs: Set of session identifiers.


ρ : mapping from variables and names to patterns
h : Sequence of facts of message and begin.
◦ Literals of horn clauses we want





[|P|] = [|(vskA).P1|]
[|P1|] = [|(vskB).P2|]
[|P2|] = [|let pkA = pk(skA) in P3|]
[|P3|] = [|let pkB = pk(skB) in P4|]
[|P4|] = [|c<pkA>.P5|]

ρ : c → c[] ,skA → skA[] , skB →
skB[]
h:

First Horn Clause: message(c[],pk(skA))=attacker(pk(skA[]))

, pkA → pk(skA[]) , pkB → pk(skB[])
Original
Protocol
Pi Calculus
Horn Clauses
Proverif
BP0,S


BP0,S : Horn clauses of the protocol
Bb : Horn clauses of allowed begin event.
We are back!

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion

Authenticity verification on Proverif

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion
Pros
Cons
Fully Automatic
Sometimes no termination
Unlimited number of sessions
Sometimes not Complete
General cryptographic
primitives
Proverif

Inductive method
Inductive
Model Checking
similarApproach
to Proverif (Mur phi)
◦ Proverif is kind of automatic
Automaticity

Y
N
Y
Model checking automatic
◦ Infinate session in Proverif.
Number of
States Support
Infinite
Infinite
Finite
Concurrency
Support
Y
Y(Manually)
Y(limited)

Whole picture

Process Calculus

Definition of Secrecy and Authenticity

Translation into Horn Clauses

Demo

Comparison

Conclusion
New Technique for
Authenticity verification in Cryptographic
Protocol
Fully automatic
 Precise sematic foundation
 Unbounded number of sessions
Support general cryptographic primitive


```