9th International Workshop on Security Issues in Concurrency

Program

09:20 - 09:30	Welcome
09:30 - 10:30	Invited talk: Carroll Morgan. Shadow- and Hyperdistribution Semantics for Noninterference and Refinement
10:30 - 11:00	Coffee break
11:00 - 11:30	Vincent Cheval, Stephanie Delaune and Hubert Comon-Lundh. A Decision Procedure for Trace Equivalence.
11:30 - 12:00	Alessandro Armando and Silvio Ranise. Automated Analysis of Infinite State Workflows with Access Control Policies
12:00 - 12:30	Chenyi Zhang Unwinding Theorems for Conditional Information Flow Policies.
12:30 - 14:30	Lunch
14:30 - 15:00	Mahrooghi Hamidreza and Mohammadreza Mousavi. Reconciling Operational and Epistemic Approaches to the Formal Analysis of Crypto-Based Security Protocols
15:00 - 15:30	Tri Ngo Minh and Marieke Huisman. Scheduler-related Condentiality for Multi-threaded Programs
15:30 - 16:00	Coffee break
16:00 - 17:00	Invited talk: Catuscia Palamidessi. Quantitative Information Flow and Applications to Differential Privacy in a Distributed Perspective
17:00 - 17:10	Closing

Invited Talks

• Carroll Morgan, University of New South Wales
  
  Title: Shadow- and Hyperdistribution Semantics for Noninterference and Refinement
  
  When concurrent processes exhibit both probabilistic and demonic choice, a third semantic question arises naturally: to what extent can demonic choices exploit probabilistic choices made at another time (eg earlier) or in another place (eg in a separate process)? This "locality issue" has been studied intensively for more than a decade, but is not yet resolved.
  
  Since the effect of locality is in essence to hide (or not to hide) some choices from others, it turns out that the semantic structures for that can also be exploited for hiding as in noninterference-style security. We have worked on this for some time, eg noninterference with demonic choice (but not probabilistic) [A], and more recently noninterference with probabilistic choice (but not demonic) [B]; some progress has been made on compositionality and, in the latter case, also on the relation between various measures of entropy.
  
  The technical component of the talk will be to describe the so-called "shadow" (qualitative, possibilistic) and "hyperdistribution" (quantitative, probabilistic) structures we have built for noninterference with a refinement partial order (ie an implementation order that respects secrecy). Less technically, I will outline how we came to this topic in the first place, and how what we have done by approaching security from refinement theory might match what others have done in the opposite direction, approaching refinement from security theory.
  
  [a] C.C. Morgan. The Shadow Knows: Refinement of ignorance in sequential programs. Conference version in Proc. Math Prog Construction 2006, LNCS 4014:359-78, 2006. Journal version in Science of Computer Programming, 74(8):629-653, 2009.
  
  [b] Annabelle McIver, Larissa Meinicke, and Carroll Morgan. Compositional closure for Bayes Risk in probabilistic noninterference. ICALP'10 Part II, pages 223-235, 2010.
  
  
• Catuscia Palamidessi, INRIA and LIX, Ecole Polytechnique
  
  Title: Quantitative Information Flow and Applications to Differential Privacy in a Distributed Perspective