Verifying authentication protocols in CSP. Schneider, S. IEEE Transactions on Software Engineering, 24(9):741--758, September, 1998. 00381
doi  abstract   bibtex   
This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs
@article{schneider_verifying_1998,
	title = {Verifying authentication protocols in {CSP}},
	volume = {24},
	issn = {0098-5589},
	doi = {10.1109/32.713329},
	abstract = {This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder (1978) public key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs},
	number = {9},
	journal = {IEEE Transactions on Software Engineering},
	author = {Schneider, S.},
	month = sep,
	year = {1998},
	note = {00381},
	keywords = {Authentication, CSP, CSP, Computer Society, Computer Society, Digital signatures, IEC standards, IEC standards, ISO standards, ISO standards, Logic, Logic, Needham-Schroeder protocol, Needham-Schroeder protocol, Public key, Public key, Security, authentication, authentication protocol verification, authentication protocol verification, communicating sequential processes, communicating sequential processes, digital signatures, formal verification, formal verification, message authentication, message authentication, protocols, protocols, public key cryptography, public key cryptography, public key protocol, public key protocol, security, semantic framework, semantic framework},
	pages = {741--758}
}

Downloads: 0