This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
25th IEEE International Conference on Distributed Computing Systems (ICDCS'05)
Equational Approach to Formal Analysis of TLS
Columbus, Ohio, USA
June 06-June 10
ISBN: 0-7695-2331-5
ASCII Text
x 
 
Kazuhiro Ogata, Kokichi Futatsugi, "Equational Approach to Formal Analysis of TLS," 2012 IEEE 32nd International Conference on Distributed Computing Systems, pp. 795-804, 25th IEEE International Conference on Distributed Computing Systems (ICDCS'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/ICDCS.2005.32,
author = {Kazuhiro Ogata and Kokichi Futatsugi},
title = {Equational Approach to Formal Analysis of TLS},
journal ={2012 IEEE 32nd International Conference on Distributed Computing Systems},
volume = {0},
year = {2005},
issn = {1063-6927},
pages = {795-804},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICDCS.2005.32},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - 2012 IEEE 32nd International Conference on Distributed Computing Systems
TI - Equational Approach to Formal Analysis of TLS
SN - 1063-6927
SP795
EP804
A1 - Kazuhiro Ogata,
A1 - Kokichi Futatsugi,
PY - 2005
KW - algebraic specification
KW - interactive theorem proving
KW - security
KW - rewriting
KW - verification
VL - 0
JA - 2012 IEEE 32nd International Conference on Distributed Computing Systems
ER -
 
Kazuhiro Ogata, NEC Software Hokuriku, Ltd.
Kokichi Futatsugi, Japan Advanced Institute of Science and Technology
TLS has been formally analyzed with the OTS/CafeOBJ method. In the method, distributed systems are modeled as transition systems, which are written in terms of equations, and it is verified that the models have properties by means of equational reasoning. TLS is the latest version, or the successor of SSL, which is probably the most widely deployed security protocol. Among the results of the analysis are that pre-master secrets cannot be leaked, when a client has negotiated a cipher suite and security parameters with a server, the server has really agreed on them, and client cannot be identified if they do not send their certificates to servers.
Index Terms:
algebraic specification, interactive theorem proving, security, rewriting, verification
Citation:
Kazuhiro Ogata, Kokichi Futatsugi, "Equational Approach to Formal Analysis of TLS," icdcs, pp.795-804, 25th IEEE International Conference on Distributed Computing Systems (ICDCS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.