Okazaki, Hiroyuki On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors. (English) Zbl 07771368 Formaliz. Math. 31, No. 1, 53-57 (2023). MSC: 68V20 65F25 94A11 97H60 PDFBibTeX XMLCite \textit{H. Okazaki}, Formaliz. Math. 31, No. 1, 53--57 (2023; Zbl 07771368) Full Text: DOI OA License
Mazurek, Łukasz EthVer: formal verification of randomized Ethereum smart contracts. (English) Zbl 1490.91255 Bernhard, Matthew (ed.) et al., Financial cryptography and data security. FC 2021 international workshops. Codecfin, DeFi, VOTING, and WTSC, virtual event, March 5, 2021. Revised selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 12676, 364-380 (2021). MSC: 91G99 94A60 PDFBibTeX XMLCite \textit{Ł. Mazurek}, Lect. Notes Comput. Sci. 12676, 364--380 (2021; Zbl 1490.91255) Full Text: DOI
Arusoaie, Andrei Certifying Findel derivatives for blockchain. (English) Zbl 1518.91271 J. Log. Algebr. Methods Program. 121, Article ID 100665, 20 p. (2021). MSC: 91G20 91G80 94A62 PDFBibTeX XMLCite \textit{A. Arusoaie}, J. Log. Algebr. Methods Program. 121, Article ID 100665, 20 p. (2021; Zbl 1518.91271) Full Text: DOI arXiv
Butler, D.; Lochbihler, A.; Aspinall, D.; Gascón, A. Formalising \(\varSigma\)-protocols and commitment schemes using CryptHOL. (English) Zbl 1524.94063 J. Autom. Reasoning 65, No. 4, 521-567 (2021). MSC: 94A60 68V20 PDFBibTeX XMLCite \textit{D. Butler} et al., J. Autom. Reasoning 65, No. 4, 521--567 (2021; Zbl 1524.94063) Full Text: DOI
Ribeiro, Maria; Adão, Pedro; Mateus, Paulo Formal verification of Ethereum smart contracts using Isabelle/HOL. (English) Zbl 1476.68156 Nigam, Vivek (ed.) et al., Logic, language, and security. Essays dedicated to Andre Scedrov on the occasion of his 65th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12300, 71-97 (2020). MSC: 68Q60 03B70 68V15 91B41 94A60 PDFBibTeX XMLCite \textit{M. Ribeiro} et al., Lect. Notes Comput. Sci. 12300, 71--97 (2020; Zbl 1476.68156) Full Text: DOI
Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza CryptHOL: game-based proofs in higher-order logic. (English) Zbl 1455.94121 J. Cryptology 33, No. 2, 494-566 (2020). MSC: 94A60 94A62 68V15 91A99 PDFBibTeX XMLCite \textit{D. A. Basin} et al., J. Cryptology 33, No. 2, 494--566 (2020; Zbl 1455.94121) Full Text: DOI
Butler, David; Aspinall, David; Gascón, Adrià On the formalisation of \(\varSigma \)-protocols and commitment schemes. (English) Zbl 1524.94062 Nielson, Flemming (ed.) et al., Principles of security and trust. 8th international conference, POST 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11426, 175-196 (2019). MSC: 94A60 68V20 PDFBibTeX XMLCite \textit{D. Butler} et al., Lect. Notes Comput. Sci. 11426, 175--196 (2019; Zbl 1524.94062) Full Text: DOI
Hess, Andreas V.; Mödersheim, Sebastian A.; Brucker, Achim D. Stateful protocol composition. (English) Zbl 1496.68065 Lopez, Javier (ed.) et al., Computer security. 23rd European symposium on research in computer security, ESORICS 2018, Barcelona, Spain, September 3–7, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 11098, 427-446 (2018). MSC: 68M25 94A60 PDFBibTeX XMLCite \textit{A. V. Hess} et al., Lect. Notes Comput. Sci. 11098, 427--446 (2018; Zbl 1496.68065) Full Text: DOI Link
Butler, David; Aspinall, David; Gascón, Adrià How to simulate it in Isabelle: towards formal proof for secure multi-party computation. (English) Zbl 1483.68486 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 114-130 (2017). MSC: 68V20 68Q10 68V15 94A60 PDFBibTeX XMLCite \textit{D. Butler} et al., Lect. Notes Comput. Sci. 10499, 114--130 (2017; Zbl 1483.68486) Full Text: DOI arXiv
Lochbihler, Andreas Probabilistic functions and cryptographic oracles in higher order logic. (English) Zbl 1335.68033 Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 503-531 (2016). MSC: 68N18 94A60 PDFBibTeX XMLCite \textit{A. Lochbihler}, Lect. Notes Comput. Sci. 9632, 503--531 (2016; Zbl 1335.68033) Full Text: DOI
Affeldt, Reynald; Hagiwara, Manabu; Sénizergues, Jonas Formalization of Shannon’s theorems. (English) Zbl 1315.68216 J. Autom. Reasoning 53, No. 1, 63-103 (2014). MSC: 68T15 94A17 94A24 PDFBibTeX XMLCite \textit{R. Affeldt} et al., J. Autom. Reasoning 53, No. 1, 63--103 (2014; Zbl 1315.68216) Full Text: DOI
Li, Yongjian; Pang, Jun An inductive approach to strand spaces. (English) Zbl 1298.68083 Formal Asp. Comput. 25, No. 4, 465-501 (2013). MSC: 68P25 68M12 68T15 94A60 94A62 PDFBibTeX XMLCite \textit{Y. Li} and \textit{J. Pang}, Formal Asp. Comput. 25, No. 4, 465--501 (2013; Zbl 1298.68083) Full Text: DOI
Mhamdi, Tarek; Hasan, Osman; Tahar, Sofiène Formalization of entropy measures in HOL. (English) Zbl 1342.68295 Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 233-248 (2011). MSC: 68T15 94A17 PDFBibTeX XMLCite \textit{T. Mhamdi} et al., Lect. Notes Comput. Sci. 6898, 233--248 (2011; Zbl 1342.68295) Full Text: DOI
Jacobs, Bart; Wichers Schreur, Ronny Logical formalisation and analysis of the Mifare Classic card in PVS. (English) Zbl 1342.68288 Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 3-17 (2011). MSC: 68T15 94A60 94A62 PDFBibTeX XMLCite \textit{B. Jacobs} and \textit{R. Wichers Schreur}, Lect. Notes Comput. Sci. 6898, 3--17 (2011; Zbl 1342.68288) Full Text: DOI Link
Basin, David; Capkun, Srdjan; Schaller, Patrick; Schmidt, Benedikt Let’s get physical: Models and methods for real-world security protocols. (English) Zbl 1252.68040 Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 1-22 (2009). MSC: 68M12 68T15 94A60 PDFBibTeX XMLCite \textit{D. Basin} et al., Lect. Notes Comput. Sci. 5674, 1--22 (2009; Zbl 1252.68040) Full Text: DOI
Backes, Michael; Berg, Matthias; Unruh, Dominique A formal language for cryptographic pseudocode. (English) Zbl 1182.94035 Cervesato, Iliano (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 15th international conference, LPAR 2008, Doha, Qatar, November 22–27, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89438-4/pbk). Lecture Notes in Computer Science 5330. Lecture Notes in Artificial Intelligence, 353-376 (2008). MSC: 94A60 68N18 68T15 PDFBibTeX XMLCite \textit{M. Backes} et al., Lect. Notes Comput. Sci. 5330, 353--376 (2008; Zbl 1182.94035) Full Text: DOI
Kahsai, Temesghen; Miculan, Marino Implementing spi calculus using nominal techniques. (English) Zbl 1142.68445 Beckmann, Arnold (ed.) et al., Logic and theory of algorithms. 4th conference on computability in Europe, CiE 2008, Athens, Greece, June 15–20, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-69405-2/pbk). Lecture Notes in Computer Science 5028, 294-305 (2008). MSC: 68Q85 03B70 68T15 94A60 PDFBibTeX XMLCite \textit{T. Kahsai} and \textit{M. Miculan}, Lect. Notes Comput. Sci. 5028, 294--305 (2008; Zbl 1142.68445) Full Text: DOI
Zhang, Ningrong; Zhang, Xingyuan; Wang, Yuanyuan Mechanical proofs about BW multi-party contract signing protocol. (English) Zbl 1119.68429 Wuhan Univ. J. Nat. Sci. 11, No. 6, 1516-1520 (2006). MSC: 68T15 94A60 PDFBibTeX XMLCite \textit{N. Zhang} et al., Wuhan Univ. J. Nat. Sci. 11, No. 6, 1516--1520 (2006; Zbl 1119.68429) Full Text: DOI
Chadha, Rohit; Kremer, Steve; Scedrov, Andre Formal analysis of multiparty contract signing. (English) Zbl 1134.94372 J. Autom. Reasoning 36, No. 1-2, 39-83 (2006). MSC: 94A62 68M12 03B44 68Q60 PDFBibTeX XMLCite \textit{R. Chadha} et al., J. Autom. Reasoning 36, No. 1--2, 39--83 (2006; Zbl 1134.94372) Full Text: DOI
Bella, Giampaolo; Massacci, Fabio; Paulson, Lawrence C. Verifying the SET purchase protocols. (English) Zbl 1104.68465 J. Autom. Reasoning 36, No. 1-2, 5-37 (2006). MSC: 68P25 68T15 94A62 PDFBibTeX XMLCite \textit{G. Bella} et al., J. Autom. Reasoning 36, No. 1--2, 5--37 (2006; Zbl 1104.68465) Full Text: DOI
Ogawa, Mizuhito; Horita, Eiichi; Ono, Satoshi Proving properties of incremental Merkle trees. (English) Zbl 1135.68558 Nieuwenhuis, Robert (ed.), Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28005-7/pbk). Lecture Notes in Computer Science 3632. Lecture Notes in Artificial Intelligence, 424-440 (2005). MSC: 68T15 94A62 PDFBibTeX XMLCite \textit{M. Ogawa} et al., Lect. Notes Comput. Sci. 3632, 424--440 (2005; Zbl 1135.68558) Full Text: DOI
Li, Yongjian The inductive approach to strand space. (English) Zbl 1169.68327 Wang, Farn (ed.), Formal techniques for networked and distributed systems – FORTE 2005. 25th IFIP WG 6.1 international conference, Taipei, Taiwan, October 2–5, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29189-X/pbk). Lecture Notes in Computer Science 3731, 547-552 (2005). MSC: 68M12 68T15 94A62 PDFBibTeX XMLCite \textit{Y. Li}, Lect. Notes Comput. Sci. 3731, 547--552 (2005; Zbl 1169.68327) Full Text: DOI