|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
Ninth IEEE Computer Security Foundations Workshop
A HOL extension of GNY for automatically analyzing cryptographic protocols
Dromquinna Manor, Kenmare, County Kerry, Ireland
March 10-March 12
ISBN: 0-8186-7522-5
| ASCII Text | x | ||
| S.H. Brackin, "A HOL extension of GNY for automatically analyzing cryptographic protocols," Computer Security Foundations Workshop, IEEE, pp. 62, Ninth IEEE Computer Security Foundations Workshop, 1996. | |||
| BibTex | x | ||
| @article{ 10.1109/CSFW.1996.503691, author = {S.H. Brackin}, title = {A HOL extension of GNY for automatically analyzing cryptographic protocols}, journal ={Computer Security Foundations Workshop, IEEE}, volume = {0}, year = {1996}, issn = {1063-6900}, pages = {62}, doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1996.503691}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Computer Security Foundations Workshop, IEEE TI - A HOL extension of GNY for automatically analyzing cryptographic protocols SN - 1063-6900 SP EP A1 - S.H. Brackin, PY - 1996 KW - message authentication; cryptography; access protocols; belief maintenance; formal specification; HOL extension; automatically analyzing cryptographic protocols; higher order logic theory; belief logic; authentication properties; protocol properties; multiple encryption; hash operations; message authentication codes; key-exchange algorithms VL - 0 JA - Computer Security Foundations Workshop, IEEE ER - | |||
This paper describes a Higher Order Logic (HOL) theory formalizing an extended version of the Gong, Needham, Yahalom (GNY) belief logic, a theory used by software that automatically proves authentication properties of cryptographic protocols. The theory's extensions to the GNY logic include being able to specify protocol properties at intermediate stages and being able to specify protocols that use multiple encryption and hash operations, message authentication codes, computed values (e.g., hash codes) as keys, and key-exchange algorithms.
Index Terms:
message authentication; cryptography; access protocols; belief maintenance; formal specification; HOL extension; automatically analyzing cryptographic protocols; higher order logic theory; belief logic; authentication properties; protocol properties; multiple encryption; hash operations; message authentication codes; key-exchange algorithms
Citation:
S.H. Brackin, "A HOL extension of GNY for automatically analyzing cryptographic protocols," csfw, pp.62, Ninth IEEE Computer Security Foundations Workshop, 1996
Usage of this product signifies your acceptance of the Terms of Use.