{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T18:10:38Z","timestamp":1778263838140,"version":"3.51.4"},"publisher-location":"Boston, MA","reference-count":11,"publisher":"Springer US","isbn-type":[{"value":"9781441959058","type":"print"},{"value":"9781441959065","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-1-4419-5906-5_869","type":"book-chapter","created":{"date-parts":[[2011,10,27]],"date-time":"2011-10-27T09:50:45Z","timestamp":1319709045000},"page":"1285-1287","source":"Crossref","is-referenced-by-count":1,"title":["Theorem Proving and Security"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Meadows","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"869_CR1_869","unstructured":"Owre S, Shankar N, Rushby J (1992) PVS: a prototype verification system. In: CADE 11, Saratoga Springs"},{"key":"869_CR2_869","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Academic,\u00a0Boston"},{"key":"869_CR3_869","volume-title":"Isabelle\/HOL: a proof-assistant for higher-order logic","author":"T Nipkow","year":"2010","unstructured":"Nipkow T, Paulson L, Wenzel M (2010) Isabelle\/HOL: a proof-assistant for higher-order logic. Springer,\u00a0Berlin"},{"key":"869_CR4_869","unstructured":"Bertot Y, Casteran P (2004) Interactive theorem proving and protocol development. Coq\u2019Art: the calculus of inductive constructions. Springer,\u00a0Berlin"},{"key":"869_CR5_869","unstructured":"Benzel TV (1984) Analysis of a Kernel verification. In: Proceedings of 1984 IEEE security and privacy, Oakland. IEEE Computer Society Press, Silver\u00a0Spring"},{"issue":"1","key":"869_CR6_869","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/TSE.2007.70772","volume":"34","author":"CL Heitmeyer","year":"2008","unstructured":"Heitmeyer CL, Archer M, Leonard EI, McLean J (2008) Applying formal methods to a certifiably secure software system. IEEE Trans Softw Eng 34(1):82\u201398","journal-title":"IEEE Trans Softw Eng"},{"key":"869_CR7_869","first-page":"85","volume":"6","author":"L Paulson","year":"1998","unstructured":"Paulson L (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6:85\u2013128","journal-title":"J Comput Secur"},{"key":"869_CR8_869","unstructured":"Youn P, Adida B, Bond M, Clulow J, Herzog J, Lin A, Rivest RL, Anderson R (2005) Robbing the bank with a theorem prover. Cambridge University Computer Laboratory Technical Report UCAM-CL-TR-644"},{"key":"869_CR9_869","unstructured":"Bellare M, Rogaway P (2006) Code-based game-playing proofs and the security of triple encryption. In: EUROCRYPT 2006, St. Petersburg. LNCS, vol 4004. Springer,\u00a0Berlin"},{"key":"869_CR10_869","unstructured":"Nowak D (2008) On formal verification of arithmetic-based cryptographic primitives. In: Proceedings of information security and cryptology\u00a0\u2013 ICISC 2008, Seoul. Springer, Berlin, pp 368\u2013382"},{"key":"869_CR11_869","unstructured":"Barthe G, Gr\u00e9goire B, B\u00e9guelin SZ (2009) Formal certification of code-based cryptographic proofs. In: POPL 2009, Savannah, ACM, pp\u00a090\u2013101"}],"container-title":["Encyclopedia of Cryptography and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-5906-5_869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T17:36:43Z","timestamp":1778261803000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-5906-5_869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9781441959058","9781441959065"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-5906-5_869","relation":{},"subject":[],"published":{"date-parts":[[2011]]}}}