Secrecy in stochastic discrete event systems

In security critical system, keeping a property of system behaviors secret from an observer (or adversary, who has a partial observation of any executed behavior) is crucial. This paper proposes two notions of secrecy for stochastic discrete event systems. The notion of S_τ-Secrecy requires the set of system traces, that reveals the secret to an observer, occurs with probability smaller than τ. A stronger notion of Increasing-S-Secrecy captures system requirement that the secrecy level become increasingly tighter as the system evolves for longer periods. Algorithms for verifying both notions are provided. An illustrative example is examined to demonstrate the proposed notions.