Title
Automatic Generation of the C# Code for Security Protocols Verified with Casper/FDR
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.
Year
DOI
Venue
2005
10.1109/AINA.2005.128
AINA
Keywords
Field
DocType
security flaw,yahalom security protocol,secure code,automatic code generation,automatic generation,formal methods technique offer,different feature,design process,security protocol,implementation code,case study,formal methods,formal method,security protocols,computer security,computer bugs,protocols,communication networks,process design,authentication,programming language,computer science,computer languages
Programming language,Cryptographic protocol,Computer science,Correctness,Code generation,Engineering design process,Formal methods,Automatic programming
Conference
ISBN
Citations 
PageRank 
0-7695-2249-1
10
0.54
References 
Authors
2
3
Name
Order
Citations
PageRank
Chul-Wuk Jeon1100.54
Il-gon Kim2245.91
Jin Young Choi376899.57