TY - GEN
T1 - Formal Verification and Security Analysis of AMQP
AU - Liu, Huiying
AU - Dong, Wenting
AU - Zhu, Huibiao
AU - Su, Ziqing
N1 - Publisher Copyright:
© 2024 IEEE.
PY - 2024
Y1 - 2024
N2 - AMQP, serving as the application layer standard protocol for advanced message queuing systems, has garnered widespread adoption in middleware systems, including Rab-bitMQ, ActiveMQ, and Qpid. However, the key properties and security of AMQP's messaging mechanism remain unverified. Hence, in this paper, we employ process algebra CSP to formalize the AMQP and verify properties such as deadlock freedom, data reachability, concurrency, sequence consistency, and scala-bility. The verification results indicate that AMQP satisfies these properties, demonstrating the reliability in message transmission. Moreover, to further analyze the security of AMQP messaging mechanism, the intruder model and SSL protocol model are introduced in this work. Meanwhile, the comparison of the verification results with and without SSL is also presented, showing an improvement of the AMQP messaging mechanism security.
AB - AMQP, serving as the application layer standard protocol for advanced message queuing systems, has garnered widespread adoption in middleware systems, including Rab-bitMQ, ActiveMQ, and Qpid. However, the key properties and security of AMQP's messaging mechanism remain unverified. Hence, in this paper, we employ process algebra CSP to formalize the AMQP and verify properties such as deadlock freedom, data reachability, concurrency, sequence consistency, and scala-bility. The verification results indicate that AMQP satisfies these properties, demonstrating the reliability in message transmission. Moreover, to further analyze the security of AMQP messaging mechanism, the intruder model and SSL protocol model are introduced in this work. Meanwhile, the comparison of the verification results with and without SSL is also presented, showing an improvement of the AMQP messaging mechanism security.
KW - AMQP
KW - CSP
KW - PAT
KW - Security
KW - Verification
UR - https://www.scopus.com/pages/publications/85204047468
U2 - 10.1109/COMPSAC61105.2024.00349
DO - 10.1109/COMPSAC61105.2024.00349
M3 - 会议稿件
AN - SCOPUS:85204047468
T3 - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
SP - 2177
EP - 2182
BT - Proceedings - 2024 IEEE 48th Annual Computers, Software, and Applications Conference, COMPSAC 2024
A2 - Shahriar, Hossain
A2 - Ohsaki, Hiroyuki
A2 - Sharmin, Moushumi
A2 - Towey, Dave
A2 - Majumder, AKM Jahangir Alam
A2 - Hori, Yoshiaki
A2 - Yang, Ji-Jiang
A2 - Takemoto, Michiharu
A2 - Sakib, Nazmus
A2 - Banno, Ryohei
A2 - Ahamed, Sheikh Iqbal
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 48th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2024
Y2 - 2 July 2024 through 4 July 2024
ER -