Reasoning about Cryptographic Protocols in the Spi Calculus
作者： Martín Abadi , Andrew D. Gordon
关键词: Equivalence (formal languages) 、 Secrecy 、 Cryptographic primitive 、 Encryption 、 Computability 、 Computer science 、 Pi calculus 、 Cryptographic protocol 、 Calculus 、 Cryptography
摘要: The spi calculus is an extension of the pi with constructs for encryption and decryption. This paper develops theory calculus, focusing on techniques establishing testing equivalence, applying these to proof authenticity secrecy properties cryptographic protocols.
springer.com
core.ac.uk
sci-hub.st 参考文章(20)
John McLean, James W. Gray, Using Temporal Logic to Specify and Verify Cryptographic Protocols (Progress Report) ,(1995)
Robin Milner, Communication and Concurrency ,(1989)
Bruce Schneier, Phil Sutherland, Applied Cryptography: Protocols, Algorithms, and Source Code in C ,(1993)
Catherine Meadows, Applying Formal Methods to the Analysis of a Key Management Protocol Journal of Computer Security. ,vol. 1, pp. 5- 35 ,(1992) , 10.3233/JCS-1992-1102
J.K. Millen, The Interrogator model ieee symposium on security and privacy. pp. 251- 260 ,(1995) , 10.1109/SECPRI.1995.398937
J.W. Gray, J. McLean, Using temporal logic to specify and verify cryptographic protocols Proceedings The Eighth IEEE Computer Security Foundations Workshop. pp. 108- 116 ,(1995) , 10.1109/CSFW.1995.518557
Armin Liebl, Authentication in distributed systems ACM SIGOPS Operating Systems Review. ,vol. 27, pp. 31- 41 ,(1993) , 10.1145/163640.163643
M. Boreale, R. Denicola, Testing Equivalence for Mobile Processes Information & Computation. ,vol. 120, pp. 279- 303 ,(1995) , 10.1006/INCO.1995.1114
R.A. Kemmerer, Analyzing encryption protocols using formal verification techniques IEEE Journal on Selected Areas in Communications. ,vol. 7, pp. 448- 457 ,(1989) , 10.1109/49.17707
Martín Abadi, Andrew D. Gordon, A calculus for cryptographic protocols: the spi calculus computer and communications security. pp. 36- 47 ,(1997) , 10.1145/266420.266432