{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T11:49:31Z","timestamp":1783684171194,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,1,10]],"date-time":"2005-01-10T00:00:00Z","timestamp":1105315200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,1,10]]},"DOI":"10.1145\/1045405.1045413","type":"proceedings-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:31:47Z","timestamp":1123057907000},"page":"67-80","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Formal prototyping in early stages of protocol design"],"prefix":"10.1145","author":[{"given":"Alwyn","family":"Goodloe","sequence":"first","affiliation":[{"name":"University of Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carl A.","family":"Gunter","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark-Oliver","family":"Stehr","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,1,10]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes inComputer Science 2618","volume-title":"The European Symposium on Programming (ESOP)","author":"Abadi M.","year":"2004","unstructured":"M. Abadi , B. Blanchet , and C. Fournet . Just Fast Keying in the Pi Calculus . In D. Schmidt, editor, The European Symposium on Programming (ESOP) , Lecture Notes inComputer Science 2618 . Springer-Verlag , 2004 .]] M. Abadi, B. Blanchet, and C. Fournet. Just Fast Keying in the Pi Calculus. In D. Schmidt, editor, The European Symposium on Programming (ESOP), Lecture Notes inComputer Science 2618. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/996943.996946"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.347833"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988495"},{"key":"e_1_3_2_1_6_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44659-1_4","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs","author":"Bhargavan K.","year":"2000","unstructured":"K. Bhargavan , C. A. Gunter , and D. Obradovic . Routing information protocol in HOL\/SPIN . In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 , volume 1869 of Lecture Notes in Computer Science , pages 53 -- 72 , Portland, Oregon, August 2000. Springer-Verlag .]] K. Bhargavan, C. A. Gunter, and D. Obradovic. Routing information protocol in HOL\/SPIN. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 53--72, Portland, Oregon, August 2000. Springer-Verlag.]]"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_3_2_1_8_1","volume-title":"9th International Static Analysis Symposium (SAS'02)","author":"Blanchet B.","year":"2002","unstructured":"B. Blanchet . From Secrecy to Authencity in Security Protocols . In 9th International Static Analysis Symposium (SAS'02) , Lecture Notes In Computer Science 2477, pages 342--359. Springer-Verlag , 2002 .]] B. Blanchet. From Secrecy to Authencity in Security Protocols. In 9th International Static Analysis Symposium (SAS'02), Lecture Notes In Computer Science 2477, pages 342--359. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_9_1","first-page":"86","volume-title":"Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy","author":"Blanchet B.","year":"2004","unstructured":"B. Blanchet . Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy , pages 86 -- 100 , 2004 .]] B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy, pages 86--100, 2004.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00206-6"},{"key":"e_1_3_2_1_11_1","volume-title":"Communicating Sequential Processes","author":"Hoare C.A.R.","year":"1985","unstructured":"C.A.R. Hoare . Communicating Sequential Processes . Prentice-Hall , 1985 .]] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.]]"},{"key":"e_1_3_2_1_12_1","volume-title":"Model Checking","author":"Clark E.","year":"2000","unstructured":"E. Clark , O. Grumberg , and D. Peled . Model Checking . MIT Press , 2000 .]] E. Clark, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000.]]"},{"key":"e_1_3_2_1_13_1","unstructured":"M. Clavel F. Dur\u00e1n S. Eker P. Lincoln N. Mart\u00ed-Oliet J. Meseguer and J. Quesada. A Tutorial on Maude. http:\/\/maude.csl.sri.com March 2000.]]  M. Clavel F. Dur\u00e1n S. Eker P. Lincoln N. Mart\u00ed-Oliet J. Meseguer and J. Quesada. A Tutorial on Maude. http:\/\/maude.csl.sri.com March 2000.]]"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00359-0"},{"key":"e_1_3_2_1_15_1","volume-title":"Maude 2.0 Manual","author":"Clavel M.","year":"2003","unstructured":"M. Clavel , F. Dur\u00e1n , S. Eker , P. Lincoln , N. Mart\u00ed-Oliet , J. Meseguer , and C. Talcott . Maude 2.0 Manual . June 2003 , http:\/\/maude.cs.uiuc.edu.]] M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and C. Talcott. Maude 2.0 Manual. June 2003, http:\/\/maude.cs.uiuc.edu.]]"},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. of Workshop on Formal Methods and Security Protocols","author":"Denker G.","year":"1998","unstructured":"G. Denker , J. Meseguer , and C. Talctt . Protocol Specification and Analysis in Maude . In Proc. of Workshop on Formal Methods and Security Protocols , 1998 .]] G. Denker, J. Meseguer, and C. Talctt. Protocol Specification and Analysis in Maude. In Proc. of Workshop on Formal Methods and Security Protocols, 1998.]]"},{"key":"e_1_3_2_1_18_1","volume-title":"CDMA2000 Wireless Data Requirements for AAA. RFC 3141","author":"Hiller T.","year":"2001","unstructured":"T. Hiller , P. Walsh , X. Chen , M. Munson , G. Dommety , S. Sivalingham , B. Lim , P. McCann , H. Shiino , B. Hirschman , S. Manning , R. Hsu , R. Hsu , M. Lipford , P. Calhoun , C. Lo , E. Jaques , E. Campbell , Y. Xu , S. Baba , T. Ayaki , T. Seki , and A. Hammed . CDMA2000 Wireless Data Requirements for AAA. RFC 3141 , IETF, 2001 .]] T. Hiller, P. Walsh, X. Chen, M. Munson, G. Dommety, S. Sivalingham, B. Lim, P. McCann, H. Shiino, B. Hirschman, S. Manning, R. Hsu, R. Hsu, M. Lipford, P. Calhoun, C. Lo, E. Jaques, E. Campbell, Y. Xu, S. Baba, T. Ayaki, T. Seki, and A. Hammed. CDMA2000 Wireless Data Requirements for AAA. RFC 3141, IETF, 2001.]]"},{"key":"e_1_3_2_1_19_1","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall 1991.]]   G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall 1991.]]"},{"key":"e_1_3_2_1_20_1","volume-title":"IETF","author":"Kaufman C.","year":"2004","unstructured":"C. Kaufman . Internet Key Exchange(IKE V2) Protocol. RFC 2407 , IETF , 2004 .]] C. Kaufman. Internet Key Exchange(IKE V2) Protocol. RFC 2407, IETF, 2004.]]"},{"key":"e_1_3_2_1_21_1","volume-title":"IETF","author":"Kent S.","year":"1998","unstructured":"S. Kent and R. Atkinson . Security Architecture for the Internet Protocol. RFC 2401 , IETF , 1998 .]] S. Kent and R. Atkinson. Security Architecture for the Internet Protocol. RFC 2401, IETF, 1998.]]"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2004.5342234"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"e_1_3_2_1_24_1","first-page":"2","author":"K","year":"2000","unstructured":"K . McMillan. The SMV Manual. November 2000 , http:\/\/www- 2 .cs.cmu.edu\/~modelcheck\/smv.html.]] K. McMillan. The SMV Manual. November 2000, http:\/\/www-2.cs.cmu.edu\/~modelcheck\/smv.html.]]","journal-title":"McMillan. The SMV Manual."},{"key":"e_1_3_2_1_25_1","volume-title":"Journal of Logic Programming","author":"Meadows C.","year":"1994","unstructured":"C. Meadows . The NRL Protocol Analyzer : An Overview . Journal of Logic Programming , 1994 .]] C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 1994.]]"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/548089"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"C. Rigney. RADIUS Accounting. RFC 2866 IETF 2000.]]   C. Rigney. RADIUS Accounting. RFC 2866 IETF 2000.]]","DOI":"10.17487\/rfc2866"},{"key":"e_1_3_2_1_31_1","volume-title":"Modeling and Analysis of Security Protocols","author":"Ryan P.","year":"2001","unstructured":"P. Ryan and S. Schneider . Modeling and Analysis of Security Protocols . Addison-Wesley , 2001 .]] P. Ryan and S. Schneider. Modeling and Analysis of Security Protocols. Addison-Wesley, 2001.]]"}],"event":{"name":"WITS05: Workshop on Issues in the Theory of Security 2005 ( co-located with POPL 2005 Conference )","location":"Long Beach California","acronym":"WITS05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2005 workshop on Issues in the theory of security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1045405.1045413","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1045405.1045413","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:43:31Z","timestamp":1750286611000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1045405.1045413"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,10]]},"references-count":30,"alternative-id":["10.1145\/1045405.1045413","10.1145\/1045405"],"URL":"https:\/\/doi.org\/10.1145\/1045405.1045413","relation":{},"subject":[],"published":{"date-parts":[[2005,1,10]]},"assertion":[{"value":"2005-01-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}