{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:32:20Z","timestamp":1720625540567},"reference-count":62,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,3,13]],"date-time":"2014-03-13T00:00:00Z","timestamp":1394668800000},"content-version":"vor","delay-in-days":4089,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003]]},"DOI":"10.1016\/s1571-0661(03)50004-4","type":"journal-article","created":{"date-parts":[[2014,3,17]],"date-time":"2014-03-17T20:33:12Z","timestamp":1395088392000},"page":"55-98","source":"Crossref","is-referenced-by-count":1,"special_numbering":"C","title":["Towards the Correctness of Security Protocols"],"prefix":"10.1016","volume":"83","author":[{"given":"Mourad","family":"Debbabi","sequence":"first","affiliation":[]},{"given":"Mohamed","family":"Mejri","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(03)50004-4_bb0005","series-title":"Technical report, DEC\/SRC","article-title":"A Calculus for Cryptographic Protocols: The Spi Calculus","author":"Abadi","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0010","doi-asserted-by":"crossref","DOI":"10.1145\/266420.266432","article-title":"A Calculus for Cryptographic Protocols: The Spi Calculus","author":"Abadi","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0015","first-page":"201","article-title":"A semantics for a logic of authentication","author":"Abadi","year":"1991"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0020","first-page":"14","article-title":"A Logic of Communication in a Hostile Environment","author":"Bieber","year":"1990"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0025","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-3240-0_5","article-title":"Formal development of authentication protocols","author":"Bieber","year":"1994"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0030","doi-asserted-by":"crossref","DOI":"10.1109\/CSFW.1993.246632","article-title":"Abstract machines for communication security","author":"Bieber","year":"1993"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0035","series-title":"Proceedings of the Third ACM Conference on Computer and Communications Security, CCS\u201996","first-page":"106","article-title":"An Approach to the Formal Verification of Cryptographic Protocols","author":"Bolignano","year":"1996"},{"issue":"5","key":"10.1016\/S1571-0661(03)50004-4_bb0040","doi-asserted-by":"crossref","first-page":"694","DOI":"10.1109\/49.223872","article-title":"Security Archituctures Using Formal Methods","volume":"11","author":"Boyd","year":"1990","journal-title":"Journal on Selected Areas in Communications"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0045","first-page":"273","article-title":"A Framework for Authentication","author":"Boyd","year":"1992"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0050","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R. Needham. A logic of authentication. In Proceedings of the Royal Society of London A Vol.426, pages 233\u2013271, 198.","DOI":"10.1145\/74850.74852"},{"issue":"2","key":"10.1016\/S1571-0661(03)50004-4_bb0055","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/382258.382790","article-title":"Rejoinder to Nessett","volume":"24","author":"Burrows","year":"1990","journal-title":"ACM Operating Systems Review"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0060","series-title":"Technical Report No. SSC\/1999\/38","article-title":"Formal methods in the design of cryptographic protocols (state of the art)","author":"Buttyan","year":"1999"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0065","series-title":"These d\u2019Informatique soutenue \u00e0 l\u2019Universit\u00e9 PARIS XI","article-title":"Formal Specification and Analysis of Cryptographic Protocols","author":"Carlsen","year":"1994"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0070","series-title":"A Survey of Authentication Protocol Literature","author":"Clark","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0075","first-page":"390","article-title":"The murphi verification system","volume":"volume 1102","author":"Dill","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0080","article-title":"A New Algorithm for Automatic Verification of Authentication Cryptographic Protocols","author":"Debbabi","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0085","series-title":"Hiroshima","article-title":"Formal Automatic Verification of Authentication Cryptographic Protocols","author":"Debbabi","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0090","series-title":"Proceedings of the Second International Workshop on Enterprise Security, Massachusetts Institute of Technology (MIT)","article-title":"From Protocol Specifications to Flaws and Attack Scenarios: An Automatic and Formal Algorithm","author":"Debbabi","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0095","series-title":"the International Journal on Software Tools For Technology Transfer (STTT)","first-page":"1","article-title":"Security by Typing","author":"Debbabi","year":"2002"},{"issue":"1&2","key":"10.1016\/S1571-0661(03)50004-4_bb0100","first-page":"279","article-title":"Termination of Rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. of Symbolic Computation"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0105","series-title":"Technical report, Imperial College, Reserch Report DOC 84\/21","article-title":"Eqution reasoning and the knuth-bandix algorithm-an informal introduction","author":"Dick","year":"1984"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0110","series-title":"IEEE Transactions on Information Theory","first-page":"198","article-title":"On the Security of Public Key Protocols","author":"Dolev","year":"1983"},{"issue":"2","key":"10.1016\/S1571-0661(03)50004-4_bb0115","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/BF00196790","article-title":"Applying a formal analysis technique to the ccitt x.509 strong two-way authentication protocol","volume":"3","author":"Gaarder","year":"1991","journal-title":"Journal of cryptology"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0120","series-title":"Technical report","article-title":"Security Modelling in CSP and FDR: Deliverable Bundle 2","author":"Gardiner","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0125","series-title":"Security Modelling in CSP and FDR: Deliverable Bundle 3","author":"Gardiner","year":"1996"},{"issue":"3","key":"10.1016\/S1571-0661(03)50004-4_bb0130","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/146937.146940","article-title":"A Logic for Reasoning About Security","volume":"10","author":"Glasgow","year":"1992","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0135","first-page":"103","article-title":"On Belief Evolution in Authentication Protocols","author":"Gligor","year":"1991"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0140","first-page":"234","article-title":"Reasoning About Belief in Cryptographic Protocols","author":"Gong","year":"1990"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0145","series-title":"Communating Sequential Process","author":"Hoare","year":"1985"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0150","first-page":"35","article-title":"Relating Strands and Multiset Rewriting for Security Protocol Analysis","author":"Iliano","year":"2000"},{"issue":"2","key":"10.1016\/S1571-0661(03)50004-4_bb0155","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00197942","article-title":"Three Systems for Cryptographic Protocol Analysis","volume":"7","author":"Kemmerer","year":"1994","journal-title":"Journal of Cryptology"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0160","first-page":"134","article-title":"Using Formal Verification Techniques to Analyse Encryption Protocols","author":"Kemmerer","year":"1987"},{"issue":"4","key":"10.1016\/S1571-0661(03)50004-4_bb0165","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","article-title":"Analysing Encryption Protocols Using Formal Verification Techniques","volume":"7","author":"Kemmerer","year":"1989","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"4","key":"10.1016\/S1571-0661(03)50004-4_bb0170","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1145\/163640.163643","article-title":"Authentication in Distributed Systems: A Bibliography","volume":"27","author":"Liebl","year":"1993","journal-title":"Operating Systems Review"},{"issue":"3","key":"10.1016\/S1571-0661(03)50004-4_bb0175","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","article-title":"An Attack on the Needham-Schroeder Public Key Authentication Protocol","volume":"56","author":"Lowe","year":"1995","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0180","first-page":"147","article-title":"Breaking and fixing the needham schroeder public-key protocol using fdr","volume":"volume 1055","author":"Lowe","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0185","doi-asserted-by":"crossref","DOI":"10.1109\/CSFW.1996.503701","article-title":"Some new attacks upon security protocols","author":"Lowe","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0190","series-title":"Technical report","article-title":"Splice-as: A case study in using csp to detect errors in security protocols","author":"Lowe","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0195","series-title":"Proceedings of the Computer Security Foundations Workshop VI","first-page":"147","article-title":"Towards the Formal Analysis of Security Protocols","author":"Mao","year":"1993"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0200","series-title":"Proceedings of Asiacrypt","first-page":"96","article-title":"Formal Verification of Cryptographic Protocols: A Survey","author":"Meadows","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0205","series-title":"Technical report, Laboratory for Foundations of Computer Science","article-title":"The polyadic \u03c0-calculus: A tutorial","author":"Milner","year":"1991"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0210","series-title":"Technical report, Laboratory for Foundations of Computer Science","article-title":"A calculus of mobile processes","author":"Milner","year":"1989"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0215","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes (Parts I and II)","volume":"100","author":"Milner","year":"1992","journal-title":"Information and, Computation"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0220","series-title":"Proceedings 1997 IEEE Symposium on Security and Privacy","first-page":"141","article-title":"Automated Analysis of Cryptographic Protocols Using Murphi","author":"Mitchell","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0225","first-page":"1","article-title":"Finite-State Analysis of SSL 3.0","author":"Mitchell","year":"1997"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0230","first-page":"57","article-title":"A Logic of Knowledge and Belief about Computer Security","author":"Moser","year":"1989"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0235","first-page":"204","article-title":"An Axomiatic Basis of Trust in Distributed System","author":"Rangan","year":"1988"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0240","series-title":"Technical report","article-title":"Security Modelling in CSP and FDR: Final Report","author":"Roscoe","year":"1995"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0245","series-title":"Technical Report Technical report 93\u20147, Technical Report, Center for Information Technology Integration","article-title":"Formal Methods for the Analysis of Authentication Protocols","author":"Rubin","year":"1993"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0250","series-title":"Journal of Logic Programming","article-title":"The NRL Protocol Analyser: An Overview","author":"C. s","year":"1994"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0255","first-page":"174","article-title":"Security Properties and CSP","author":"Schneider","year":"1996"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0260","first-page":"119","article-title":"Analysis of a Fair Exchange Protocol","author":"Shmatikov","year":"2000"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0265","first-page":"313","article-title":"Authentication in Open Systems","author":"Snekkenes","year":"1990"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0270","series-title":"Faculty of Mathematics and Natural Sciences","article-title":"Formal Specification and Analysis of Cryptographic Protocols","author":"Snekkenes","year":"1995"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0275","series-title":"Proceedings of the 1991 IEEE Symposium on Security and Privacy","first-page":"156","article-title":"The Use of Logic in the Analysis of Cryptographic Protocols","author":"Syverson","year":"1991"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0280","doi-asserted-by":"crossref","unstructured":"P. Syverson. Knowledge, Belief, and Semantics in the Analysis of Cryptographic Protocols. Journal of Computer Security, 1(3):317\u2013334, 92.","DOI":"10.3233\/JCS-1992-13-407"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0285","first-page":"87","article-title":"Dolev-Yao is no better than Machiavelli","author":"Syverson","year":"2000"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0290","series-title":"In IEEE 1994 Computer Society Symposium on Security and Privacy","first-page":"14","article-title":"On Unifing some Cryptographic Protocol Logics","author":"Syverson","year":"1994"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0295","series-title":"Security Investigation Final Report","article-title":"The commission of the European Communities CEC DG-XIII","year":"1993"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0300","first-page":"146","article-title":"Formal Specification of a Secure Distributed System","author":"Varadharajan","year":"1989"},{"issue":"8","key":"10.1016\/S1571-0661(03)50004-4_bb0305","doi-asserted-by":"crossref","DOI":"10.1016\/0167-4048(89)90008-4","article-title":"Verification of Network Security Protocols","author":"Varadharajan","year":"1989","journal-title":"Computers and Security"},{"key":"10.1016\/S1571-0661(03)50004-4_bb0310","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0920-5489(89)90022-6","article-title":"Use of Formal Technique in the Specification of Authentication Protocols","volume":"9","author":"Varadharajan","year":"1990","journal-title":"Computer Standards and Interfaces"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"pt","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066103500044?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066103500044?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T10:37:12Z","timestamp":1565260632000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066103500044"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":62,"alternative-id":["S1571066103500044"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(03)50004-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}