Analysis for Probabilistic and Timed Information Flow Security Properties via ptSPA

Information flow analysis is one of the primary approaches for analyzing computer security problems, such as covert channel and data leak. Security process algebra(SPA) is a classic method used in researching information security properties in nondeterministic system. To analyze the information security properties and capture the information leakage in probabilistic and real time system, SPA is extended in probabilistic and time setting. Probabilistic and time security process algebra(ptSPA), an extension of SPA, is proposed by first introducing the probabilistic and time calculus to specify activities constricted by probability and time, and extending the formal syntax and semantic to enhance the SPA. Then, the related notion of probabilistic and time bisimulation equivalence is presented, to describe two observable behavior traces are equivalent when considering probability and time. Based on ptSPA, several information flow security properties in probabilistic and real time system, such as TBSPNI, PTBNDC and SPTBNDC are defined, which can capture probabilistic and time covert channel while the original SPA cannot. The relations among the information flow security properties are analyzed. Finally, a case study is given to show that the expressiveness of calculus in ptSPA is possible to model and analyze probabilistic and time systems.