Parallel real time investigation of communication security changes based on probabilistic timed automata

Abstract

The proposition is connected with the research of the security or threats referring to message decryption, user dishonesty, a nonfresh nonce, uncontrolled information jurisdiction, etc. (that means security properties - attributes), in network communication processes [3]. Encrypted messages are usually sent in the form of protocol operations. Protocols may be mutually interleaving, creating the so called runs, and their operations can appear as mutual parallel processes. The investigation regards both particular security attributes and their compositions referring to more general factors, such as: Concrete users, protocols, public keys, secrets, messages, etc. Probabilistic timed automata (PTA) and Petri nets characterize the token set and the complex form of conditions which have to be fulfilled for the realization of transition [5]. The abovementioned situation forms a conception pertaining to the parallel strategy realized with the help of the Petri net that includes the set of security tokens (attributes) in each node.