부산대학교 도서관

The Internet of Things advancements has enabled smart city scenarios worldwide. A tight nit communication, on the one hand, is required for device management and monitoring, but on the other hand, it has raised risks in information exchange in cross-domain scenarios. Keeping in view the above issues, this article considered well-known cross-domain access control protocols, i.e., Shibboleth, xDAuth, and OAuth to ensure user’s security. And, the existing work focused specifically on their implementations without verifying if they are effective for the security scenarios. We aim to verify their claim of fulfilling the claimed security requirements or not. We did a Cyber Attack Analysis to highlight the possible security attacks in smart city scenarios. Then, the protocols are verified against those issues to critically analyze if they are the best fit for the said scenario. The Z3-solver and Satisfiability Modulo Theories Library have been in use for protocol verification purposes. Results reveal that the protocol models are functioning correctly in terms of confidentiality, availability, and integrity. Verifying these protocols in terms of other security properties is part of our future work.