{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T16:10:08Z","timestamp":1759939808352},"reference-count":27,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2005,7,1]],"date-time":"2005-07-01T00:00:00Z","timestamp":1120176000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":2950,"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":[[2005,7]]},"DOI":"10.1016\/j.entcs.2005.04.033","type":"journal-article","created":{"date-parts":[[2005,7,14]],"date-time":"2005-07-14T14:59:35Z","timestamp":1121353175000},"page":"225-242","source":"Crossref","is-referenced-by-count":10,"title":["Breaking the Model: Finalisation and a Taxonomy of Security Attacks"],"prefix":"10.1016","volume":"137","author":[{"given":"John A.","family":"Clark","sequence":"first","affiliation":[]},{"given":"Susan","family":"Stepney","sequence":"additional","affiliation":[]},{"given":"Howard","family":"Chivers","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2005.04.033_bib001","series-title":"Security Engineering: A Guide to Building Dependable Distributed Systems","author":"Anderson","year":"2001"},{"key":"10.1016\/j.entcs.2005.04.033_bib002","unstructured":"Banach, R. and M. Poppleton, Retrenchment: An engineering variation on refinement, in: B'98: 2nd International B Conference, Montpellier, France, LNCS 1393 (1998)"},{"key":"10.1016\/j.entcs.2005.04.033_bib003","article-title":"Z in Practice","author":"Barden","year":"1994"},{"key":"10.1016\/j.entcs.2005.04.033_bib004","series-title":"The Wonderful Wizard of Oz","author":"Baum","year":"1900"},{"key":"10.1016\/j.entcs.2005.04.033_bib005","unstructured":"Boneh, D., R. DeMillo and R.J. Lipton, Breaking DES using a molecular computer, in: Proceedings of DIMACS workshop on DNA computing (1995)"},{"key":"10.1016\/j.entcs.2005.04.033_bib006","author":"Boneh"},{"key":"10.1016\/j.entcs.2005.04.033_bib007","doi-asserted-by":"crossref","unstructured":"Clark, J.A. and J.L. Jacob, Fault injection and a timing channel on an analysis technique, in: Eurocrypt 2002, 2002","DOI":"10.1007\/3-540-46035-7_12"},{"issue":"3","key":"10.1016\/j.entcs.2005.04.033_bib008","article-title":"Unifying concurrent and relational refinement","volume":"70","author":"Derrick","year":"2002","journal-title":"ENTCS"},{"key":"10.1016\/j.entcs.2005.04.033_bib009","series-title":"Computer Security","author":"Gollman","year":"1998"},{"key":"10.1016\/j.entcs.2005.04.033_bib010","series-title":"Cryptographic Hardware and Embedded Systems","first-page":"303","article-title":"Probing attacks on tamper resistant devices","volume":"1717","author":"Handschuh","year":"1999"},{"key":"10.1016\/j.entcs.2005.04.033_bib011","first-page":"187","article-title":"Data refinement refined (resum\u00e9)","volume":"213","author":"He","year":"1986"},{"key":"10.1016\/j.entcs.2005.04.033_bib012","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/j.entcs.2005.04.033_bib013","series-title":"Software Requirements and Specifications","author":"Jackson","year":"1995"},{"key":"10.1016\/j.entcs.2005.04.033_bib014","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/JCS-1992-13-409","article-title":"Basic theorems about security","volume":"1","author":"Jacob","year":"1992","journal-title":"Journal of Computer Security"},{"key":"10.1016\/j.entcs.2005.04.033_bib015","series-title":"Advances in Cryptology \u2013 Crypto 96 Proceedings","article-title":"Timing attacks on implementations of Diffie Hellman, RSA, DSS and other systems","volume":"1109","author":"Kocher","year":"1996"},{"key":"10.1016\/j.entcs.2005.04.033_bib016","author":"Kocher"},{"key":"10.1016\/j.entcs.2005.04.033_bib017","doi-asserted-by":"crossref","first-page":"617","DOI":"10.1007\/BF01213492","article-title":"Refinement-oriented probability for CSP","volume":"8","author":"Morgan","year":"1996","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.entcs.2005.04.033_bib018","series-title":"Quantum Computation and Quantum Information","author":"Nielsen","year":"2000"},{"key":"10.1016\/j.entcs.2005.04.033_bib019","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","article-title":"A timed model for Communicating Sequential Processes","volume":"58","author":"Reed","year":"1988","journal-title":"TCS"},{"key":"10.1016\/j.entcs.2005.04.033_bib020","series-title":"The Theory and Practice of Concurrency","author":"Roscoe","year":"1998"},{"key":"10.1016\/j.entcs.2005.04.033_bib021","doi-asserted-by":"crossref","unstructured":"Sanders, J.W. and P. Zuliani, Quantum programming, Technical Report TR-5-99, Programming Research Group, Oxford University Computing Laboratory (1999)","DOI":"10.1007\/10722010_6"},{"key":"10.1016\/j.entcs.2005.04.033_bib022","first-page":"952","article-title":"Verification of ASM refinements using generalized forward simulation","volume":"7","author":"Schellhorn","year":"2001","journal-title":"Journal of Universal Computer Science"},{"key":"10.1016\/j.entcs.2005.04.033_bib023","doi-asserted-by":"crossref","first-page":"1484","DOI":"10.1137\/S0097539795293172","article-title":"Polynomial time algorithms for prime-factorisation and discrete logarithms on a quantum computer","volume":"26","author":"Shor","year":"1997","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/j.entcs.2005.04.033_bib024","series-title":"The Z Notation: a Reference Manual","author":"Spivey","year":"1992"},{"key":"10.1016\/j.entcs.2005.04.033_bib025","series-title":"ZUM'98, Berlin","first-page":"284","article-title":"More powerful Z data refinement: pushing the state of the art in industrial refinement","volume":"1493","author":"Stepney","year":"1998"},{"key":"10.1016\/j.entcs.2005.04.033_bib026","article-title":"Hardware Evolution: Automatic design of electronic circuits in reconfigurable hardware by artificial evolution","author":"Thompson","year":"1998"},{"key":"10.1016\/j.entcs.2005.04.033_bib027","series-title":"Using Z. Specification, Refinement, and Proof","author":"Woodcock","year":"1996"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105050991?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105050991?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T07:26:55Z","timestamp":1586330815000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105050991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["S1571066105050991"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2005.04.033","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2005,7]]}}}