Towards a Better Concurrency/Security Framework
notes from Andrew Miller
Outline
- Need for concurrency models in Crypto
- Concurrency hazards
- Difficulty in formalism arbitrary concurrency
- UC security experiment
- Dummy lemma
- Composition theorem
- Pi Calculus
- Work in progress - encoding the UC experiment in Pi calculus
Modern Cryptography - Ideal/Real
- Ideal/Real
- a protocol “realizes” its specification if it is “just as good as” having access to a magic trusted third party
- widely accepted way to define security, though somewhat unwieldy
- “Constructive Cryptography”
Secure protocols constructed by composing simpler secure protocols.
- Can gracefully express *all* desirable properties
- Especially Correctness, and Privacy (as well as knowledge, non-coercion, etc.,),
- Alternative is to require piecemeal experiments/properties
- This is actually hard
- state-of-the-art falls short
- time for PL to save the world (again)
How do we actually formalize any of this?
Motivating Example
Interactive (Zero-Knowledge) Proof Systems
Simple definition is tractable.
- But, hazards when run concurrently
- Naive attempt to generalize grows complex
PL knows a candidate (Pi Calculus)....
Zero Knowledge IP (GMR ‘89)
P,V are interactive protocols. L is a language. x is a statement (possibly) in L. w is a witness.
x
P
V
x,w
Accept/Reject
Requirements:
1. Complete:
If x in L, V accepts
2. Sound:
For any P*,
If x !in L, V rejects
3. Zero Knowledge:
For any V*, exists S,
View(V*) = View(S)
x in L
Zero Knowledge IP (GMR ‘89)
P,V are interactive protocols. L is a language. x is a statement (possibly) in L. w is a witness.
x
P*
V
x
Accept/Reject
Requirements:
1. Complete:
If x in L, V accepts
2. Sound:
For any P*,
If x !in L, V rejects
3. Zero Knowledge:
For any V*, exists S,
View(V*) = View(S)
x not in L
Zero Knowledge IP (GMR ‘89)
P,V are interactive protocols. L is a language. x is a statement (possibly) in L. w is a witness.
x
P
V*
x,w
Output/View
Requirements:
1. Complete:
If x in L, V accepts
2. Sound:
For any P*,
If x !in L, V rejects
3. Zero Knowledge:
For any V*, exists S,
View(V*) ~ View(S)
x in L
x
SV*
Output/View
~
Zoom in a Bit
P
V
Input
Input
Output
Communication
Zoom in a Bit
P
V
Input
Input
Output
m1p
m1v
mNp
mNv
…….
Decomposable into functions:
m1p = P1(inputP)
m1v = V1(inputV,m1p)
m2p = P2(inputP,m1v)
m2v = V2(inputV,m1p,m2p)
……
mNv = VN(inputV,m1p,...,mNp)
For any N, we could code up this experiment in EasyCrypt!
This is a game-based definition.
It is fully described by a protocol narration diagram.
Zero Knowledge IP (GMR ‘89)
Quantifies over “all” protocols (A,B) where A and B take turns communicating.
A → B
B ← A
… and so on
Only matters output of A and B.
Are secure protocols
Closed Under Composition?
Short answer: No
Long answer: depends what kind of composition
Goldreich and Krawczyk 1996
Sequential Composition
x
P
V
x,w
x in L
P
V
Accept/Reject
….
Original standalone definition is *not* closed under sequential composition.
However, this is easily remedied.
V*
P
x,w
x in L
P
….
Parallel Composition
x
P
V
x,w
x in L
P
V
P
V
P
V
Accept/Reject
x
P
x,w
x in L
P
P
P
V*
Output/View
Counter Example
x
P1
V
f
x
P2
V
f
Composition Problems
Lindell, Yehuda, Anna Lysyanskaya, and Tal Rabin. "On the composition of authenticated byzantine agreement." Journal of the ACM (JACM) 53.6 (2006): 881-917.
Many other protocols for, e.g., Byzantine agreement, are not secure under concurrent composition
Arbitrary Concurrent Composition
No longer straightforward to decompose into functions.
Countless “communication patterns” are possible
Synchronous - round-based (but Adversary gets priority!)
Adaptive - adversary chooses *who* to corrupt halfway through
Rushing - adversary chooses who to corrupt after seeing round of messages
Bounded non-determinism - adversary can’t delay messages *forever*
Asynchronous - adversary does what it wants when it wants whatever
Universal Composability experiment
Protocol Pi’ emulates protocol Pi iff:
For any adversary A, there exists a simulator S, such that for every environment E, the environment E distinguishes between Exec(E,A,Pi) and Exec(E,S,Pi’) with negligible probability.
S
Canetti, Ran. "Universally composable security: A new paradigm for cryptographic protocols." Foundations of Computer Science, 2001. Proceedings. 42nd IEEE Symposium on. IEEE, 2001.
Dummy Lemma
Only need to consider the “transparent” dummy adversary that forwards environments instructions. This drastically simplifies proofs.
Protocol Substitution
Terminology: realizes, substitution
Proof of Composition Theorem (1/2)
Proof of Composition Theorem (2/2)
Pi Calculus
Simple formal language with non-deterministic semantics.
...
Pi Calculus Examples
First Approach
- Encode the UC Execution Experiment in Pict
- Fix a protocol “pi”
- Environment invokes:
- As many instances of pi as it likes
- On arbitrary sets of parties
- With any parameters of its choice
- Instances of pi may invoke subroutines
Including “ideal functionality” subroutines shared with other parties
Related work
- Delaume et al. 2006. Simulation based security in the applied pi calculus
Pi calculus UC framework
Proved Composition theorems
…. but
Problem
- The non-deterministic semantics of Pi are incompatible with information-theoretic and computational security. (“May” and “Must”)
- Execution order is not *random* from some distribution or chosen by a *computational procedure*.
- Immediate attempts to fix it break down
Is the adversary just a process? Or a supervisor that sees state of all machines?
UC Approach to this problem
System of Interactive Turing Machines.
Execution semantics is deterministic.
On “send”, control is passed to a process that can “read”.
This means having to build contrived gadgets, so Adv *effectively* acts as scheduler.
- Other differences to Pi:
No channels - processes have PID identity strings
Messages are buffered
Weird Gadgets - F_AUTH
- Once activated, control is passed to the adversary. Adversary may never respond again, and message is lost forever.
- If you do hear back, message is untampered with and came from person who said it.
- Trivially realizable (so, the definition is a huge let down)
Solution - ongoing
- Deterministic semantics for Pi calculus.
Main engineering challenge is to trace “who owns the ‘read’ end of the channel.
- Interface structure for protocols to obtain access to shared ideal functionalities.
Why not just use UC?
- No implementation
(turing machines inconvenient)
- Big gap between formalism and plausible implementations
- Easycrypt supports game definitions, but not UC. Ability to decompose a protocol into simple functions is used extensively. This work is a step towards UC-easycrypt
Immediate Future
Preliminary results for UC. Would prefer formal/mechanical tools
1. Asynchronous network too weak, current “synchronous” models too strong.
My result: a better synchronous model (maybe this fall?)
2. “Real Name” authentication is too strong, but nothing good is possible without any authentication
My result: reasonable “pseudonymous” security in a Bitcoin-like model
puzzles and “allocation of computational power” assumption
stop here for now
thanks Kris and Matt for pi calc discussions
Jon and Elaine for UC discussions
Weird Gadgets - F_TOOSTRONG
- Upon receiving
(“send”,sid,A,m) from party A,
send
(“sent”,sid,A,m) to party B.
Eventual Delivery Gadget
- Hack - force adversary to use unary notation
- Relies on resource counting (not mentioned yet)
- Can’t delay forever
Clock
Intent is to allow a set of parties P to synchronize with each other, and corrupted parties can’t prevent clock from advancing.
- Problem: unintended power. Used to prove honesty
Composition with Global State (GUC)
GUC->EUC proof
Simple proof that illustrates executing simulators in sandboxes
Alternate Approach
Single globally-shared clock
Registration: rather than fixed participation
Even honest parties