The DH exponentiation extension in a verification logic of local sessions

Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can...

Full description

Saved in:
Bibliographic Details
Main Authors: Yinyin Xiao, Kaile Su
Format: Conference Proceeding
Language:English
Subjects:
Computational modeling
DH-HEMTs
Diffie-Hellman symmetric encryption
Encryption
formal verification
Logic of Local Sessions
Protocols
security protocol
Semantics
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page 503
container_issue
container_start_page 499
container_title
container_volume 1
creator Yinyin Xiao
Kaile Su
description Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can verify many interesting properties for complex security protocols. However, It does not discuss the DH key exchange and the related properties. In this paper, we extend the original LLS with DH exponentiation. After revising some primary concepts and definitions, a new theorem called DH-Secrecy Properties is proposed and proved. Avoiding influencing the proof of the former axioms, our extension enlarges the range of applicability of LLS.
doi_str_mv 10.1109/CSAE.2012.6272646
format conference_proceeding
fullrecord <record><control><sourceid>ieee_6IE</sourceid><recordid>TN_cdi_ieee_primary_6272646</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>6272646</ieee_id><sourcerecordid>6272646</sourcerecordid><originalsourceid>FETCH-LOGICAL-i90t-455151d4e80855fd19441f608c046a5e31c1d6a0232e99d14f6be5d85256b44d3</originalsourceid><addsrcrecordid>eNo1j8FOwzAQRI0QElDyAYiLfyBh17Ed-1iFQitV4kDulRuvwSgkVRwh-HtStexlZ2afVhrG7hEKRLCP9dtyVQhAUWhRCS31BctsZVDqqgQwVl-y239jzDXLUvqEeWZkDm7Ypvkg_rTm9HMYeuqn6KY49LOdqE9HFXvu-DeNMcT2dOuG99jyIcyidR1PlI5gumNXwXWJsvNesOZ51dTrfPv6sqmX2zxamHKpFCr0kgwYpYJHKyUGDaYFqZ2iElv02oEoBVnrUQa9J-WNEkrvpfTlgj2c3kYi2h3G-OXG3925fPkHStpMjg</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>The DH exponentiation extension in a verification logic of local sessions</title><source>IEEE Electronic Library (IEL) Conference Proceedings</source><creator>Yinyin Xiao ; Kaile Su</creator><creatorcontrib>Yinyin Xiao ; Kaile Su</creatorcontrib><description>Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can verify many interesting properties for complex security protocols. However, It does not discuss the DH key exchange and the related properties. In this paper, we extend the original LLS with DH exponentiation. After revising some primary concepts and definitions, a new theorem called DH-Secrecy Properties is proposed and proved. Avoiding influencing the proof of the former axioms, our extension enlarges the range of applicability of LLS.</description><identifier>ISBN: 1467300888</identifier><identifier>ISBN: 9781467300889</identifier><identifier>EISBN: 9781467300896</identifier><identifier>EISBN: 1467300896</identifier><identifier>EISBN: 9781467300872</identifier><identifier>EISBN: 146730087X</identifier><identifier>DOI: 10.1109/CSAE.2012.6272646</identifier><language>eng</language><publisher>IEEE</publisher><subject>Computational modeling ; DH-HEMTs ; Diffie-Hellman symmetric encryption ; Encryption ; formal verification ; Logic of Local Sessions ; Protocols ; security protocol ; Semantics</subject><ispartof>2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE), 2012, Vol.1, p.499-503</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/6272646$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,2057,27924,54919</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/6272646$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Yinyin Xiao</creatorcontrib><creatorcontrib>Kaile Su</creatorcontrib><title>The DH exponentiation extension in a verification logic of local sessions</title><title>2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE)</title><addtitle>CSAE</addtitle><description>Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can verify many interesting properties for complex security protocols. However, It does not discuss the DH key exchange and the related properties. In this paper, we extend the original LLS with DH exponentiation. After revising some primary concepts and definitions, a new theorem called DH-Secrecy Properties is proposed and proved. Avoiding influencing the proof of the former axioms, our extension enlarges the range of applicability of LLS.</description><subject>Computational modeling</subject><subject>DH-HEMTs</subject><subject>Diffie-Hellman symmetric encryption</subject><subject>Encryption</subject><subject>formal verification</subject><subject>Logic of Local Sessions</subject><subject>Protocols</subject><subject>security protocol</subject><subject>Semantics</subject><isbn>1467300888</isbn><isbn>9781467300889</isbn><isbn>9781467300896</isbn><isbn>1467300896</isbn><isbn>9781467300872</isbn><isbn>146730087X</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2012</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNo1j8FOwzAQRI0QElDyAYiLfyBh17Ed-1iFQitV4kDulRuvwSgkVRwh-HtStexlZ2afVhrG7hEKRLCP9dtyVQhAUWhRCS31BctsZVDqqgQwVl-y239jzDXLUvqEeWZkDm7Ypvkg_rTm9HMYeuqn6KY49LOdqE9HFXvu-DeNMcT2dOuG99jyIcyidR1PlI5gumNXwXWJsvNesOZ51dTrfPv6sqmX2zxamHKpFCr0kgwYpYJHKyUGDaYFqZ2iElv02oEoBVnrUQa9J-WNEkrvpfTlgj2c3kYi2h3G-OXG3925fPkHStpMjg</recordid><startdate>201205</startdate><enddate>201205</enddate><creator>Yinyin Xiao</creator><creator>Kaile Su</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>201205</creationdate><title>The DH exponentiation extension in a verification logic of local sessions</title><author>Yinyin Xiao ; Kaile Su</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i90t-455151d4e80855fd19441f608c046a5e31c1d6a0232e99d14f6be5d85256b44d3</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2012</creationdate><topic>Computational modeling</topic><topic>DH-HEMTs</topic><topic>Diffie-Hellman symmetric encryption</topic><topic>Encryption</topic><topic>formal verification</topic><topic>Logic of Local Sessions</topic><topic>Protocols</topic><topic>security protocol</topic><topic>Semantics</topic><toplevel>online_resources</toplevel><creatorcontrib>Yinyin Xiao</creatorcontrib><creatorcontrib>Kaile Su</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Electronic Library (IEL)</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Yinyin Xiao</au><au>Kaile Su</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>The DH exponentiation extension in a verification logic of local sessions</atitle><btitle>2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE)</btitle><stitle>CSAE</stitle><date>2012-05</date><risdate>2012</risdate><volume>1</volume><spage>499</spage><epage>503</epage><pages>499-503</pages><isbn>1467300888</isbn><isbn>9781467300889</isbn><eisbn>9781467300896</eisbn><eisbn>1467300896</eisbn><eisbn>9781467300872</eisbn><eisbn>146730087X</eisbn><abstract>Diffie-Hellman (DH) symmetric encryption plays an important role in the network security, and the security proof for many protocols relies on the DH assumption. The Logic of Local Sessions (LLS) is a practical security protocol logic. With its automatic tool Security Protocol Verifier (SPV), LLS can verify many interesting properties for complex security protocols. However, It does not discuss the DH key exchange and the related properties. In this paper, we extend the original LLS with DH exponentiation. After revising some primary concepts and definitions, a new theorem called DH-Secrecy Properties is proposed and proved. Avoiding influencing the proof of the former axioms, our extension enlarges the range of applicability of LLS.</abstract><pub>IEEE</pub><doi>10.1109/CSAE.2012.6272646</doi><tpages>5</tpages></addata></record>
fulltext fulltext_linktorsrc
identifier ISBN: 1467300888
ispartof 2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE), 2012, Vol.1, p.499-503
issn
language eng
recordid cdi_ieee_primary_6272646
source IEEE Electronic Library (IEL) Conference Proceedings
subjects Computational modeling
DH-HEMTs
Diffie-Hellman symmetric encryption
Encryption
formal verification
Logic of Local Sessions
Protocols
security protocol
Semantics
title The DH exponentiation extension in a verification logic of local sessions
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-08T21%3A03%3A45IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_6IE&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=The%20DH%20exponentiation%20extension%20in%20a%20verification%20logic%20of%20local%20sessions&rft.btitle=2012%20IEEE%20International%20Conference%20on%20Computer%20Science%20and%20Automation%20Engineering%20(CSAE)&rft.au=Yinyin%20Xiao&rft.date=2012-05&rft.volume=1&rft.spage=499&rft.epage=503&rft.pages=499-503&rft.isbn=1467300888&rft.isbn_list=9781467300889&rft_id=info:doi/10.1109/CSAE.2012.6272646&rft.eisbn=9781467300896&rft.eisbn_list=1467300896&rft.eisbn_list=9781467300872&rft.eisbn_list=146730087X&rft_dat=%3Cieee_6IE%3E6272646%3C/ieee_6IE%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i90t-455151d4e80855fd19441f608c046a5e31c1d6a0232e99d14f6be5d85256b44d3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=6272646&rfr_iscdi=true