[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all

      I would like to announce the following report, which is an 
extended version of a paper with the same title
presented at SecCo'07 (proceedings to appear in ENTCS):


State-oriented noninterference for CCS

    We address the question of typing noninterference (NI) in Milner's
    Calculus of Communicating Systems (CCS), in such a way that Milner's
    translation of a standard parallel imperative language into CCS
    preserves both an existing NI property and the associated type
    system. Recently, Focardi, Rossi and Sabelfeld have shown that a
    variant of Milner's translation, restricted to the sequential
    fragment of the language, maps a time-sensitive NI property to that
    of Persistent Bisimulation-based Non Deducibility on Compositions
    (PBNDC) on CCS. However, since CCS was not equipped with a security
    type system, the question of whether the translation preserves types
    could not be addressed. We extend Focardi, Rossi and Sabelfeld's
    result by showing that a slightly different variant of Milner's
    translation preserves a time-insensitive NI property on the full
    parallel language, by mapping it again to PBNDC. As a by-product, we
    formalise a folklore result, namely that Milner's translation
    preserves a natural behavioural equivalence on programs. We present
    a type system ensuring the PBNDC-property on CCS, inspired from type
    systems for the pi-calculus. Unfortunately, this type system as it
    stands is too restrictive to grant the expected type preservation
    result. We sketch a solution to overcome this problem.


Comments most welcome

Best regards



Ilaria Castellani, INRIA, 2004 Route des Lucioles, 
BP 93, 06902 Sophia-Antipolis Cedex, FRANCE                         
Tel.: +33 (0)4 92 38 76 40   Fax: +33 (0)4 92 38 50 29       

Reply via email to