Verification of internet protocol properties using cooperating automaton objects
| Autor: | Ludmila Fedorchenko, Fedor Novikov, Dmitriy Levonevskiy, Irina Afanasieva |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
business.industry
Computer science Distributed computing Automata-based programming 020206 networking & telecommunications 02 engineering and technology Specification language Information security Formal methods law.invention law Internet Protocol 0202 electrical engineering electronic engineering information engineering The Internet business Communications protocol Protocol (object-oriented programming) |
| Zdroj: | SIN |
| DOI: | 10.1145/3357613.3357639 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|