Inductive verification of cryptographic protocols

作者: Giampaolo Bella

DOI:

关键词: OpenPGP cardHash-based message authentication codeKey managementEmbedded systemCryptographic protocolComputer scienceComputer networkCryptographic primitive

摘要:

参考文章(72)
A. W. Roscoe, Model-checking CSP A classical mind. pp. 353- 378 ,(1994)
Giampaolo Bella, Lawrence C. Paulson, Mechanising BAN Kerberos by the inductive method computer aided verification. pp. 416- 427 ,(1998) , 10.1007/BFB0028763
Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols Journal of Computer Security. ,vol. 6, pp. 85- 128 ,(1998) , 10.3233/JCS-1998-61-205
L.C. Paulson, Mechanized proofs for a recursive authentication protocol ieee computer security foundations symposium. pp. 84- 94 ,(1997) , 10.1109/CSFW.1997.596790
Giampaolo Bella, Modelling Agents' Knowledge Inductively international workshop on security. pp. 85- 94 ,(1999) , 10.1007/10720107_12
G. Lowe, A hierarchy of authentication specifications Proceedings 10th Computer Security Foundations Workshop. pp. 31- 43 ,(1997) , 10.1109/CSFW.1997.596782
Roger M. Needham, Michael D. Schroeder, Using encryption for authentication in large networks of computers Communications of the ACM. ,vol. 21, pp. 993- 999 ,(1978) , 10.1145/359657.359659
R. Bird, I. Gopal, A. Herzberg, P. Janson, S. Kutten, R. Molva, M. Yung, The KryptoKnight family of light-weight protocols for authentication and key distribution IEEE ACM Transactions on Networking. ,vol. 3, pp. 31- 41 ,(1995) , 10.1109/90.365435
F.J.T. Fabrega, J.C. Herzog, J.D. Guttman, Strand spaces: why is a security protocol correct? ieee symposium on security and privacy. pp. 160- 171 ,(1998) , 10.1109/SECPRI.1998.674832
Giampaolo Bella, Lack of Explicitness Strikes Back international workshop on security. pp. 87- 93 ,(2000) , 10.1007/3-540-44810-1_14