Title :
Provable Implementations of Security Protocols
Author :
Gordon, Andrew D.
Author_Institution :
Microsoft Research
Abstract :
The author implements the relatively new enterprise of adapting formal methods for security to work on code instead of abstract models. The goal is to lower the practical cost of security protocol verification by eliminating the need to write a separate formal model. The main technical content is on extracting pi-calculus models from protocol implementation code. Our software is developed in the functional language F#, a dialect of ML
Keywords :
ML language; cryptography; formal verification; pi calculus; protocols; ML language; cryptographic protocol; formal methods; functional language; pi-calculus; security protocol verification; Algorithm design and analysis; Automation; Computational modeling; Computer languages; Computer security; Cryptographic protocols; Cryptography; Design methodology; Information security; Robustness;
Conference_Titel :
Logic in Computer Science, 2006 21st Annual IEEE Symposium on
Conference_Location :
Seattle, WA
Print_ISBN :
0-7695-2631-4
DOI :
10.1109/LICS.2006.43
