Verification of secure gateway selection protocol using PI-calculus
Abhay Kumar Rai, Rajiv Ranjan Tewari · 2013
For modeling and verifying software systems Formal Methods is an effective methodology. Pi-calculus is a kind of process algebra which can be used to model concurrent and dynamic systems. For analyzing and verifying mobile concurrent systems described by pi-calculus we use Mobility Workbench (MWB) tool. This paper presents a protocol that provides secure gateway (GW) selection mechanism depending on sensitivity of data, as well as provides security to the sensitive data to be forwarded through secure GW from MANET domain to Internet. The proposed protocol allows a source node to forward sensitive data only through secure GW. We model and verify the proposed protocol using Formal Methods in MWB tool.