{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T05:12:35Z","timestamp":1697433155426},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,6,1]],"date-time":"2003-06-01T00:00:00Z","timestamp":1054425600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["New Gener Comput"],"published-print":{"date-parts":[[2003,6]]},"DOI":"10.1007\/bf03037627","type":"journal-article","created":{"date-parts":[[2009,4,23]],"date-time":"2009-04-23T23:31:26Z","timestamp":1240529486000},"page":"87-106","source":"Crossref","is-referenced-by-count":1,"title":["Secure software infrastructure in the internet age"],"prefix":"10.1007","volume":"21","author":[{"given":"Etsuya","family":"Shibayama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akinori","family":"Yonezawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"BF03037627_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A. D., \u201cA Calculus for Cryptographic Protocols: The Spi Calculus,\u201dInformation and Computation, 148, 1, pp. 1\u201370, 1999.","journal-title":"Information and Computation"},{"issue":"1","key":"BF03037627_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02252866","volume":"2","author":"M. Abadi","year":"1990","unstructured":"Abadi, M., Feigenbaum, J., \u201cSecure Circuit Evaluation: A Protocol Based on Hiding Information from an Oracle,\u201dJ. of Cryptology, 2, 1, pp. 1\u201312, 1990.","journal-title":"J. of Cryptology"},{"key":"BF03037627_CR3","doi-asserted-by":"crossref","unstructured":"Affeldt, R. and Kobayashi, N., \u201cFormalization and Verification of a Mail Server in Coq,\u201d inProc. of ISSS2002, LNCS, to appear, 2003.","DOI":"10.1007\/3-540-36532-X_14"},{"key":"BF03037627_CR4","unstructured":"Aleph One, \u201cSmashing the Stack for Fun and Profit,\u201dPhrack 49,7, 1996, http:\/\/www.phrack.org\/leecharch.php?p=49"},{"key":"BF03037627_CR5","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-61996-8_49","volume":"1174","author":"D. Aucsmith","year":"1996","unstructured":"Aucsmith, D., \u201cTamper Resistant Software: An Implementation,\u201dInformation Hiding, LNCS 1174, pp. 317\u2013333, 1996.","journal-title":"Information Hiding"},{"issue":"1","key":"BF03037627_CR6","first-page":"47","volume":"9","author":"L. Badger","year":"1996","unstructured":"Badger, L., Sterne, D. F., Sherman, D. L. and Walker, K. M., \u201cA Domain and Type Enforcement UNIX Prototype,\u201dUSENIX Computing Systems, 9, 1, pp. 47\u201383, 1996.","journal-title":"USENIX Computing Systems"},{"key":"BF03037627_CR7","unstructured":"Baratloo, A., Singh, N. and Tsai, T., \u201cTransparent Run-time Defense against Stack-smashing Attacks,\u201d inProc. of USENIX Annual Conf., 2000."},{"key":"BF03037627_CR8","doi-asserted-by":"crossref","unstructured":"Binder, W., Hulaas, J. and Villaz\u00f3n, A., \u201cPortable Resource Control in Java: The J-SEAL2 Approach,\u201d inProc. of ACM Conf. on Object Oriented Programming Systems Languages and Applications, pp. 139\u2013155, 2001.","DOI":"10.1145\/504311.504293"},{"key":"BF03037627_CR9","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M. and Needham, R., \u201cA Logic of Authentication,\u201d inProc. of the Royal Society, Series A 426, 233\u2013271, 1989.","DOI":"10.1098\/rspa.1989.0125"},{"key":"BF03037627_CR10","doi-asserted-by":"crossref","unstructured":"Clark, D. D., \u201cThe Design Philosophy of the DARPA Internet Protocols,\u201d inProc. of SIGCOMM\u201988, Computer Communication Review, 18, 4, pp. 106\u2013114, 1988.","DOI":"10.1145\/52325.52336"},{"key":"BF03037627_CR11","unstructured":"Cowan, C., Pu, C., Maier, D., Walpole, J., Bakke, P., Beattie, S., Grier, A., Wagle, P., Zhang, Q. and Hinton, H., \u201cStackGuard: Automatic Adaptive Detection and Prevention of Buffer-overflow Attacks,\u201d inProc. of 7th USENIX Security Conf., pp. 63\u201378, 1998."},{"issue":"5","key":"BF03037627_CR12","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D. E. Denning","year":"1976","unstructured":"Denning, D. E., \u201cA Lattice Model of Secure Information Flow,\u201dComm. of the ACM, 19, 5, pp. 236\u2013243, 1976.","journal-title":"Comm. of the ACM"},{"key":"BF03037627_CR13","unstructured":"Formal Systems (Europe) Ltd., \u201cFDR2 User Manual,\u201d http:\/\/www.formal.demon.co.uk\/fdr2manual\/index.html, 2000."},{"key":"BF03037627_CR14","unstructured":"Forrester, J. E. and Miller, B. P., \u201cAn Empirical Study of the Robustness of Windows NT Applications Using Random Testing,\u201dUSENIX Windows Systems Symp., 2000."},{"key":"BF03037627_CR15","unstructured":"Gong, L., Mueller, M., Prafullchandra, H. and Schemers, R., \u201cGoing beyond the Sandbox: An Overview of the New Security Architecture in the Java Development Kit 1.2,\u201dUSENIX Symp. on Internet Technologies and Systems, pp. 103\u2013112, 1997."},{"key":"BF03037627_CR16","doi-asserted-by":"crossref","unstructured":"Grothoff, C., Palsberg, J. and Vitek, J., \u201cEncapsulating Objects with Confined Types,\u201d inProc. of ACM Conf. on Object Oriented Programming Systems Languages and Applications, pp. 241\u2013255, 2001.","DOI":"10.1145\/504311.504300"},{"key":"BF03037627_CR17","unstructured":"Gutmann, P., \u201cLessons Learned in Implementing and Deploying Crypto Software,\u201d inProc. of 11th USENIX Security Symp., pp. 315\u2013326, 2002."},{"issue":"4","key":"BF03037627_CR18","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"1998","unstructured":"Havelund, K. and Pressburger, T., \u201cModel Checking Java Programs Using Java PathFinder,\u201dInt\u2019l J. on Software Tools for Technology Transfer, 2, 4, pp. 366\u2013381, 1998.","journal-title":"Int\u2019l J. on Software Tools for Technology Transfer"},{"issue":"5","key":"BF03037627_CR19","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"Holzmann, G. J., \u201cThe Model Checker SPIN,\u201d IEEE Trans. on Software Engineering,23, 5, pp. 279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"BF03037627_CR20","doi-asserted-by":"crossref","unstructured":"Heintze, N. and Riecke, J. G., \u201cThe SLam Calculus: Programming with Secrecy and Integrity,\u201d inProc. of ACM Symp. on Principles of Programming Languages, pp. 365\u2013377, 1998.","DOI":"10.1145\/268946.268976"},{"key":"BF03037627_CR21","doi-asserted-by":"crossref","unstructured":"Igarashi, A. and Kobayashi, N., \u201cResource Usage Analysis,\u201d inProc. of ACM Symp. on Principles of Programming Languages, pp. 331\u2013342, 2001.","DOI":"10.1145\/565816.503303"},{"key":"BF03037627_CR22","doi-asserted-by":"crossref","unstructured":"Kato, K. and Oyama, Y., \u201cSoftware Pot: An Encapsulated Transferable File System for Secure Software Circulation,\u201d inProc. of ISSS2002, LNCS, to appear, 2003.","DOI":"10.1007\/3-540-36532-X_8"},{"issue":"2","key":"BF03037627_CR23","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1145\/276393.278524","volume":"20","author":"N. Kobayashi","year":"1998","unstructured":"Kobayashi, N., \u201cA Partially Deadlock-free Typed Process Calculus,\u201dACM Trans. on Programming Languages and Systems, 20, 2, pp. 436\u2013482, 1998.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"BF03037627_CR24","doi-asserted-by":"crossref","unstructured":"Leroy., X., \u201cJava Bytecode Verication: An Overview,\u201dInt\u2019l. Conf. on Computer Aided Verication, LNCS 2001, pp. 265\u2013285, 2001.","DOI":"10.1007\/3-540-44585-4_26"},{"key":"BF03037627_CR25","doi-asserted-by":"crossref","unstructured":"Myers, A. C., \u201cJFlow: Practical Mostly-static Information Flow Control,\u201d inProc. of ACM Symp. on Principles of Programming Languages, pp. 228\u2013241, 1999.","DOI":"10.1145\/292540.292561"},{"issue":"12","key":"BF03037627_CR26","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/96267.96279","volume":"33","author":"B. P. Miller","year":"1990","unstructured":"Miller, B. P., Fredriksen, L. and So, B., \u201cAn Empirical Study of the Reliability of UNIX Utilities,\u201dComm. of the ACM, 33, 12, pp. 32\u201344, 1990.","journal-title":"Comm. of the ACM"},{"key":"BF03037627_CR27","doi-asserted-by":"crossref","unstructured":"Mitchell, J. C., \u201cProgramming Language Methods in Computer Security,\u201d inProc. of ACM Symp. on Principles of Programming Languages, pp. 1\u20133, 2001.","DOI":"10.1145\/360204.360205"},{"issue":"3","key":"BF03037627_CR28","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K. and Glew, N., \u201cFrom System F to Typed Assembly Language,\u201d ACM Trans. on Programming Languages and Systems,21, 3, pp. 527\u2013568, 1999.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"BF03037627_CR29","unstructured":"National Institute of Standards and Technology, \u201cData Encryption Standard (DES),\u201d FIPS PUB 46-3, 1999."},{"key":"BF03037627_CR30","doi-asserted-by":"crossref","unstructured":"Necula, G. C., \u201cProof-carrying Code,\u201d inProc. of ACM Symp. on Principles of Programming Languages, pp. 106\u2013119, 1997.","DOI":"10.1145\/263699.263712"},{"key":"BF03037627_CR31","doi-asserted-by":"crossref","unstructured":"Necula, G. C. and Lee, P., \u201cThe Design and Implementation of a Certifying Compiler,\u201d inProc. of ACM Conf. on Programming Language Design and Implementation, pp. 333\u2013344, 1998.","DOI":"10.1145\/277652.277752"},{"key":"BF03037627_CR32","doi-asserted-by":"crossref","unstructured":"Necula, G. C., McPeak, S. and Weimer, W., \u201cCCured: Type-safe Retrofitting of Legacy Code,\u201dACM Symp. on Principles of Programming Languages, pp. 128\u2013139, 2002.","DOI":"10.1145\/565816.503286"},{"key":"BF03037627_CR33","doi-asserted-by":"crossref","unstructured":"Oiwa, Y., Sekiguchi, T., Sumii, E., Yonezawa, A., \u201cFail-safe ANSI-C Compiler: An Approach to Making C Programs Secure,\u201d inProc. of ISSS2002, LNCS, to appear, 2003.","DOI":"10.1007\/3-540-36532-X_9"},{"key":"BF03037627_CR34","unstructured":"Peterson, D. S., Bishop, M. and Pandey, R., \u201cA Flexible Containment Mechanism for Executing Untrusted Code,\u201d inProc. of 11th USENIX Security Symp., pp. 207\u2013225, 2002."},{"issue":"2","key":"BF03037627_CR35","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"R. L. Rivest","year":"1978","unstructured":"Rivest, R. L., Shamir, A., and Adelman, L. M., \u201cA Method for Obtaining Digital Signatures and Public-key Cryptosystems,\u201dComm. of the ACM, 21, 2, pp. 120\u2013126, 1978.","journal-title":"Comm. of the ACM"},{"issue":"6","key":"BF03037627_CR36","doi-asserted-by":"crossref","first-page":"689","DOI":"10.1145\/63526.63528","volume":"32","author":"J. A. Rochlis","year":"1989","unstructured":"Rochlis, J. A. and Eichin, M. W., \u201cWith Microscope and Tweezers: the Worm from MIT\u2019s Perspective,\u201dComm. of the ACM, 32, 6, pp. 689\u2013698, 1989.","journal-title":"Comm. of the ACM"},{"issue":"1","key":"BF03037627_CR37","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F. B. Schneider","year":"2000","unstructured":"Schneider, F. B., \u201cEnforceable Security Policies,\u201dACM Trans. Information and System Security, 3, 1, pp. 30\u201350, 2000.","journal-title":"ACM Trans. Information and System Security"},{"key":"BF03037627_CR38","unstructured":"Schneier, B.,Secrets and Lies: Digital Security in a Networked World, John Wiley & Sons, 2000."},{"key":"BF03037627_CR39","doi-asserted-by":"crossref","unstructured":"Shibayama, E., Hagihara, S., Kobayashi, N., Nisizaki, S., Taura, K. and Watanabe, T., \u201cAnZenMail: A Secure and Certified E-mail System,\u201d inProc. of ISSS2002, LNCS, to appear, 2003.","DOI":"10.1007\/3-540-36532-X_13"},{"key":"BF03037627_CR40","unstructured":"Simon, S.,The Code Book: The Science of Secrecy from Ancient Egypt to Quantum Cryptography, Anchor Books, 2000."},{"key":"BF03037627_CR41","unstructured":"The Coq Development Team,The Coq Proof Assistant Reference Manual, Version 7, 3, 2002."},{"key":"BF03037627_CR42","doi-asserted-by":"crossref","unstructured":"Erlingsson, \u00da. and Schneider, F. B., \u201cIRM Enforcement of Java Stack Inspection,\u201dIEEE Symp. on Security and Privacy, pp. 246\u2013255, 2000.","DOI":"10.1109\/SECPRI.2000.848461"},{"issue":"6","key":"BF03037627_CR43","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1002\/spe.369","volume":"31","author":"J. Vitek","year":"2001","unstructured":"Vitek, J. and Bokowski, B., \u201cConfined Types in Java,\u201dSoftware Practice and Experience, 31, 6, pp. 507\u2013532, 2001.","journal-title":"Software Practice and Experience"},{"key":"BF03037627_CR44","doi-asserted-by":"crossref","unstructured":"Wahbe, R. Lucco, S., Anderson T. E., and Graham, S. L., \u201cEfficient Software-based Fault Isolation,\u201d inProc. of ACM Symp. on Operating Systems Principles, pp. 203\u2013216, 1993.","DOI":"10.1145\/173668.168635"},{"key":"BF03037627_CR45","doi-asserted-by":"crossref","unstructured":"Walker, D., \u201cA Type System for Expressive Security Policies,\u201dACM Symp. on Principles of Programming Languages, pp. 254\u2013267, 2000.","DOI":"10.1145\/325694.325728"},{"issue":"3","key":"BF03037627_CR46","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF03037600","volume":"19","author":"W. Wen","year":"2001","unstructured":"Wen, W. and Mizoguchi, F., \u201cWeb Security: Authentication Protocols and Their Analysis,\u201dNew Generation Computing, 19, 3, pp. 283\u2013299, 2001.","journal-title":"New Generation Computing"}],"container-title":["New Generation Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037627.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF03037627\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03037627","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T20:52:40Z","timestamp":1558558360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF03037627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,6]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,6]]}},"alternative-id":["BF03037627"],"URL":"https:\/\/doi.org\/10.1007\/bf03037627","relation":{},"ISSN":["0288-3635","1882-7055"],"issn-type":[{"value":"0288-3635","type":"print"},{"value":"1882-7055","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,6]]}}}