00:23:11 | Guest73987: | Guest73987 is now known as SomeoneWeird |
00:52:02 | c0rw1n_: | c0rw1n_ is now known as c0rw1n |
02:49:53 | jcrubino: | jcrubino has left #bitcoin-wizards |
03:35:35 | c0rw1n: | c0rw1n is now known as c0rw|sleep |
03:41:22 | nsh: | you can definitely econogametheoretically achieve timelock encryption on a sidechain with relatively arbitrary 'grace windows' and relatively clear cost-security bounds |
03:41:46 | nsh: | (i contend) |
03:43:06 | nsh: | grace window being a rubbish term of blockspans wherein the game-theoretical and economic incentive conditions afford for dedistributed of secret shares |
03:43:12 | nsh: | *for blockspans |
03:43:44 | nsh: | within optimality thresholds |
03:44:34 | nsh: | (it'll always be possible for people to forsake their deposits and collude to bring the pieces together and decrypt prematurely / out-of-grace |
03:44:36 | nsh: | ) |
05:28:18 | orik_: | orik_ is now known as orik |
07:23:04 | spiftheninja: | spiftheninja has left #bitcoin-wizards |
09:05:18 | tepper.freenode.net: | topic is: This channel is not about short-term Bitcoin development | http://bitcoin.ninja/ | This channel is logged. | For logs and more information, visit http://bitcoin.ninja |
09:05:18 | tepper.freenode.net: | Users on #bitcoin-wizards: andy-logbot profreid Guyver2 orik webdeli bosma_ irclouis [7] justanotheruser dansmith_btc OneFixt Greed Dr-G3 GAit go1111111 prodatalab zenojis drawingthesun c0rw|sleep zwischenzug luny devrandom RoboTeddy epscy MoALTz_ NikolaiToryzin rasengan kgk forrestv null_radix ryanxcharles Luke-Jr Myagui nickler bobke_ myeagleflies altoz warptangent mr_burdell Logicwax zibbo Meeh kanzure tromp_ dgenr8 ebfull SomeoneWeird Krellan coutts tromp__ |
09:05:18 | tepper.freenode.net: | Users on #bitcoin-wizards: DougieBot5000 poggy pi07r_ sipa_ comboy_ jtimon_ mmozeiko lnovy btcdrak Taek42 optimator_ [\\\] Adlai phantomcircuit waxwing Guest39111 Apocalyptic throughnothing Pan0ram1x yoleaux petertodd crescend1 jgarzik kyletorpey CryptOprah Flyer33 AdrianG cfields kumavis sl01_ Fistful_of_Coins gmaxwell kinlo ahmed_ a5m0_ BlueMatt mortale eristisk copumpkin Starduster PaulCapestany maaku Shiftos Emcy_ Aquent atgreen wizkid057 Baz__ prepost doc321R K1773R |
09:05:18 | tepper.freenode.net: | Users on #bitcoin-wizards: SDCDev so mkarrer_ nuke1989 weex Anduck snorkl livegnik Graftec Alanius lclc Grishnakh fanquake GnarSith sneak [d__d] gnusha_ espes___ hguux_ btc_ jbenet michagogo samson_ BigBitz grandmaster2 spinza_ DoctorBTC PRab SubCreative otoburb wumpus artifexd EasyAt HaltingState starsoccer Hunger- HM hollandais Cory Nightwolf fluffypony fenn heath stonecoldpat LarsLarsen jaromil helo Keefe Iriez Eliel jrayhawk iddo huseby phedny MRL-Relay berndj |
09:05:18 | tepper.freenode.net: | Users on #bitcoin-wizards: midnightmagic nsh Muis coryfields mappum andytoshi BrainOverfl0w fds4345 gazab warren gavinandresen pigeons nanotube asoltys gribble LaptopZZ Graet smooth @gwillen amiller danneu catcow TD-Linux [Tristan] ryan-c roasbeef pajarillo Gnosis harrow abc56889 lechuga_ @ChanServ |
09:17:27 | c0rw|sleep: | c0rw|sleep is now known as c0rw|away |
11:36:13 | justanotheruser: | justanotheruser is now known as yolandi |
11:36:17 | yolandi: | yolandi is now known as yolandiVisser |
13:56:22 | kanzure: | are there any working whuffie implementations? |
13:57:19 | fenn: | whuffie, why don't we have it? a distributed trust network immune to sybil attacks, good for filtering content by relevance to your social ingroup |
13:59:48 | fenn: | "Levien observed that his notion of attack resistant trust metric was fundamentally very similar to the PageRank algorithm used by Google to rate article interest. In the case of Advogato, the trust metric is designed to include all individuals who could reasonably be considered members of the Free Software and Open Source communities while excluding others." |
14:00:18 | fenn: | but advogato is limited to a single website, single ingroup, and single trust metric |
15:08:18 | fenn: | Luke-Jr: are you preferentially re-mining valid blocks that have a large transaction fee in order to get the fee for yourself? curious minds are curious |
15:20:16 | fenn: | adding work to a stale block in hopes of finding one with higher difficulty and causing chain reorganization elsewhere |
15:46:57 | Luke-Jr: | fenn: that wouldn't work |
15:47:22 | fenn: | that's what i said |
15:48:31 | kanzure: | hm? |
16:08:47 | cbeams_: | cbeams_ is now known as cbeams |
17:19:55 | Taek42: | Taek42 is now known as Taek |
20:19:54 | a5m0_: | a5m0_ is now known as a5m0 |
20:23:15 | nsh: | -- |
20:23:15 | nsh: | Alfredo DeSantis … spoke on “Graph decompositions and secret-sharing schemes,” a silly topic which brings joy to combinatorists and yawns to everyone else. |
20:23:17 | nsh: | -- http://www.scottaaronson.com/blog/?p=2059 |
20:23:18 | nsh: | .t |
20:23:18 | yoleaux: | Sun, 16 Nov 2014 20:23:18 UTC |
20:23:20 | nsh: | .title |
20:23:21 | yoleaux: | Shtetl-Optimized » Blog Archive » What does the NSA think of academic cryptographers? Recently-declassified document provides clues |
20:26:24 | kanzure: | "I think I have hammered home my point often enough that I shall regard it as proved (by emphatic enunciation): the tendency at IACR meetings is for academic scientists (mathematicians, computer scientists, engineers, and philosophers masquerading as theoretical computer scientists) to present commendable research papers (in their own areas) which might affect cryptology at some future time or (more likely) in some other world. Naturally ... |
20:26:30 | kanzure: | ... this is not anathema to us." |
20:28:04 | nsh: | * nsh smiles |
20:28:18 | nsh: | tbh, this endears me to the NSA more than any of their public-relations exercises since Snowden |
20:30:15 | kanzure: | linked from that page... http://anotherlook.ca/ "n our time one of the dominant paradigms in cryptographic research goes by the name "provable security." This is the notion that the best (or, some would say, the only) way to have confidence in the security of a cryptographic protocol is to have a mathematically rigorous theorem that establishes some sort of guarantee of security (defined in a suitable way) under certain conditions and given ... |
20:30:21 | kanzure: | ... certain assumptions. The purpose of this website is to encourage the emergence of a more skeptical and less credulous attitude toward this notion and to contribute to a process of critical analysis of the positive and negative features of the "provable security" paradigm." |
20:31:46 | kanzure: | http://eprint.iacr.org/2004/152.pdf "We discuss the reasons why the search for mathematically convincing theoretical evidence to support the security of public-key systems has been an important theme of researchers. But we argue that the theorem-proof paradigm of theoretical mathematics is of limited relevance here and often leads to papers that are confusing and misleading." |
20:33:54 | fenn: | also theoretical mathematical proofs ignore the reality of hardware vulnerabilities |
20:38:02 | amiller: | fenn, that's not inherent, and not universally true, there are models of computation that more closely map to hardware, for example certicrypt is able to show that an implementation of a crypto algorithm takes the same amount of time to execute regardless of its input |
20:39:14 | kanzure: | also i would appreciate wizardly review of http://diyhpl.us/~bryan/irc/bitcoin/reorgs.log.txt regarding the handling of reorgs for bitcoin-using services/companies, but it's not a strongly wizardly topic |
20:40:23 | fenn: | amiller: you can't use math to prove that math is infallible |
20:40:35 | kanzure: | (well, i suppose it might be relevant, since i haven't seen good reorg-handling software implementations in non-bitcoin-wallets quite yet) |
20:40:41 | amiller: | fenn, sure, no one plans to |
20:42:46 | amiller: | fenn, you use math as a tool for bringing as much of the complicated parts of an argument into a simple world where it's easier to check the argument by simple procedures and even by computer program |
20:43:00 | kanzure: | oh, verification stuff |
20:43:02 | amiller: | i really like the tradition of "provable security" but the name itself "provable security" is almost entirely wrong and misleading |
20:43:20 | fenn: | then call it something else |
20:43:28 | hashtag_: | hashtag_ is now known as hashtag |
20:43:28 | amiller: | a little bit like calling GNU linux |
20:44:06 | fenn: | "newcomers to the field would logically expect that the problems that are used in security proofs come from a small set of extensively studied, natural problems. But they are in for an unpleasant surprise. What they encounter instead is a menagerie of ornate and bizarre mathematical problems whose presumed intractability is a basic assumption in the theorems about the security of many of the |
20:44:12 | fenn: | cryptographic protocols that have been proposed in the literature. |
20:44:15 | fenn: | this is certainly how i feel, as a newcomer to cryptography |
20:47:41 | amiller: | it's nice being able to reduce (the most complicated and specific) assumptions to other (well studied and minimalistic) assumptions, but a) you're still inevitably left with *some* unprovable assumptions (we are absolutely stuck with this fact as long as P!=NP is unsolved) and b) yeah if you look at *all* the literature there are a ton of bizarre assumptions, the goal is to stick to a few most plausible ones but thats hard to do |
20:47:47 | kanzure: | what would you (personally) expect instead? (instead of whatever that quote's author was expecting) |
20:50:03 | andytoshi: | fenn: is this referring to nonstandard assumptions or cryptosystems with weird properties? |
20:50:47 | fenn: | "traditionally, the security of a public-key system rests upon the assumed difficulty of a certain mathematical problem" |
20:50:51 | andytoshi: | a lot of that kinda stuff stuff is mapping out what's provably possible and provably impossible, and under what conditions |
20:50:57 | fenn: | so i assume he's talking about standard assumptions |
20:51:14 | andytoshi: | well, PKE under very standard assumptions is long since solved.. |
20:51:25 | fenn: | like the factorability of large prime numbers |
20:51:47 | fenn: | products* |
20:52:24 | andytoshi: | so, like, the first page of that paper says that RSA is CPA secure but not CCA secure ... except he doesn't use those terms (because he is anti-academia?) so it takes him forever |
20:52:35 | fenn: | if it's solved, why do we use other supposedly "hard" mathematical problems |
20:52:49 | andytoshi: | fenn: because there is more to life than PKE |
20:53:20 | andytoshi: | fenn: go check out IBE or ABE as examples of "weird" cryptosystems which require weird assumptions |
20:53:36 | andytoshi: | or the snark/iO stuff for way weirder cryptosystems which require way weirder assumptions |
20:53:54 | andytoshi: | (snarks and io are very different, i just lumped them in because they both require multilinear map assumptions) |
20:53:56 | kanzure: | PKE is public key encryption, RSA is RSA in the shamir sense |
20:53:59 | kanzure: | CPA is chosen plaintext.. something? |
20:54:56 | sipa_: | chosen plaintext attack |
20:54:57 | andytoshi: | even for something as "simple" as signatures, sometimes you need unique signatures, sometimes you need strong signatures, etc, these are all useful but weird properties |
20:55:02 | sipa_: | cca = chosen ciphertext attack |
20:55:10 | kanzure: | thank you sipa_ |
20:56:18 | kanzure: | andytoshi: my collection of foundational papers is a little bit lacking at the moment.. any suggestions would be appreciated. |
20:57:09 | andytoshi: | kanzure: mine is too :/ i try to keep an eye out for them when i encounter them |
20:57:25 | andytoshi: | but these days i learn foundational stuff from the introductions to non-foundational stuff :P |
20:57:27 | kanzure: | merkle's thesis only has <500 cites? what's going on here |
20:57:46 | andytoshi: | what was his thesis? |
20:58:17 | kanzure: | http://diyhpl.us/~bryan/papers2/security/cryptography/Secrecy,%20authentication,%20and%20public%20key%20systems%20-%20Ralph%20Merkle.pdf |
21:04:41 | kanzure: | "special physically secure communication channel" powered by rainbows and love and pixiedust |
21:06:05 | kanzure: | (not sure if there's a paper on that in particular) |
21:14:47 | amiller: | as a scientist i am skeptical that love exists at all, therefore your secure protocol based on a "love" assumption is unfounded |
21:15:34 | kanzure: | good |
21:16:43 | gmaxwell: | interesting commentary from the NSA text in aronson.com/blog/?p=2059 |
21:16:44 | gmaxwell: | 12:23 < nsh> .t |
21:16:49 | gmaxwell: | oops. |
21:17:38 | gmaxwell: | Interesting commentary, and somewhat concerning. That much of academic cryptographic is off in lala land is apparent enough to those of us in industry; that it's also apparent to the NSA ups my assessment of their capabilities somewhat. |
21:18:58 | nsh: | * nsh nods |
21:19:26 | andytoshi: | in fairness, this commentary is almost 20 years old |
21:20:27 | andytoshi: | i mean, academics are largely in lala land |
21:20:33 | andytoshi: | but there has been a lot of good stuff to come out of academia despite this |
21:20:44 | kanzure: | for all you know the guy was fired for not paying enough attention to all the topics |
21:21:13 | gmaxwell: | Sure sure, actually some things we respect very much would have been going on there at that time. (e.g. around that time is where most of the NIZKP stuff comes from) |
21:21:26 | kanzure: | oh hm |
21:21:59 | andytoshi: | also a lot of the stuff he described i think was labelled cryptography for grant-related reasons, but i expect nobody actually considered it to be cryptography |
21:22:15 | andytoshi: | e.g. any separation results involving oracles |
21:23:45 | gmaxwell: | Still, there is a lot of paper and time lost to very contrived research; and the mass of this stuff distances cryptography from the public. If the NSA has the resources to see through that noise, it means they gain a greater benefit from academic cryptography than the public does. |
21:24:36 | gmaxwell: | (I know that I've wasted many hours read papers only to realize that they were talking about non-constructable systems; based on unrealistic assumptions, etc.) |
21:29:31 | gwillen: | gmaxwell: you dropped the first half of your link http://www.scottaaronson.com/blog/?p=2059 |
21:29:46 | kanzure: | he goof-copied nsh's linkdrop |
21:30:21 | gwillen: | ahh, yeah, that was way up in my sb |
21:30:29 | kanzure: | gmaxwell: could i coerce you into glancing at http://diyhpl.us/~bryan/irc/bitcoin/reorgs.log.txt ? it's an idea i was going over with andytoshi for not losing BTC during reorgs. |
21:30:45 | nsh: | only if you pretty-print it |
21:31:04 | kanzure: | what does a pretty-printed irc log look like? |
21:31:31 | gmaxwell: | gwillen: yea, was meaning to leave it out entorely, the link was in the channel just above. :) |
21:31:46 | gmaxwell: | accidentally sent the line while trying to remove the link. |
21:31:54 | gwillen: | * gwillen nods |
21:32:52 | andytoshi: | so, what i got out of that "provable security" paper is that there are a lot of false proofs out there and almost everything is totally unreviewed |
21:33:18 | andytoshi: | which are both true -- coming from mathematics this "everyone submits several papers to every conference and the organizers spend 5 mins on each" thing seems totally insane |
21:33:38 | andytoshi: | but they are also not inherent problems with the program of reduction-proofs |
21:34:06 | gmaxwell: | Well its also no like anyone is using machine checkable proofs for these things either... |
21:34:26 | gmaxwell: | (and of course, even if they were there would be errors in the conversion to formal form) |
21:34:39 | andytoshi: | there is some interesting stuff on that i was reading ... standard IND-CPA/IND-CCA do not interact well with machine-checkable proofs |
21:34:46 | fenn: | wow, hash functions were new in 1994 |
21:35:00 | andytoshi: | you need some form of circular security (security even given encryptions of secret key data) |
21:35:15 | andytoshi: | one sec, i'll see if i can find a cite.. |
21:35:43 | kanzure: | "MD5 was designed by Ron Rivest in 1991 to replace an earlier hash function, MD4.[3] " |
21:35:57 | kanzure: | "MD4.. is a cryptographic hash function developed by Ronald Rivest in 1990." |
21:36:41 | fenn: | new enough that the author of this newsletter post has to explain what they're useful for |
21:36:41 | Eliel: | fenn: hash functions are pretty useless without a working computer, so I'm not surprised they aren't too old. |
21:37:08 | fenn: | computers were around for 40 years or so by then |
21:37:40 | gmaxwell: | andytoshi: I'd like to figure out how to get more people working on formal validation of software into the cryptocurrency space... as I think we're a better audience for their work then most other applications of software. (e.g. we're willing to take more costs in order to use software which has higher assurance than most other fields) |
21:37:58 | kanzure: | are the coq theorem solvers relevant? |
21:38:08 | kanzure: | oops, i mean coq theorem provers |
21:38:16 | kanzure: | like https://coq.inria.fr/ |
21:38:21 | Eliel: | fenn: the keyword is networks, cryptography and computers I believe. Not much use for cryptographic hash functions without all three. |
21:38:37 | gmaxwell: | kanzure: Absolutely. |
21:38:43 | fenn: | what was the NSA doing if not that |
21:39:02 | gmaxwell: | kanzure: though there are not extractors for languages we're likely to use for cryptocurrency production work right now. |
21:39:03 | andytoshi: | ok top paragroph http://link.springer.com/chapter/10.1007/978-3-540-78967-3_7#page-3 is where i read the circular security claim |
21:39:22 | kanzure: | paperbot: http://link.springer.com/chapter/10.1007/978-3-540-78967-3_7#page-3 |
21:39:40 | andytoshi: | top of page 3, since i assume paperbot will lose the #page-3 :) |
21:41:14 | gmaxwell: | kanzure: I've been doing some formal analysis of e.g. libsecp256k1. I have maching checkable proofs of overflow freeness in the field multiply and square operations. And sipa wrote semi-formal (but not machine checkable) proofs of correct computation given overflow freeness. |
21:43:28 | sipa_: | gmaxwell: you should patch frama-c to support int128 :) |
21:43:52 | gmaxwell: | sipa_: The frama-c guys actually told me what to do to do that. |
21:43:59 | sipa_: | cool |
21:44:05 | gmaxwell: | So it's on my todo list. |
21:45:27 | gmaxwell: | kanzure: one of the rust folks created a todo for someone to write a CoQ extractor to rust, so you could write provably correct software in CoQ and get rust code out; which would be neat. |
21:50:26 | kanzure: | seems like the efficient thing to do would be maybe routing through llvm (the details of which i'm unsure about) |
21:50:43 | kanzure: | .title http://www.cis.upenn.edu/~stevez/vellvm/ |
21:50:44 | yoleaux: | Vellvm: Verified LLVM |
21:51:04 | kanzure: | "The Vellvm project is building a (verified LLVM), a framework for reasoning about programs expressed in LLVM's intermediate representation and transformations that operate on it. .... The framework is built using the Coq interactive theorem prover." |
21:56:37 | gmaxwell: | kanzure: hm. I'm unable to tell how useful that is. A lot of it seems to be around creating provably correct optimization passes. Do you know if also includes things to take arbritary Coq proofs and extract LLVM implementations from them? |
21:59:13 | sipa_: | sipa_ is now known as sipa |
22:00:19 | kanzure: | sorry, no i don't know |
22:03:15 | kanzure: | "a framework for mechanized verification of llvm IR code, and IR to IR transformations" |
22:04:46 | Eliel: | I wonder... Would it be possible to use a simple pure non-optimized functional implementation that is provably correct and somehow verify that a compiled program is functionally equal with it? |
22:05:21 | Eliel: | while allowing for different optimization strategies for the compiler |
22:07:22 | midnightmagic: | :-o Sounds like a great deal of work. |
22:11:47 | jrayhawk: | that is harder than just writing an optimizing compiler for the functional implementation |
22:12:57 | gmaxwell: | Eliel: A lot of the functional implementations have bad realiablity once you consider computational and memory resource limits. Actually proving the peak resource usage in that context is an extra layer of difficulty. |
22:13:27 | gmaxwell: | (the seL4 proofs actually do this, but thats the largest piece of software that I'm aware of that has correctness proofs that extend to resource usage) |
22:13:43 | gmaxwell: | (not that I'm extremely well read on this space) |
22:15:54 | spiftheninjai: | spiftheninjai has left #bitcoin-wizards |
23:09:40 | c0rw|away: | c0rw|away is now known as c0rw1n |
23:10:38 | c0rw1n: | c0rw1n is now known as c0rw|timetravel |
23:12:41 | c0rw|timetravel: | c0rw|timetravel is now known as c0rw1n |
23:27:47 | OneFixt_: | OneFixt_ is now known as OneFixt |