Using automated model analysis for reasoning about security of web protocols

摘要: Interoperable identity and trust management infrastructure plays an important role in enabling integrations cloud computing environments. In the past decade or so, several web-based workflows have emerged as de-facto standards for user resource access across enterprises. Establishing correctness of such web protocols is immense importance to a large number common business transactions on web. this paper, we propose framework analyzing security protocols. A novel aspect our proposal bringing together two contrasting styles used protocol analysis. We use inference construction style, which well-known BAN logic has been extended reason about protocols, conjunction with, attack style that performs SAT based model-checking rule out certain active attacks. The result analysis method shares simplicity intuitive appeal belief logics, at same time covers wider range along with ability automatically find To illustrate effectiveness, case study leading presented, where application results previously unreported being identified.