Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.06833 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909610790617088 |
|---|---|
| author | Nasrabadi, Faezeh Künnemann, Robert Nemati, Hamed |
| author_facet | Nasrabadi, Faezeh Künnemann, Robert Nemati, Hamed |
| contents | The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_06833 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Symbolic Parallel Composition for Multi-language Protocol Verification Nasrabadi, Faezeh Künnemann, Robert Nemati, Hamed Cryptography and Security The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems. |
| title | Symbolic Parallel Composition for Multi-language Protocol Verification |
| topic | Cryptography and Security |
| url | https://arxiv.org/abs/2504.06833 |