Information Flow Analysis in a Discrete-Time Process Algebra

Some of the non interference properties studied in [4, 6, 18] for information flow analysis in computer systems, notably Æ , are reformulated here in a realtime setting. This is done by enhancing the Security Process Algebra of [6, 10] with some extra constructs to model real-time systems (in a discrete time setting); and then by studying the natural extensions of those properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate a case study of a system that presents no information flows when analyzed without considering timing constraints. But, when the specification is refined with time, some interesting information flows are detected.

• Type: Conference
• Year: 2000
• Where: CSFW
• Authors: Riccardo Focardi, Roberto Gorrieri, Fabio Martinelli
• Keywords: CSFW 2000, Information flows, Non Interference Properties, Security Privacy, Security Process Algebra