Generic verification of security protocols

Khan, Abdul Sahid ; Mukund, Madhavan ; Suresh, S. P. (2005) Generic verification of security protocols In: 12th International SPIN Workshop on Model Checking of Software, 22-24 Aug 2005, San Francisco, CA, USA.

Full text not available from this repository.

Official URL:

Related URL:


Security protocols are notoriously difficult to debug. One approach to the automatic verification of security protocols with a bounded set of agents uses logic programming with analysis and synthesis rules to describe how the attacker gains information and constructs new messages. We propose a generic approach to verifying security protocols in Spin. The dynamic process creation mechanism of Spin is used to nondeterministically create different combinations of role instantiations. We incorporate the synthesis and analysis features of the logic programming approach to describe how the intruder learns information and replays it back into the system. We formulate a generic “loss of secrecy” property that is flagged whenever the intruder learns private information from an intercepted message. We also describe a simplification of the Dolev-Yao attacker model that suffices to analyze secrecy properties.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag.
Keywords:Authentication Protocol; Security Protocol; Cryptographic Protocol; Secrecy Property; Model Check Approach
ID Code:114150
Deposited On:25 May 2018 04:55
Last Modified:25 May 2018 04:55

Repository Staff Only: item control page