Verification of internet protocol properties using cooperating automaton objects

Reliable verification of compliance with information security requirements when exchanging data on the Internet is an urgent task. Information is transferred through interaction protocols that are being constantly updated and changed. Methods for verifying the compliance of new protocols with safety requirements are practically significant. Among compliance verification methods, an important place belongs to formal methods based on the study of adequate protocol models and software that implements these protocols. Such methods are known as symbolic protocol verification methods. The article describes a method for symbolic verification of such protocols. The advantage of the proposed method is the comparative simplicity and straightforwardness of the verification process achieved due to the expressive power of the used behavior specification language. The protocol specification uses the model of interacting automaton objects. The language used is CIAO (Cooperative Interaction of Automata Objects). Verification is considered using the TLS (Transport Level Security) handshake protocol as an example.