Khurana, HimanshuGligor, Virgil D.The process of negotiating common access states in dynamic coalitions that comprise tens of autonomous domains sharing hundreds of resources is time-consuming and error-prone if performed without the benefit of automated tools. This process is also repetitive since, during the lifetime of a dynamic coalition, member domains must undertake the task of negotiating common access states multiple times as domains leave and new ones join the coalition. To define and verify the correctness of tools for automated negotiation, we develop a formal state-transition model of the process of negotiating a common access state. We extend an existing Role Based Access Control (RBAC) language to illustrate a wide variety of negotiation constraints and present a resolution procedure for verifying the satisfaction of such constraints in the state-transition model.en-USTechnical Report