TY - GEN
T1 - Modular Verification of Sequential Composition for Private Channels in Maude-NPA
AU - Yang, Fan
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
N1 - Publisher Copyright:
© 2018, Springer Nature Switzerland AG.
PY - 2018
Y1 - 2018
N2 - This paper gives a modular verification methodology in which, given parametric specifications of a key establishment protocol P and a protocol Q providing private channel communication, security and authenticity properties of their sequential composition $$P\;;\; Q$$ can be reduced to: (i) verification of corresponding properties for P, and (ii) verification of corresponding properties for an abstract version $$Q^\alpha $$ of Q in which keys have been suitably abstracted. Our results improve upon previous work in this area in several ways. First of all, we both support a large class of equational theories and provide tool support via the Maude-NPA cryptographic protocol analysis tool. Secondly as long as certain conditions on P and Q guaranteeing the secrecy of keys inherited by Q from P are satisfied, our results apply to the composition of any two reachability properties of the two protocols.
AB - This paper gives a modular verification methodology in which, given parametric specifications of a key establishment protocol P and a protocol Q providing private channel communication, security and authenticity properties of their sequential composition $$P\;;\; Q$$ can be reduced to: (i) verification of corresponding properties for P, and (ii) verification of corresponding properties for an abstract version $$Q^\alpha $$ of Q in which keys have been suitably abstracted. Our results improve upon previous work in this area in several ways. First of all, we both support a large class of equational theories and provide tool support via the Maude-NPA cryptographic protocol analysis tool. Secondly as long as certain conditions on P and Q guaranteeing the secrecy of keys inherited by Q from P are satisfied, our results apply to the composition of any two reachability properties of the two protocols.
UR - http://www.scopus.com/inward/record.url?scp=85054867665&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85054867665&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-01141-3_2
DO - 10.1007/978-3-030-01141-3_2
M3 - Conference contribution
AN - SCOPUS:85054867665
SN - 9783030011406
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 20
EP - 36
BT - Security and Trust Management - 14th International Workshop, STM 2018, Proceedings
A2 - Alcaraz, Cristina
A2 - Katsikas, Sokratis K.
A2 - Katsikas, Sokratis K.
PB - Springer
T2 - 14th International Workshop on Security and Trust Management, STM 2018
Y2 - 6 September 2018 through 7 September 2018
ER -