Information Technology Reference
In-Depth Information
2. There are infinite sessions between the participants. Because the LTS se-
mantics of our model is based on structural induction, we'll adopt the approach
similar to Paulson's inductive method [14].
As for future work, we plan to define formally other security properties based
on our model, and analyze the protocols such as Kerberos, SET etc.
References
1. Abadi, M., Fournet, C.: Mobile values, new names, and seucre communication. Pro-
ceedings of the 28th ACM Symposium on Principles of Programming Languages.
ACM Press (2001) 104-115
2. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus.
Information and Computation. 148(1) (1999) 1-70
3. Boreale, M.: Symbolic trace analysis of cryptographic protocols. Proceedings of the
28th International Colloquium on Automata, Languages and Programming. LNCS
2076, Springer-Verlag (2001) 667-681
4. Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R: Automatic valida-
tion of protocol narration. Proceedings of the 16th Computer Security Foundations
workshop. IEEE Computer Society Press, (2003) 126-140
5. Cardelli, L., Gordon, A.D: Mobile ambients. Foundations of Software Science and
Computational Structures. LNCS 1378, Springer-Verlag, (1998) 140-155
6. Crazzolara, F., Winskel, G.: Events in security protocols. Proceedings of the 8th
ACM conference on Computer and Communications Security. ACM Press (2001)
96-105
7. Dolev, D., Yao, A.C: On the security of the public key protocols. IEEE Transcations
on Information Theroy. 29(2) (1983) 198-208
8. Focardi, R., Gorrieri, R.: The compositional security checker: A tool for the ver-
ification of information flow security properties. IEEE Transactions on Software
Engineering. 23(9) (1997) 550-571
9. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)
10. Lowe, G.: Breaking and fixing the Needham-Schroeder Public-key protocol using
FDR. Proceedings of Tools and Algorithms for the Construction and Analysis of
Systems. LNCS 1055, Springer-Verlag (1996) 147-166
11. Milner, R.: Communication and Concurrency. Prentice Hall (1989)
12. Milner, R., Parrow, J., Walker, D.: A calculus of moblie processes(I and II). Infor-
mation and Computation. 100(1) (1992) 1-77
13. Needham, R., Schroeder, M.: Using encryption authentication in large networks of
computers. Communications of the ACM. 21(12) (1978) 993-999
14. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Jour-
nal of Computer Security. 6, (1998) 85-128
15. Pitts, A.M., Stark,I.: Observable properties of higher order functions that dy-
namically create local names, or: What's new? Proceedings of the 18th Interna-
tional Symposium on Mathematical Foundations of Computer Science. LNCS 711,
Springer-Verlag (1993) 122-141
16. Schneider, S.A.: Security properties and CSP. Proceedings of the IEEE Symposium
on Security and Privacy. IEEE Computer Society (1996) 174-187
17. Zhou, J., Gollmann, D.: Towards verification of non-repudiation protocols. Pro-
ceedings of the International Refinerment Workshop and Formal Methods Pacific.
Springer-Verlag (1998) 370-380
