谁能帮忙翻译一下啊，不要求很对，只要求通顺，关于C#的【计算机专业英语在线翻译吧】

Automatic Generation of the C# Code for Security Protocols Verified with Casper/FDR
Chul-Wuk Jeon, Il-Gon Kim, Jin-Young Choi
Dept. of Computer Science and Engineering, Korea University, Seoul, 136-701 KOREA
{cwjeon, igkim, choi}@formal.korea.ac.kr
Abstract
     Formal methods technique offer a means of verifying the correctness of the design process used to create the security protocol. Notwithstanding the successful verification of the design of security protocols, the implementation code for them may contain security flaws, due to the mistakes made by the programmers or bugs in the programming language itself. We propose an ACG-C# tool, which can be used to generate automatically C# implementation code for the security protocol verified with Casper and FDR. The ACG-C# approach has several different features, namely automatic code generation, secure code, and high confidence. We conduct a case study on the Yahalom security protocol, using ACG-C # to generate the C# implementation code.
1 Introduction
     With the rapid development of communication networks, the use of security protocols to achieve security goals such as confidentiality, authentication, integrity and nonrepudiation is becoming more and more popular. However, many supposedly inviolable security protocols have been proposed in the literature and even exploited in practice, only to be found to be vulnerable later on. Therefore, various formal methods have been developed to verify the safety of security protocols. These include belief logics such as BAN[1] and various tools such as FDR, Murphi, NRL Analyzer, and Isabelle[2].
     Notwithstanding the successful verification of the design of security protocols, the implementation code for them may contain security flaws, due to the mistakes made by the programmers or bugs in the programming language itself. In addition, the process of implementing a security protocol is a tedious and time-consuming task. For example, a flaw pertaining to a buffer overflow attack was found in the OpenSSH code of the SSH protocol[3]. This vulnerability did not concern the security protocol itself, but its imperfect implementation.
     Accordingly, research into the generation of the program code automatically from a high-level specification of a security protocol is necessary, in order to reduce such vulnerabilities in the implementation phase. If the design of the security protocol is found to be correct, the use of automated translation guarantees that the behavior of the implementation code corresponds precisely to the formal specification.
In this paper, we propose an ACG-C# tool, which can be used to generate automatically the C# implementation code for security protocols from the high-level specification written in a variation of Casper notation. This ACG-C# tool compiles the specification to produce C# code that is a concrete implementation of the protocol.
The remainder of this paper is organized as follows. Section 2 provides a brief overview of Casper notation. Section 3 introduce the notation, the process of code generation, architecture, API of the ACG-C# tool and the advantages of our approach. Finally, section 4 concludes this paper.

送TA礼物

1楼2010-03-28 15:47回复

3.3 Architecture
ACG-C# separates the implementation of the protocol notation from that of the network communications and cryptographic algorithms.
Figure 4. Protocol notation from ACG-C# to C# code
• Protocol notation - this part of the architecture is related to the “#Protocol description” section in Casper script. This code maintains the protocol state, determines when and if messages are sent and received, checks the contents of the outgoing messages and the incoming messages, as well as stores the message components.
     In Figure 4, the “#Protocol description” section in Casper script, the desired security protocol is separated into two agents for the sake of computer networking. Agent a creates the new nonce, na and then sends it. Agent b receives nonce, na. Similarly, Agent b encrypts the received nonce with RSA encryption algorithm and then sends it.
•Secret and Communication Provider(SCP) - this part of the architecture involves provider specific code that handles the concatenating and separating of message components into the byte stream, implements the cryptographic algorithms, and manages the network protocol specific aspects. The Secret and Communication Provider forms the common base when the C# implementation code is running.
3.4 SCP(Secret and Communication Provider)API
     SCP API provides the C# implementation code with runtime access to the Secret and Communication library. The agent class provides the functions required for the two agents to communicate with each other. The agent classcontains the agent’s ID, IP, socket, and opponent fields. The ID field represents the identity of the agent as it is used in the protocol description section of the input script. The IP field is the IP address which the agent uses for computer networking. Socket is an instance of the class socket that is used to communicate with the agent. The opponent can get the IP address that the agent uses to communicate with another agent. The message class represents the messages sent and received during communication. The message class deals with operations involving the message's contents, such as encryption, decryption, and so on. The message class includes the encrypt method, decrypt method, hash method, and addMessage method.
     The generated C# implementation code uses the protocol class method. The protocol class uses a design patttern, abstract factory, which allows different providers to be plugged into the SCP API. It provides the Protocol notation code with a single point of access to instances of the concrete provider classes that are used to implement the SCP API defined interfaces, and the cryptographic and network operations.
Compared with COSP-J, the entire architecture is changed due to the features of the C # language. In ACG-C#, the class, MessageT, which is itself composed of the class Message, is used to implement the interface IMessage. This architecture can easily be extended by changing the classMessage.

4楼2010-03-28 17:16

北京百度网讯科技有限公司

专业移民顾问和详尽的移民政策咨询全程指导和支持，包括移民手续的办理和居住地的适应问题

2025-03-21 09:07广告

立即查看

3.5 Advantages
• No error-prone : If the programmer is inexperienced, the security protocol is likely to be flawed. ACG-C# precludes the possibility of the programmer making such mistakes. Furthermore, the ACG-C# tool helps the programmer to reduce tedious and time-consuming tasks.
• Secure code : With the managed code in C#, the CLR(Common Language Runtime) can perform checks for type safety, memory overwrites, memory management, and garbage collection. This results in a reduction of memory leaks and related issues. The CLR performing the memory management prevents the code from buffer overflow, accessing memory directly, eliminating pointers, and greatly reducing crashes or other memory-overwrite behaviors.
• High confidence : Using the well-defined Casper script can provide guarantees that the desired security properties are satisfied, thus imparting high confidence.
• Strong key : People tend to choose their passwords poorly[6]. To prevent guessing attacks, a good random number generator is needed. The key generator generates DES keys which have 108 possible variations and keys are saved in an XML file.
4 Conclusion
The security protocol implementation process can cause difficulties, due to; a lack of expertise and experience on the part of the programmer and bugs in the implementation language, which lead to the implemented security protocols behaving incorrectly. The automatic code generation approach not only eliminates these shortcomings, but offers several advantages, such as its automatic code generation, type safety, and high confidence. Using Casper provides the designer with high confidence and high quality in terms of the analysis of the security protocol. Once the security protocol has been verified with Casper/FDR, the ACG-C# tool generates the C# implementation code. This code is guaranteed to be free of designer induced buffer overflow, memory leaks, and type-flaw attacks. We believe that using formal methods and the automatic code implementation approach is the efficient way to guarantee the safety of security protocols in the design and the implementation steps.
References
[1] M.Burrows, M.Abadi, and R.Needham. A Logic of Authentication. ACM Transactions on Computer Systems, pp.18-36, 1990.
[2] P.Y.A. Ryan and S. A, Schneider. Modeling and analysis of security protocols: the CSP Approach. Addison-Wesley, 2001.
[3] M.Zalewski. Remote vulnerability in SSH daemon crc32 compensation attack detector. Available from
http://razor.bindview.com/publish/advisories/adv_ssh1_crc.html, 2001.
[4] X.Didelot. COSP-J: A Compiler for Security Protocols. MSc dissertation, Available from
http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/COSPJ/, 2003.
[5] K.Shakil. Security Features inC#, The article, Available from
http://www.developersdex.com/gurus/articles/5.asp,2004.
[6] Gavin Lowe. Analysing Protocols Subject to GuessingAttacks. Journal of Computer Security, 2004.

5楼2010-03-28 17:16

3.3 Architecture
ACG-C# separates the implementation of the protocol notation from that of the network communications and cryptographic algorithms.
Figure 4. Protocol notation from ACG-C# to C# code
• Protocol notation - this part of the architecture is related to the “#Protocol description” section in Casper script. This code maintains the protocol state, determines when and if messages are sent and received, checks the contents of the outgoing messages and the incoming messages, as well as stores the message components.
     In Figure 4, the “#Protocol description” section in Casper script, the desired security protocol is separated into two agents for the sake of computer networking. Agent a creates the new nonce, na and then sends it. Agent b receives nonce, na. Similarly, Agent b encrypts the received nonce with RSA encryption algorithm and then sends it.
•Secret and Communication Provider(SCP) - this part of the architecture involves provider specific code that handles the concatenating and separating of message components into the byte stream, implements the cryptographic algorithms, and manages the network protocol specific aspects. The Secret and Communication Provider forms the common base when the C# implementation code is running.
3.4 SCP(Secret and Communication Provider)API
     SCP API provides the C# implementation code with runtime access to the Secret and Communication library. The agent class provides the functions required for the two agents to communicate with each other. The agent classcontains the agent’s ID, IP, socket, and opponent fields. The ID field represents the identity of the agent as it is used in the protocol description section of the input script. The IP field is the IP address which the agent uses for computer networking. Socket is an instance of the class socket that is used to communicate with the agent. The opponent can get the IP address that the agent uses to communicate with another agent. The message class represents the messages sent and received during communication. The message class deals with operations involving the message's contents, such as encryption, decryption, and so on. The message class includes the encrypt method, decrypt method, hash method, and addMessage method.
     The generated C# implementation code uses the protocol class method. The protocol class uses a design patttern, abstract factory, which allows different providers to be plugged into the SCP API. It provides the Protocol notation code with a single point of access to instances of the concrete provider classes that are used to implement the SCP API defined interfaces, and the cryptographic and network operations.
Compared with COSP-J, the entire architecture is changed due to the features of the C # language. In ACG-C#, the class, MessageT, which is itself composed of the class Message, is used to implement the interface IMessage. This architecture can easily be extended by changing the classMessage.

6楼2010-03-28 17:16

3.5 Advantages
• No error-prone : If the programmer is inexperienced, the security protocol is likely to be flawed. ACG-C# precludes the possibility of the programmer making such mistakes. Furthermore, the ACG-C# tool helps the programmer to reduce tedious and time-consuming tasks.
• Secure code : With the managed code in C#, the CLR(Common Language Runtime) can perform checks for type safety, memory overwrites, memory management, and garbage collection. This results in a reduction of memory leaks and related issues. The CLR performing the memory management prevents the code from buffer overflow, accessing memory directly, eliminating pointers, and greatly reducing crashes or other memory-overwrite behaviors.
• High confidence : Using the well-defined Casper script can provide guarantees that the desired security properties are satisfied, thus imparting high confidence.
• Strong key : People tend to choose their passwords poorly[6]. To prevent guessing attacks, a good random number generator is needed. The key generator generates DES keys which have 108 possible variations and keys are saved in an XML file.
4 Conclusion
The security protocol implementation process can cause difficulties, due to; a lack of expertise and experience on the part of the programmer and bugs in the implementation language, which lead to the implemented security protocols behaving incorrectly. The automatic code generation approach not only eliminates these shortcomings, but offers several advantages, such as its automatic code generation, type safety, and high confidence. Using Casper provides the designer with high confidence and high quality in terms of the analysis of the security protocol. Once the security protocol has been verified with Casper/FDR, the ACG-C# tool generates the C# implementation code. This code is guaranteed to be free of designer induced buffer overflow, memory leaks, and type-flaw attacks. We believe that using formal methods and the automatic code implementation approach is the efficient way to guarantee the safety of security protocols in the design and the implementation steps.
References
[1] M.Burrows, M.Abadi, and R.Needham. A Logic of Authentication. ACM Transactions on Computer Systems, pp.18-36, 1990.
[2] P.Y.A. Ryan and S. A, Schneider. Modeling and analysis of security protocols: the CSP Approach. Addison-Wesley, 2001.
[3] M.Zalewski. Remote vulnerability in SSH daemon crc32 compensation attack detector. Available from
http://razor.bindview.com/publish/advisories/adv_ssh1_crc.html, 2001.
[4] X.Didelot. COSP-J: A Compiler for Security Protocols. MSc dissertation, Available from
http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/COSPJ/, 2003.
[5] K.Shakil. Security Features inC#, The article, Available from
http://www.developersdex.com/gurus/articles/5.asp,2004.
[6] Gavin Lowe. Analysing Protocols Subject to GuessingAttacks. Journal of Computer Security, 2004.

7楼2010-03-28 17:16

3.3 Architecture
ACG-C# separates the implementation of the protocol notation from that of the network communications and cryptographic algorithms.
Figure 4. Protocol notation from ACG-C# to C# code
• Protocol notation - this part of the architecture is related to the “#Protocol description” section in Casper script. This code maintains the protocol state, determines when and if messages are sent and received, checks the contents of the outgoing messages and the incoming messages, as well as stores the message components.
     In Figure 4, the “#Protocol description” section in Casper script, the desired security protocol is separated into two agents for the sake of computer networking. Agent a creates the new nonce, na and then sends it. Agent b receives nonce, na. Similarly, Agent b encrypts the received nonce with RSA encryption algorithm and then sends it.
•Secret and Communication Provider(SCP) - this part of the architecture involves provider specific code that handles the concatenating and separating of message components into the byte stream, implements the cryptographic algorithms, and manages the network protocol specific aspects. The Secret and Communication Provider forms the common base when the C# implementation code is running.
3.4 SCP(Secret and Communication Provider)API
     SCP API provides the C# implementation code with runtime access to the Secret and Communication library. The agent class provides the functions required for the two agents to communicate with each other. The agent classcontains the agent’s ID, IP, socket, and opponent fields. The ID field represents the identity of the agent as it is used in the protocol description section of the input script. The IP field is the IP address which the agent uses for computer networking. Socket is an instance of the class socket that is used to communicate with the agent. The opponent can get the IP address that the agent uses to communicate with another agent. The message class represents the messages sent and received during communication. The message class deals with operations involving the message's contents, such as encryption, decryption, and so on. The message class includes the encrypt method, decrypt method, hash method, and addMessage method.
     The generated C# implementation code uses the protocol class method. The protocol class uses a design patttern, abstract factory, which allows different providers to be plugged into the SCP API. It provides the Protocol notation code with a single point of access to instances of the concrete provider classes that are used to implement the SCP API defined interfaces, and the cryptographic and network operations.
Compared with COSP-J, the entire architecture is changed due to the features of the C # language. In ACG-C#, the class, MessageT, which is itself composed of the class Message, is used to implement the interface IMessage. This architecture can easily be extended by changing the classMessage.

9楼2010-03-28 17:22

3.5 Advantages
• No error-prone : If the programmer is inexperienced, the security protocol is likely to be flawed. ACG-C# precludes the possibility of the programmer making such mistakes. Furthermore, the ACG-C# tool helps the programmer to reduce tedious and time-consuming tasks.
• Secure code : With the managed code in C#, the CLR(Common Language Runtime) can perform checks for type safety, memory overwrites, memory management, and garbage collection. This results in a reduction of memory leaks and related issues. The CLR performing the memory management prevents the code from buffer overflow, accessing memory directly, eliminating pointers, and greatly reducing crashes or other memory-overwrite behaviors.
• High confidence : Using the well-defined Casper script can provide guarantees that the desired security properties are satisfied, thus imparting high confidence.
• Strong key : People tend to choose their passwords poorly[6]. To prevent guessing attacks, a good random number generator is needed. The key generator generates DES keys which have 108 possible variations and keys are saved in an XML file.
4 Conclusion
The security protocol implementation process can cause difficulties, due to; a lack of expertise and experience on the part of the programmer and bugs in the implementation language, which lead to the implemented security protocols behaving incorrectly. The automatic code generation approach not only eliminates these shortcomings, but offers several advantages, such as its automatic code generation, type safety, and high confidence. Using Casper provides the designer with high confidence and high quality in terms of the analysis of the security protocol. Once the security protocol has been verified with Casper/FDR, the ACG-C# tool generates the C# implementation code. This code is guaranteed to be free of designer induced buffer overflow, memory leaks, and type-flaw attacks. We believe that using formal methods and the automatic code implementation approach is the efficient way to guarantee the safety of security protocols in the design and the implementation steps.
References
[1] M.Burrows, M.Abadi, and R.Needham. A Logic of Authentication. ACM Transactions on Computer Systems, pp.18-36, 1990.
[2] P.Y.A. Ryan and S. A, Schneider. Modeling and analysis of security protocols: the CSP Approach. Addison-Wesley, 2001.
[3] M.Zalewski. Remote vulnerability in SSH daemon crc32 compensation attack detector. Available from
http://razor.bindview.com/publish/advisories/adv_ssh1_crc.html, 2001.
[4] X.Didelot. COSP-J: A Compiler for Security Protocols. MSc dissertation, Available from
http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Security/Casper/COSPJ/, 2003.
[5] K.Shakil. Security Features inC#, The article, Available from
http://www.developersdex.com/gurus/articles/5.asp,2004.
[6] Gavin Lowe. Analysing Protocols Subject to GuessingAttacks. Journal of Computer Security, 2004.

10楼2010-03-28 17:22

日	一	二	三	四	五	六

谁能帮忙翻译一下啊，不要求很对，只要求通顺，关于C#的

登录百度账号

扫二维码下载贴吧客户端