Probabilistic Polynomial-Time CalculusSecurity as EquivalenceBridging the GapStandard Example: PRNGProcess Calculus ApproachChallengesNondeterminism Is Too StrongPPT Calculus: SyntaxProbabilistic Operational SemanticsProbabilistic SchedulingSimple ExampleComplexityHow To Define Process Equivalence?Probabilistic Observat’l EquivalenceProbabilistic BisimulationProvable Equivalences (1)Provable Equivalences (2)Connection with CryptographyReview: Decisional Diffie-HellmanElGamal CryptosystemDDH Semantic Security of ElGamalSemantic Security of ElGamal DDHCS 395TProbabilistic Polynomial-Time CalculusSecurity as EquivalenceIntuition: encryption scheme is secure if ciphertextis indistinguishable from random noiseIntuition: protocol is secure if it is indistinguishable from a perfectly secure “ideal” protocolSecurity is defined as observational equivalencebetween protocol and its ideal functionality• Both formal methods and cryptography use this approach, but with different notions of what it means for the adversary to “observe” the protocol executionBridging the GapCryptography: observational equivalence is defined as computational indistinguishability• No probabilistic poly-time algorithm can tell the difference between the real and the ideal protocol with more than negligible probabilityFormal methods: observational equivalence is defined as some form of process bisimulation• No probabilitities, no computational boundsGoal: bridge the gap by explicitly supporting probability and complexity in process calculusStandard Example: PRNGPseudo-random sequence Pn: let b = nk-bit sequence generated from nrandom bits (”seed”)in PUBLIC〈b〉 end Truly random sequenceQn: let b = sequence ofnkrandom bitsin PUBLIC〈b〉 end P is a cryptographically strong pseudo-random number generator if the two sequences are observationally equivalent P ≈ Q• Equivalence is asymptotic in security parameter nProcess Calculus Approach Write protocol in process calculus• For example, applied pi-calculusExpress security using observational equivalence• Standard relation from programming language theoryP ≈ Q iff for all contexts C[ ], same observations about C[P] and C[Q]• Inherently compositional (quantifies over all contexts)• Context (environment) represents adversaryUse proof rules for ≈ to prove observational equivalence to the “ideal” protocol[Abadi-Gordon and others]ChallengesProbabilistic formal model for crypto primitives • Key generation, random nonces, randomized encryptionProbabilistic attacker• Replace nondeterminism with probability• Need a formal way of representing complexity boundsAsymptotic form of observational equivalence• Relate to polynomial-time statistical testsProof rules for probabilistic observational equivalenceNondeterminism Is Too StrongAlice encrypts message and sends to BobA → B: { msg } KAdversary “nondeterministically” guesses every bit of the keyProcess E0c〈0〉 | c〈0〉 | … | c〈0〉Process E1c〈1〉 | c〈1〉 | … | c〈1〉Process E c(b1).c(b2)...c(bn).decrypt(b1b2...bn, msg)In reality, at most 2-nchance to guess n-bit keyPPT Calculus: SyntaxBounded π-calculus with integer termsP :: = 0| cq(|n|)〈T〉 send up to q(|n|) bits| cq(|n|)(x).P receive| υcq(|n|).P private channel| [T=T] P test| P | P parallel composition| !q(|n|)P bounded replicationSize of expressions is polynomial in |n| Terms may contain symbol n; channel width and replication bounded by polynomial of |n|Probabilistic Operational SemanticsBasic idea: alternate between terms & processes• Probabilistic scheduling of parallel processes• Probabilistic evaluation of terms (incl. rand)Outer term evaluation• Evaluate all exposed terms, evaluate testsCommunication• Match up pairs “send” and “receive” actions• If multiple pairs, schedule them probabilistically– Probabilistic if multiple send-receive pairsalternateProbabilistic SchedulingOuter term evaluation• Evaluate all exposed terms in parallel• Multiply probabilitiesCommunication• E(P) = set of eligible subprocesses• S(P) = set of schedulable pairs• Schedule private communication first• Probabilistic poly-time computable scheduler that makes progressSimple ExampleProcess• c〈rand+1〉 | c(x).d〈x+1〉 | d〈2〉 | d(y).e〈y+1〉Outer evaluation • c〈1〉 | c(x).d〈x+1〉 | d〈2〉 | d(y). e〈y+1〉• c〈2〉 | c(x).d〈x+1〉 | d〈2〉 | d(y). e〈y+1〉Communication• c〈1〉 | c(x).d〈x+1〉 | d〈2〉 | d(y). e〈y+1〉rand is 0 or 1 with prob. ½Each with prob ½Choose according to probabilistic schedulerComplexityBound on number of communications• Count total number of inputs, multiplying by q(|n|) to account for bounded replication !q(|n|)PBound on term evaluation• Closed term T is evaluated in time qT(|n|)Bound on time for each communication step• Example: c〈m〉 | c(x).P → [m/x]P – Bound on size of m; previous steps preserve # of x occurrencesFor each closed process P, there is a polynomial q(x) such that for all n, all probabilistic poly-time schedulers, evaluation of P halts in time q(|n|)How To Define Process Equivalence?Intuition: P and Q are equivalent if no test by any context can distinguish them• | Prob{ C[P] → “yes” } - Prob{ C[Q] → “yes” } | < εHow do we choose ε?– Less than 1/2, 1/4, … ? (not an equivalence relation)– Vanishingly small? As a function of what?Solution: asymptotic form of process equivalence• Use security parameter (e.g., key length)• Protocol is a family { Pn}n>0 indexed by key lengthProbabilistic Observat’l EquivalenceAsymptotic equivalence within f• Families of processes { Pn}n>0{ Qn}n>0• Family of contexts { Cn}n>0• P ≈fQ if ∀ context C[ ]. ∀ observation v. ∃n0. ∀n>n0| Prob(Cn[Pn] → v) – Prob(Cn[Qn] → v) | < f(n)Asymptotic polynomial indistinguishability• P ≈ Q if P ≈fQ for every f(n) = 1/p(n) where p(n) isa polynomial function of nProbabilistic BisimulationLabeled transition system• Evaluate process in a “maximally benevolent context”• Process may read any input on public channel or send output even if no matching input exists in process• Label with numbers “resembling probabilities”Bisimulation relation• If P ~ Q and P P’,
View Full Document
Unlocking...