{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:07:00Z","timestamp":1743077220532,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_4","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"61-72","source":"Crossref","is-referenced-by-count":2,"title":["Pseudo-Random Number Generator Verification: A Case Study"],"prefix":"10.1007","author":[{"given":"Felix","family":"D\u00f6rre","sequence":"first","affiliation":[]},{"given":"Vladimir","family":"Klebanov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Heidelberg (2014)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Barak, B., Halevi, S.: A model and architecture for pseudo-random generation with applications to \/dev\/random. In: Proceedings of the 12th ACM Conference on Computer and Communications Security, CCS 2005, pp. 203\u2013212. ACM (2005)","DOI":"10.1145\/1102120.1102148"},{"key":"4_CR3","unstructured":"Bitcoin.org. Android security vulnerability (2013). \n                    https:\/\/bitcoin.org\/en\/alert\/2013-08-11-android"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Cornejo, M., Ruhault, S.: Characterization of real-life PRNGs under partial state corruption. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, CCS 2014, pp. 1004\u20131015. ACM (2014)","DOI":"10.1145\/2660267.2660377"},{"key":"4_CR5","unstructured":"Debian Weak Key Vulnerability. CVE-2008-0166 (2008). \n                    https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2008-0166"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Dodis, Y., Pointcheval, D., Ruhault, S., Vergniaud, D., Wichs, D.: Security analysis of pseudo-random number generators with input: \/dev\/random is not robust. In: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, pp. 647\u2013658. ACM (2013)","DOI":"10.1145\/2508859.2516653"},{"key":"4_CR7","unstructured":"Gurney, J.-M.: URGENT: RNG broken for last 4 months (2015). \n                    https:\/\/lists.freebsd.org\/pipermail\/freebsd-current\/2015-February\/054580.html"},{"issue":"1","key":"4_CR8","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/s102070100002","volume":"1","author":"D Johnson","year":"2001","unstructured":"Johnson, D., Menezes, A., Vanstone, S.: The elliptic curve digital signature algorithm (ECDSA). Int. J. Inf. Secur. 1(1), 36\u201363 (2001)","journal-title":"Int. J. Inf. Secur."},{"key":"4_CR9","unstructured":"The KeY Tool. \n                    www.key-project.org"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/j.tcs.2014.04.022","volume":"538","author":"V Klebanov","year":"2014","unstructured":"Klebanov, V.: Precise quantitative information flow analysis - a symbolic approach. Theoret. Comput. Sci. 538, 124\u2013139 (2014)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-40196-1_16","volume-title":"Quantitative Evaluation of Systems","author":"V Klebanov","year":"2013","unstructured":"Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177\u2013192. Springer, Heidelberg (2013)"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-36095-4_9","volume-title":"Topics in Cryptology \u2013 CT-RSA 2013","author":"K Michaelis","year":"2013","unstructured":"Michaelis, K., Meyer, C., Schwenk, J.: Randomly failed! the state of randomness in current Java implementations. In: Dawson, E. (ed.) CT-RSA 2013. LNCS, vol. 7779, pp. 129\u2013144. Springer, Heidelberg (2013)"},{"issue":"2","key":"4_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1023\/A:1025436905711","volume":"30","author":"PQ Nguyen","year":"2003","unstructured":"Nguyen, P.Q., Shparlinski, I.E.: The insecurity of the elliptic curve digital signature algorithm with partially known nonces. Des. Codes Crypt. 30(2), 201\u2013217 (2003)","journal-title":"Des. Codes Crypt."},{"key":"4_CR15","unstructured":"Scheben, C.: Program-level specification and deductive verification of security properties. Ph.D. thesis, Karlsruhe Institute of Technology (2014)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-31762-0_15","volume-title":"Formal Verification of Object-Oriented Software","author":"C Scheben","year":"2012","unstructured":"Scheben, C., Schmitt, P.H.: Verification of information flow properties of Java programs without approximations. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 232\u2013249. Springer, Heidelberg (2012)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-319-06410-9_39","volume-title":"FM 2014: Formal Methods","author":"C Scheben","year":"2014","unstructured":"Scheben, C., Schmitt, P.H.: Efficient self-composition for weakest precondition calculi. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 579\u2013594. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:54:54Z","timestamp":1559375694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}