B. {n-a, The formal definition of the rules are

O. {}, A. Says, N. B-{|nonce, A. Agent, and B. Agent, Crypt (shrK A) {|Nonce NA

O. , B. Server-{|nonce, N. Agent, A. Agent, and B. , Crypt (shrK A) {|Nonce NA,Agent A, Agent B|}, Crypt (shrK B) {|Nonce NA

M. Abadi, M. Burrows, and R. Needham, A logic of authentication, Proceedings of the Royal Society, pp.233-271, 1871.

N. Asokan, C. Gülcü, and G. Karjoth, Protecting the computation results of free-roaming agents, Proceedings of the 2nd International Workshop on Mobile Agents, Lecture Notes in Computer Science 1477, 1998.

G. Bella and L. Paulson, Kerberos Version IV: Inductive analysis of the secrecy goals, Proceedings of the 5th European Symposium on Research in Computer Security, Lecture Notes in Computer Science 1485, 1998.
DOI : 10.1007/BFb0055875

L. Buttyán, S. Staamann, and U. Wilhelm, Introducing trusted third parties to the mobile agent paradigm, Proceedings of the 4th ECOOP Workshop on Mobile Object Systems, Lecture Notes in Computer Science 1603, 1998.

G. , D. Caro, and M. Dorigo, Mobile agents for adaptive routing, Proceedings of the 31st Hawaii International Conference on System Sciences, 1998.

E. Cohen, TAPS: a first-order verifier for cryptographic protocols, Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000.
DOI : 10.1109/csfw.2000.856933

V. Cortier, J. Millen, and H. Rueß, Proving secrecy is easy enough, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001.
DOI : 10.1109/CSFW.2001.930139

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, Undecidability of bounded security protocols, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.

J. Guttman, J. Herzog, and J. Thayer, Honest ideals on strand spaces, Proceedings of the 11th IEEE Computer Security Foundations Workshop, 1998.

J. Guttman, J. Herzog, and J. Thayer, Strand spaces: Why is a security protocol correct?, Proceedings of the IEEE Symposium on Security and Privacy, 1998.

J. Guttman, J. Thayer, and L. Zuck, The faithfulness of abstract protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, 2001.
DOI : 10.1145/501983.502009

P. Lee and G. Necula, Research on proof-carrying code for mobile-code security, DARPA Workshop on Foundations for Secure Mobile Code, 1997.

G. Lowe, Towards a completeness result for model checking of security protocols, Proceedings of the 11th IEEE Computer Security Foundations Workshop, 1998.

G. Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, vol.56, issue.3, pp.131-133, 1995.
DOI : 10.1016/0020-0190(95)00144-2

J. Millen and H. Rueß, Protocol-independent secrecy, Proceeding 2000 IEEE Symposium on Security and Privacy. S&P 2000, 2000.
DOI : 10.1109/SECPRI.2000.848449

J. Millen and H. Rueß, Local secrecy for stated-based models, Workshop on Formal Methods in Computer Security, 2000.

R. Needham and M. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-998, 1978.
DOI : 10.1145/359657.359659

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2002.
DOI : 10.1007/3-540-45949-9

D. Otway and O. Rees, Efficient and timely mutual authentication, ACM SIGOPS Operating Systems Review, vol.21, issue.1, pp.8-10, 1987.
DOI : 10.1145/24592.24594

L. Paulson, Verifying the SET protocol, Proceedings of the 1st International Joint Conference on Automated Reasoning, 2001.

L. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, vol.6, issue.1-2, pp.85-128, 1998.
DOI : 10.3233/JCS-1998-61-205

L. Paulson, Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security, vol.2, issue.3, pp.332-351, 1999.
DOI : 10.1145/322510.322530

L. Paulson, Relations between secrets: two formal analyses of the Yahalom protocol, Journal of Computer Security, vol.9, issue.3, pp.197-216, 2001.
DOI : 10.3233/JCS-2001-9302

N. Shankar, PVS: Combining specification, proof checking, and model checking, Proceedings of the 1st International Conference on Formal Methods in Computer- Aided Design, 1996.
DOI : 10.1007/BFb0031813

D. Song, D. Wagner, and X. Tian, Timing analysis of keystrokes and timing attacks on SSH, Proceedings of the 10th USENIX Security Symposium, 2001.

B. Yee, A Sanctuary for Mobile Agents, Proceedings of the 4th ECOOP Workshop on Mobile Object Systems, Lecture Notes in Computer Science 1603, 1998.
DOI : 10.1007/3-540-48749-2_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.280