Cryptographic Stack Machine Notation One
A worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/528 |
| _version_ | 1818359731018792960 |
|---|---|
| author | S. E. Prokopev |
| author_facet | S. E. Prokopev |
| author_sort | S. E. Prokopev |
| collection | DOAJ |
| description | A worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic stack machine. The paper presents the syntax and semantics of CMN.1 and the principles of implementation of the CMN.1-based executable protocol specification language. The core language library (the engine) performs all the message processing, whereas a specification should only provide the declarative definitions of the messages. If an outcoming message must be formed, the engine takes the CMN.1 definition as input and produces the binary data in consistency with it. When an incoming message is received, the engine verifies the binary data with respect to the given CMN.1 definition memorizing all the information needed in the further actions. The verification is complete: the engine decrypts the ciphertexts, checks the message authentication codes and signatures, etc. Currently, the author's proof-of-concept implementation of the language (embedded in Haskell) can translate a CMN.1-based specifications both to the interoperable implementations and to the programs for the ProVerif protocol analyzer. The excerpts from the CMN.1-based TLS protocol specification and corresponding automatically generated ProVerif program are provided as an illustration. |
| first_indexed | 2024-12-13T20:49:33Z |
| format | Article |
| id | doaj.art-f0d8ace6260f4a9e88aff5554f8a12e3 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-13T20:49:33Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-f0d8ace6260f4a9e88aff5554f8a12e32022-12-21T23:31:54ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0130316518210.15514/ISPRAS-2018-30(3)-12528Cryptographic Stack Machine Notation OneS. E. Prokopev0Независимый исследовательA worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic stack machine. The paper presents the syntax and semantics of CMN.1 and the principles of implementation of the CMN.1-based executable protocol specification language. The core language library (the engine) performs all the message processing, whereas a specification should only provide the declarative definitions of the messages. If an outcoming message must be formed, the engine takes the CMN.1 definition as input and produces the binary data in consistency with it. When an incoming message is received, the engine verifies the binary data with respect to the given CMN.1 definition memorizing all the information needed in the further actions. The verification is complete: the engine decrypts the ciphertexts, checks the message authentication codes and signatures, etc. Currently, the author's proof-of-concept implementation of the language (embedded in Haskell) can translate a CMN.1-based specifications both to the interoperable implementations and to the programs for the ProVerif protocol analyzer. The excerpts from the CMN.1-based TLS protocol specification and corresponding automatically generated ProVerif program are provided as an illustration.https://ispranproceedings.elpub.ru/jour/article/view/528язык спецификаций криптографических протоколовнотация сообщений криптографических протоколовкриптографическая стековая машинавстроенные предметно-ориентированные языкиhaskellproveriftls |
| spellingShingle | S. E. Prokopev Cryptographic Stack Machine Notation One Труды Института системного программирования РАН язык спецификаций криптографических протоколов нотация сообщений криптографических протоколов криптографическая стековая машина встроенные предметно-ориентированные языки haskell proverif tls |
| title | Cryptographic Stack Machine Notation One |
| title_full | Cryptographic Stack Machine Notation One |
| title_fullStr | Cryptographic Stack Machine Notation One |
| title_full_unstemmed | Cryptographic Stack Machine Notation One |
| title_short | Cryptographic Stack Machine Notation One |
| title_sort | cryptographic stack machine notation one |
| topic | язык спецификаций криптографических протоколов нотация сообщений криптографических протоколов криптографическая стековая машина встроенные предметно-ориентированные языки haskell proverif tls |
| url | https://ispranproceedings.elpub.ru/jour/article/view/528 |
| work_keys_str_mv | AT seprokopev cryptographicstackmachinenotationone |