First Pronobis Meeting LSV, 22 mai 2006. -------------------------------------------------------- 10h. JGL: présentation générale + SECSI + LSV. -------------------------------------------------------- 10h30. Catuscia: presentation of Comète. Central theme: async pi-calc + a probabilistic input-choice construct. Used to specify security protocols (fair exchange [Kostas, Catuscia] based on oblivious transfer, various anonymity protocols [Kostas, Catuscia].) Model-checker based on Prism developed with Marta's group [Parker, Wu]. Anonymity: - study of a notion of strong probabilistic anonymity [Catuscia, Mohit Bhargava]. combines non-determinism (anonymous agents) and probability (protocol mechanisms). Theory of evidence. - probable innocence: - satisfied by "real protocols" like Crowds. - various definitions: - limit on the probability of detecting the culprit (Rubin); - limit on the probability of the agent to be the culprit (Halpern, O'Neil); -> developing a notion combining both [Kostas, Catuscia] - future work: - other forms of non-determinism [with Purnina]; - group anonymity [with Purnina]; - extension to other paradigms of partial information hiding [with Sardaouna]; - relation with information theory [project Printemps, with Prakash]; - logic based on conditional probability. Concurrent Constraint Programming (CCP). - applications to security: - constraints = partial knowledge accumulated by adversary; - monotonic evalution of the store = monotonic adversary; SPL (Winskel, Crazzolara), applied pi-calculus. - advantages: elegant and simple denotational semantics based on closure operators (Panangaden, Saraswat 1991). - CCP as a subset of the pi-calculus (Valencia, Saraswat, Victor, Catuscia); - project followed by Valencia. Collaboration with Columbian universities. -------------------------------------------------------- 11h. Roberto Segala. Mostly work in progress, rather than finished work. - comparative semantics - alternating and non-alternating models; all models are instances of the non-alternating case; - simulation and bisimulation relations; - logical characterization: extensions of HM logic; - non-discrete measures: stochastic transition measures; real-time systems (continuous); - verification of cryptographic protocols: - task-based PIOAs; oblivious transfer; - approximate simulations: authentication, matching conversations. Probabilistic Automata NA: NA = (Q, q0, E, H, D), transition relation D \subseteq Q x (E U H) x Disc(Q) where Disc(Q) is space of discrete probability distributions over Q. H: internal (hidden) actions. E: external actions, E & H = empty. Logical characterization: phi ::= true | not phi | phi and phi | phi | [phi]_p where [phi]_p holds whenever prob (phi) >= phi is a complete logic for bisimulation. Stochastic Transition Systems (Cattani, Segala, Kwiatkowska, Normal). Same, with sigma-fields for actions and states, too. But need schedulers to be measurable, i.e., so as to define Markov kernels. (Measurable) Markov kernels are preserved by projection -> modularity. UC security (Canetti). See talk by Pereira (notes reproduced below). Approximate simulations [Segala, Turrini]. to describe the notion of matching conversations (Bellare, Rogaway) in authentication. ---[snip]Talk by Olivier Pereira, LSV, 16 mai 2006[snip--- Olivier Pereira (with Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Roberto Segala) Using Task-Structured PIOAs to Analyze Security Protocols (PIOA = Probabilistic Input-Output Automata, by Roberto Segala). PIOA : state variables, actions (input, output, internal), transitions: state x action -> Disc(states)_\bot [Disc = discrete distributions on states.] Add internal nondeterminism for output and internal actions, which is not algorithmically resolved, and kept unresolved in the analyzed systems. Tasks are used to resolve nondeterminism: - equivalence classes on actions (send message 1, select key, give turn to adv, etc.) - given a task, at most one possible (probabilistic) action. Task schedulers resolve nondeterminism and give probabilistic executions: - are sequences of tasks; - constraint: task schedulers do not give extra power to adv; - execution: read first task, find and execute the action if enabled, then go to next task; - proofs quantify over all possible task schedulers. Example: oblivious tranfer. Input actions: in(x)_Trans, x in {0,1} -> {0,1} (maps request to requested bit) in(i)_Rec, i in {0,1} Output actions: out(x)_Rec, x in {0,1} State: consists of two (imperative) variables: inval(Trans) in ({0,1} -> {0,1})_\bot, initially \bot inval(Rec) in {0,1,\bot}, initially \bot. Transitions: in(x)_Trans: if inval(Trans)=\bot then inval(Trans):=x in(i)_Rec: if inval(Rec)=\bot then inval(Rec):=i out(x)_Rec: pre inval(Trans), inval(Rec) != \bot and x=inval(Trans)(inval(Rec)). Tasks: {out(*)_Rec} UC-style security: protocol pi realizes functionality phi iff for every task-PIOA A, there is a task-PIOA S such that pi | A <= phi | S where <= is an implementation relation for task-PIOAs: A <= B means that for every environment E and task scheduler for A | E, there is a task scheduler for B | E st. E cannot distinguish A from B. <= is transitive and composable (ie, compatible with parallel composition |). Two variants: - <=_0 for perfect indistinguishability; proved using a sound simulation relation; very systematic proofs; - <=_{neg, pt} for computational indistinguishability (poly time adv, negligible advantages). Computational assumptions are expressed in the form C1 <=_{neg, pt} C2. Example: hardcore predicates for trapdoor permutations. SH <=_{neg, pt} SHR where SH does: - given two random sources f (random permutation) and y, sends f, and f (y), B(y) (hardcore bit) and SHR just draws f, z (claimed value of f(y)) and b (claimed B(y)) at random. What if we use 2 hardcore bits (generated from same f)? By composition and transitivity, SH2 <=_{neg, pt} SHR2. Proving T1 <=_0 T2: by standard simulation techniques (also relating distributions). Case study on a simple oblivious transfer protocol [GMW87]. ---[snip]end of talk by Olivier Pereira[snip]--- -------------------------------------------------------- 11h45. Angelo Troina. Time and probability based information flow analysis. (with Ruggero Lanotte [U. Insubria at Como], Andrea Maggiolo Schettini [U. Pisa]). Multilevel security (non-interference). Low-level agents are not able to deduce anything about the activity of high level agents. Timed case: (Focardi, Gorrieri, Martinelli 2000), (Evans, Schneider 2000), (Barbuti, Tesei 2003). Probabilistic case: (Gray, 1992), (Aldini, Bravetti, Gorrieri 2004), (Di Pierro, Hankin, Wiklicky 2004). Model: probabilistic timed automata; bisimulation. (Sigma, X, Q, q0, delta, pi), where X is set of clocks, configs (q,v) where q in Q, and v is a valuation mapping clocks to their values. A weak bisimulation is an equivalence relation R such that for every (s,s') in R and equivalence classes C of R, Pr [s, tau^* alpha, C] = Pr [s', tau^* alpha, C] for every alpha in Sigma U {tau} U \real^+ (last component is for idle waiting). New definitions: A \ L restricts actions to set L, renormalizing probabilities; L / A (hiding) replaces every translation label a in L by tau; parallel composition A1 ||^p_L A2 (A1 advances with probability p, A2 with 1-p) obtained by hiding wrt. L and renormalizing. S satisfies non-interference (NI) iff S / Sigma_H is weakly bisimilar to S \ Sigma_H where Sigma_H is set of high-level actions. Decidable because weak bisim is decidable (finite state, guards as in timed automata). Information flow analysis: probabilitistic and/or timed security properties. Good property: if we satisify (probabilistic, timed) NI then forgetting about probas/times gives us systems that satisfy the corresponding weaker notion of NI. The converse does not hold. Non-deducibility on composition (NDC): S satisfied NDC iff for every high level agent Pi, for any p, for any L (high level), S / Sigma_H weakly bisim (S ||^p_L Pi) \ Sigma_H. Decidable: split possible Pi's in finitely many equivalence classes. Note: mNDC => mNI for every model m (probabilistic, timed, both). Observations and future work: - introduce approximate version of weak bisim for PTA; - we can formulate other well-known information flow security properties within our framwork; - extend the model with cryptographic primitives in order to analyze security protocols; - develop an automatic technique to adjust insecure systems. -------------------------------------------------------- 15h JGL. On capacities, games, and previsions. -------------------------------------------------------- 15h45 Catuscia Palamidessi (with Mohit Bhargava) Probabilistic and Nondeterministic Aspects of Anonymity. The concurrency approach to anonymity (Schneider-Sidiropoulos) Let A = {a(i) | i in Anonymous agents} = anonymous actions B = actions visible to observers C = Actions - (A U B) actions we want to hide Defn: P is anon iff its set of traces is invariant wrt any permutation p of the actions in A, i.e. p(Traces(P)) = Trace(P) (after projection onto B?) Mix proba and nondet, using proba async pi-calc (Herescu, Palamidessi 2000) semantics based on probabilistic automata of Segala and Lynch, 1994. S-S encode proba as non-det. Encoding "beyond suspicion" level of anonymity (strongly probabilistic anon.) (in the sense of Reiter and Rubin.) What Chaum proves: for every i, o if o => a then p(a(i)|o) = p(a(i)|a). (o => a meaning that we can observe that some agent paid) provided the coins are fair. Ie, the observation of o does not add anything to the knowledge of p(a(i)), except that a has been performed ~ conditional anon by Halpern and O'Neill. Pbs: may depend on the probs of the agents; not applicable to non-det users. Formalize strongly prob anon. in terms of notion of evidence. Given a set of exhaustive and mutually exclusive hypothesis h1...hn, and an event o, what is the evidence, given o, that h1 holds? - prob: evidence (hi,o) = p(o|hi) - nondet: evidence (hi,o) = p_{hi}(o) / sum_j p_{hj} (o) = prob case with uniform distribution. -------------------------------------------------------- 16h40 Dave Parker - Research activities at Bham. Focus: probabilistic verification. PRISM. MDPs + discrete/continuous time MCs. Handles PCTL, and CSL, plus extensions. Efficient MTBDD-based (multi-terminal) implementation. Discrete event simulation engine for MCs (not MDPs). Cost/reward-based property analysis. Improved tool links: eg, CADP (for bisimulation; Verimag, i.e., Caesar-Aldebaran). Counterexample generation. Research areas: efficiency improvements (symbolic impl., parallelisation, grid computing), model-checking algorithms (symmetry reduction, abstraction techniques for MDPs, partial order reduction [Baier et al.], compositionality), additional models and formalisms (real-time probabilistic model-checking (PTAs), probabilistic calculi for mobility (pi-calculus, ambients)). Also applications of probabilistic model-checking: - ubiquitous computing (manet's); - security protocols: prob. contract signing (with Shmatikov), anonymity; - systems biology (CTMCs, signalling pathways: cyclin, FGF, e-coli(sigma_32)). - Probabilistic pi-calculus model-checking [with Catuscia, Peng]. Restrictions: - control-finite (no recursion within parallel) - input-closed (no inputs from environment) Combine MMC (Stony Brook; pi-calculus model-checker for mu-calculus) with PRISM. - Game-based abstraction for MDPs. ie., CEGAR. Use Simple Stochastic Games [Condon 92], where we have 3 players: 1, 2, and probabilistic. Encode abstraction by having player 1 control non-determinism from abstraction, player 2 control original non-determinism. Analysis of SSGs: reachability of goal vertex set F. p_{a1, a2} (F) = prob. to reach F under player strategies a1, a2. Optimal probs sup_{a1} inf_{a2} p_{a1, a2} (F) and sup_{a2} inf_{a1} p_{a1, a2} (F) computable by iterative methods, as in MDPs. Then compute bounds for pmin(F) and pmax(F) in MDP: - inf_{a1,a2} p_{a1, a2} (F) <= pmin(F) <= sup_{a1} inf_{a2} p_{a1, a2} (F) - sup_{a2} inf_{a1} p_{a1, a2} (F) <= pmax(F) <= sup_{a1,a2} p_{a1, a2} (F) Case study: the zeroconf protocol (decentralized IP address config. protocol).