{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:42:23Z","timestamp":1773247343826,"version":"3.50.1"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030916305","type":"print"},{"value":"9783030916312","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T00:00:00Z","timestamp":1637280000000},"content-version":"vor","delay-in-days":322,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Cryptographic Protocol Shapes Analyzer <jats:sc>cpsa<\/jats:sc> determines if a cryptographic protocol achieves authentication and secrecy goals. It can be difficult to ensure that an implementation of a protocol matches up with what <jats:sc>cpsa<\/jats:sc> analyzed, and therefore be sure the implementation achieves the security goals determined by <jats:sc>cpsa<\/jats:sc>.<\/jats:p><jats:p>Roletran is a program distributed with <jats:sc>cpsa<\/jats:sc> that translates a role in a protocol into a language independent description of a procedure that is easily translated into an existing computer language. This paper shows how we ensure the procedure produced by Roletran is faithful to strand space semantics and therefore achieves the security goals determined by <jats:sc>cpsa<\/jats:sc>.<\/jats:p><jats:p>Real implementations of cryptographic functions make use of probabilistic encryption, but <jats:sc>cpsa<\/jats:sc> will conclude that two encryptions are the same if they are constructed with the same plaintext and key. The paper concludes by showing how we ensure that executions of generated code that make use of probabilistic encryption achieve the goals determined by <jats:sc>cpsa<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/978-3-030-91631-2_20","type":"book-chapter","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T21:02:24Z","timestamp":1637269344000},"page":"355-369","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5547-0427","authenticated-orcid":false,"given":"John D.","family":"Ramsdell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,19]]},"reference":[{"key":"20_CR1","unstructured":"The Coq proof assistant reference manual (2021). http:\/\/coq.inria.fr"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, 8\u201310 July 2009, pp. 124\u2013140. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/CSF.2009.26","DOI":"10.1109\/CSF.2009.26"},{"issue":"2","key":"20_CR3","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217\u2013273 (1992). https:\/\/citeseer.ist.psu.edu\/goguen92ordersorted.html","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11580850_8","volume-title":"Trustworthy Global Computing","author":"JD Guttman","year":"2005","unstructured":"Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116\u2013145. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11580850_8"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01128406","volume":"8","author":"JD Guttman","year":"1995","unstructured":"Guttman, J.D., Wand, M.: VLISP: a verified implementation of scheme. Lisp Symbolic Comput. 8, 5\u201332 (1995). https:\/\/doi.org\/10.1007\/BF01128406","journal-title":"Lisp Symbolic Comput."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Rowe, P.D., Thayer, F.J.: Completeness of CPSA. Technical report, MTR110479, The MITRE Corporation (2011). https:\/\/www.mitre.org\/publications\/technical-papers\/completeness-of-cpsa","DOI":"10.21236\/ADA562264"},{"key":"20_CR8","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA4: A cryptographic protocol shapes analyzer. The MITRE Corporation (2018). https:\/\/github.com\/mitre\/cpsaexp"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191\u2013230 (1999). http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs117","DOI":"10.3233\/JCS-1999-72-304"}],"container-title":["Lecture Notes in Computer Science","Protocols, Strands, and Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91631-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T13:07:34Z","timestamp":1652101654000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91631-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916305","9783030916312"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91631-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}