- cypherpunks@lists.ogf.org

Re: [tor-talk] New paper : Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries
by Eugen Leitl 02 Sep '13

02 Sep '13

----- Forwarded message from Roger Dingledine <arma(a)mit.edu> ----- Date: Sun, 1 Sep 2013 22:10:56 -0400 From: Roger Dingledine <arma(a)mit.edu> To: tor-talk(a)lists.torproject.org Subject: Re: [tor-talk] New paper : Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries User-Agent: Mutt/1.5.20 (2009-06-14) Reply-To: tor-talk(a)lists.torproject.org On Mon, Sep 02, 2013 at 11:35:22AM +1000, Erik de Castro Lopo wrote: > Hi all, > > Heads up on a new paper suggesting that its possible to unmask > Tor users using traffic correlation: > > http://www.ohmygodel.com/publications/usersrouted-ccs13.pdf > > Code here: > > http://torps.github.io/ > > Would be interested in hearing the opinions of the core Tor > develpoment team on this stuff. Yep. They're part of the Tor research community. I have plans for writing a blog post about the paper, to explain what it means, what it doesn't mean, what we should do about it, and what research questions remain open. Stuff keeps catching fire with bigger flames though. The extremely short answer is "Yes, a big enough adversary can screw Tor users. But we knew that. I think it's great that the paper presents the dual risks of relay adversaries and link adversaries, since most of the time when people are freaking out about one of them they're forgetting the other one. And we really should raise the guard rotation period. If you do their compromise graphs again with guards rotated every nine months, they look way different." https://trac.torproject.org/projects/tor/ticket/8240 https://trac.torproject.org/projects/tor/ticket/9321 --Roger -- tor-talk mailing list - tor-talk(a)lists.torproject.org To unsusbscribe or change other settings go to https://lists.torproject.org/cgi-bin/mailman/listinfo/tor-talk ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

1 0

[tor-talk] New paper : Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries
by Eugen Leitl 02 Sep '13

02 Sep '13

----- Forwarded message from Erik de Castro Lopo <mle+tools(a)mega-nerd.com> ----- Date: Mon, 2 Sep 2013 11:35:22 +1000 From: Erik de Castro Lopo <mle+tools(a)mega-nerd.com> To: tor-talk(a)lists.torproject.org Subject: [tor-talk] New paper : Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries Organization: Erik Conspiracy Secret Labs X-Mailer: Sylpheed 3.4.0beta4 (GTK+ 2.24.10; x86_64-pc-linux-gnu) Reply-To: tor-talk(a)lists.torproject.org Hi all, Heads up on a new paper suggesting that its possible to unmask Tor users using traffic correlation: http://www.ohmygodel.com/publications/usersrouted-ccs13.pdf Code here: http://torps.github.io/ Would be interested in hearing the opinions of the core Tor develpoment team on this stuff. Cheers, Erik -- ---------------------------------------------------------------------- Erik de Castro Lopo http://www.mega-nerd.com/ -- tor-talk mailing list - tor-talk(a)lists.torproject.org To unsusbscribe or change other settings go to https://lists.torproject.org/cgi-bin/mailman/listinfo/tor-talk ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

1 0

Who bought off Zimmermann?
by StealthMonger 01 Sep '13

01 Sep '13

How ironic and sad it is that Phil Zimmermann, the author of PGP, has become so imbued with the enterprise culture that he's now so blind to the original peer-to-peer spirit of PGP that he would say things like There is no way to do encrypted e-mail where the content is protected. [1] This is simply false. If sender and receiver exchange keys out-of-band and nobody else knows the keys, the content can have cryptographically strong protection. Why would Zimmermann allow himself to be bought off? What kind of pressure is being brought to bear? Is this protracted world-class human engineering in action? [1] http://www.forbes.com/sites/parmyolson/2013/08/09/e-mails-big-privacy-probl… -- -- StealthMonger <StealthMonger(a)nym.mixmin.net> Long, random latency is part of the price of Internet anonymity. anonget: Is this anonymous browsing, or what? http://groups.google.ws/group/alt.privacy.anon-server/msg/073f34abb668df33?… stealthmail: Hide whether you're doing email, or when, or with whom. mailto:stealthsuite@nym.mixmin.net?subject=send%20index.html Key: mailto:stealthsuite@nym.mixmin.net?subject=send%20stealthmonger-key

9 11

So I discovered that my HP laptop leaks/transmits its built-in mic audio somewhere around 24Mhz
by Eugen Leitl 01 Sep '13

01 Sep '13

http://www.reddit.com/r/RTLSDR/comments/1le3if/so_i_discovered_that_my_hp_l… So I discovered that my HP laptop leaks/transmits its built-in mic audio somewhere around 24Mhz (self.RTLSDR) submitted 23 hours ago by cronek I accidentally stumbled upon a signal in the 24MHz range, appearing to be 4 carriers. I tuned to it and heard silence, then someone came into my office and started talking and I could hear them speak. The signal appeared to be coming from my other laptop (not the one running the SDR) and was pretty weak (my antenna, the crappy one that comes with the dongle, stuck to a metal stapler was right next to the HP laptop). Here's a picture Both mics transmit independently, in the picture I rubbed one mic. The signal appears to be mirrored. When I tap the microphone, or make a loud noise that would clip the preamp, the signal drifts off and then slowly comes back to its original frequency, as illustrated here (only one of the two mics drifted, if I hit it harder or clip both mics, both will drift). I'm pretty sure that if I build a nice high-gain antenna optimized for 24Mhz I would be able to pick up the sound from some distance away. The laptop is an EliteBook 8460p. I have checked identical laptops and they do not transmit at this frequency. I didn't have the time to scan the full spectrum though. I'm guessing the preamp is really crappy and somehow ends up transmitting FM at HF freqs. Anyone has any ideas about this? I work in a high security setting and having laptops transmitting audio from everyone's office/meeting room etc is a really big deal. I somewhat doubt it to be an intentional listening device due to the weird frequency drifting. For now I guess I'll just disconnect the mic preamp pcb.

2 1

Re: Who bought off Zimmermann?
by John Young 31 Aug '13

31 Aug '13

Emitting signal that "crypto works" is a hoary practice, nothing more useful than a belief in an uncrackable means of comms, used often in war and commerce and love affairs. Crypto-AG, AES, PGP, Tor, OTR, offline exchange of keys, the list is growing with each disclosure that something stinks in crypto ex-cess. Getting the best and brightest (BAB) to affirm that crypto works, say by open and limited competitions as well as by confidential testing results leaked, would be a part of that campaign. Leaking other forms of attack, like metadata, would be another part, bit by bit, authenticity heightened by obligatory redactions and vetting by quiet government consultation. Presume Snowden dribbling juicy comsec architecture and data, witting or unwitting of their ulterior purpose as beautifully crafted to appear suspicious to BABs but so tasty to be irresistable as a floating British officer corpse stuffed with secret war plans retrieved by the Germans. Until all of Snowden's booty is released and carefully studied by virulently suspicious and paranoid BABs not snared by sweet contracts to muse and declare authenticity, it cannot be seen as more than an ingenious ruse, likely with the complicity of the BABs once believed to be poorly-paid angels dancing on a pinhead. The saluatory benefit of these ruses is to shock the shit out of the lazy and arrogant comfuckers whose stake is put at risk by being left out of the ruse, not easy to do if they are lulled into complacency by admiration, handsome pay, invites to classified dances, insured and pensioned by NDAs, well, hell, why else raise a ruckus with ruses like crypto lists and fora and history confabbing at NSA. None of this is intended to impugn the few BABs who remain outside secret circles, or at least appear to do so in best and brightest ways. And don't invoke a hoary NSL as basis for silence. It does intend to impugn denial of the inevtiable failure of crypto alone or in concert with infrastructure. Remember that 1997 NSA paper foretelling the fail. Was that a ruse too? If I was a BAB looking for a edge on the competition for ruses, I might blurt that crypto deception is the essence of crypto, that is why it works so well.

2 1

[tahoe-dev] reproducible builds for Tahoe-LAFS: where do we start?
by Eugen Leitl 31 Aug '13

31 Aug '13

----- Forwarded message from Zooko O'Whielacronx <zookog(a)gmail.com> ----- Date: Sat, 31 Aug 2013 14:12:07 +0000 From: Zooko O'Whielacronx <zookog(a)gmail.com> To: tahoe-dev <tahoe-dev(a)tahoe-lafs.org> Subject: [tahoe-dev] reproducible builds for Tahoe-LAFS: where do we start? Folks: Here's some recent news: http://m.washingtonpost.com/world/national-security/us-spy-agencies-mounted… That article says that the U.S. espionage agencies have surreptitiously installed sophisticated malware on tens of thousands of remote machines, and have plans to increase that number into the millions. It is important to remember that while the U.S. espionage establishment is the one that is currently having its activities and plans exposed, it is not the only one of its kind. It is safe to assume that there are many other organizations with similar capabilities engaged in similar activities. It is also likely that some of those groups are engaged not in warfare but in industrial espionage or other kinds of theft or sabotage. In this modern world, it would be very useful if you could check whether the binaries that you are running are the same as the binaries that other people are running that were ostensibly built from the same source code. That way, implanted malware would be more likely to be exposed. This is the idea of "reproducible builds", as championed by Tor ¹, Bitcoin ², and Debian ³. LWN.net recently had a nice overview article about this: ⁴. Now: how do we start? We have a trac ticket: https://tahoe-lafs.org/trac/tahoe-lafs/ticket/2057# reproducible builds But I don't understand what the next step on the path to really protecting users. The situation we're considering here is that a user is installing Tahoe-LAFS, for example by running "sudo apt-get install tahoe-lafs" on Debian, and the computer that was used to build the tahoe-lafs Debian package had malware running on it, that inserted a backdoor into the tahoe-lafs Debian package. How can we help users to defend against that? There are lots of other packagers which provide installable versions of Tahoe-LAFS to their users. For example, the "pkgsrc/NetBSD" system ⁵, whose Tahoe-LAFS package is maintained by Greg Troxel, who reads this mailing list. If you click on the big friendly blue "Download Tahoe-LAFS" button on the front page of https://Tahoe-LAFS.org, it takes you to a menu of packages provided by different free-and-open-source operating systems. One thing that worries me about this issue is that it is one of those things were different open source projects can reasonably assume that it is Someone Else's Problem to fix this. I've often seen this: when there is an issue that spans multiple open source projects, that it is hard to make progress on that issue, since every open source project has a theory of how it ought to be fixed by some other open source project taking responsibility for it. So what can we do to push on this issue now? Regards, Zooko ¹ https://blog.torproject.org/blog/deterministic-builds-part-one-cyberwar-and… ² https://en.bitcoin.it/wiki/Release_process ³ https://wiki.debian.org/ReproducibleBuilds ⁴ http://lwn.net/Articles/564263/ ⁵ ftp://ftp.netbsd.org/pub/pkgsrc/current/pkgsrc/filesystems/tahoe-lafs/READM… _______________________________________________ tahoe-dev mailing list tahoe-dev(a)tahoe-lafs.org https://tahoe-lafs.org/cgi-bin/mailman/listinfo/tahoe-dev ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

1 0

Re: [liberationtech] Why cant email be secure? - Silent Circle Blog
by John Young 31 Aug '13

31 Aug '13

A swell beginning, for email to be merely one way to communicate, supplemented with unlimited other ways which do not require email, or for that matter, the Internet or any digital means. Presume that digital means are the easiest to fuck with, sorry, subvert, corrupt, pack with junk, surveil, harvest, store, search, forge, track, make your own list on your digital device and expect it to be violated accordingly and used against you whether you know or not, usually not. Here especially. Now the other means, non-digital, ancient and amply used and understood among those who use them although susceptible to the digital vulnerabilites if considerable more difficult: Paper Music Sound Dance Architecture Plastic arts Graphic arts Poetry Drum Glossalia Jokes Holler Gypsy Mime Chant Curse Vulgarity Sex Sin And much more everybody uses with greater facility than digital emissions. Note that conventional lanugages are not on the list because of the heavy reliance upon them to communicate and thus most heavily scutinized and attacked, usually successfully. Language is like metadata, with only its mastery the content can be followed from end to end, then the ends burgled, beat, cut, shot, persuaded to talk in plain language. Steagonagraphy is not on the list unless it is non-digital, and if not, then hiding communication has great potential. Its weakness is finding a means, non-digital, for preparation and transceiving. For example, architecture is an ancient means of communication, among its funders, designers, builders, maintainers, destructors, restorers, investors, evaluators, burgler, surveyors, surveillors, protectors, attackers, underminers, repairers, materials suppliers, excavators, and a host of participants -- the list of guilds and unions and professionals is vast -- perhaps one of the largest cohorts of quasi-private aggregations on earth lagging only farmers if taken to mean any form of human construction. I flatter myself, so do yourself likewise. Similarly, just about any specialty of human intercourse has its quasi-private, esoteric, unique means of communication. The human body specialists -- scientific, shamanistic, soulseeking -- along with its pschobabbling corollary, generates a fantastic array of marketable, if not wholly, believable garble and gibberish. Politics and law the most vivid at laying on the self-serving shit about the necessity of government and the rule of law(yers). Now back to the simple task of communicating in private. Before that, a side note, the end is near: First do not expect anyone to believe anything using the word "security." So comsec is dead due to abuse. Maybe compriv is better, understanding that privacy has become a crock of shit too. "Shit bag" (thanks to Assange) Natsec needs to go as well because it has been abused the most of all since assuming the parmount importance of a secular religion prevailing over all belief-systems with deadly weaponry, heartlessness, amorality, criminality and unaccountability, motto: fuck with it and you will die. Much evidence of motto in deed. And much evidence it will be used against its insiders. This is relevant to private communication. Natsec really hates being cut out of any kind of communication. It will use virtually unlimited means to get inside, most of them kept secret and manifestly violent if needs be. So compriv should not be promoted as capable to exclude natsec's prying, stealing, owning, using to demolish with its opponents. OTR is futile, BTW, as comsec. Wind compriv down to comchat. Then wind comchat down to comgossip, to comwhine, comjoke, comlie, comlurk, comslur, com-social engineer. You get the point. Do nothing life-threatening or natsec defying by com-whatever. Communications is owned by those who provide its means and they are owned by extremely badass natsec ritualists willing to barbecue your beloveds to share the goodness carefully prescribed in their secret manuals of unlimited warfare. In conclusion, there you have it, com-bat, the most reliable means of communication. Anything less is com-ical.

3 2

Re: [tor-talk] About time to make BitTorrent work over Tor,
by Eugen Leitl 30 Aug '13

30 Aug '13

----- Forwarded message from grarpamp <grarpamp(a)gmail.com> ----- Date: Thu, 29 Aug 2013 04:09:35 -0400 From: grarpamp <grarpamp(a)gmail.com> To: tor-talk(a)lists.torproject.org Subject: Re: [tor-talk] About time to make BitTorrent work over Tor, Reply-To: tor-talk(a)lists.torproject.org On 8/26/13, Kostas Jakeliunas <kostas(a)jakeliunas.com> wrote: > On Mon, Aug 26, 2013 at 2:46 PM, Nathan Suchy < > theusernameiwantistaken(a)gmail.com> wrote: > >> I don't want this for piracy as I have a paid VPN account that is much >> faster for that if I decide to pirate. I think we need BitTorrent though >> to >> work on Tor so Tor Users can securely share files with one another. > > > AFAIK the most obvious issue with this (among more subtle side-channel > attack / decloaking problems) is network scalability. Total relay bandwidth > available is, while seemingly increasing in general, very limited given > such use cases. [1] How does one scale BitTorrent on top of that? > ... > But perhaps there's still some discussion to be had. I'm sure this has been > discussed myriads of times, however - maybe it's worth trying to browse > through the mailing list archives. > > [1]: https://metrics.torproject.org/network.html#bandwidth Technically, Bittorrent works fine when run completely inside Tor. The resources needed at the client are reasonable (ie: cpu). The bandwidth is currently reasonably available. And onions are secure enough for people who insist on skirting copyright. That alone makes me wonder why Tor hasn't grown any long lived torrent clouds. Probably because the entry bar is high and the slower speed is beyond the scope of the typical leeching mindset. What people should know is that Tor currently can't handle it at scale in at least two areas... Transferring 1MiB causes about 7MiB worth of reduction in Tor bandwidth, plus the CPU and state for processing the circuits. You can get that back by running relays, but the vast bulk of the above users probably won't be willing or bothered to do that, let alone be able to figure out how to do it right and in conjunction with their BT app. So Tor is likely to tank from that alone. Then assuming they did run relays, the last part is dealing with N million users worth of relay and onion descriptors. That takes out more bandwidth, the dirservers, and everyone's local cpu and ram. For those reasons, it's hard to truly push mass use of p2p over Tor. Yet I think given the greater probability of a p2p influx as time goes on [1], Tor really should have some prepared design considerations on the table beyond "please don't do that", which torrenters obviously ignore. Hopefully designs can be found that aren't restrictive. [1] Pick any hot p2p app, drop N million users worth on Tor. In this thread it's BT... being driven slowly towards anonymous systems by the anti's [today, Russian blocking], enhanced by piratebrowser giving hints to millions of users "Hey, what's this Tor thing? What are these onions I see there? Hmm..." -- tor-talk mailing list - tor-talk(a)lists.torproject.org To unsusbscribe or change other settings go to https://lists.torproject.org/cgi-bin/mailman/listinfo/tor-talk ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

5 4

[Cryptography] The Case for Formal Verification
by Eugen Leitl 30 Aug '13

30 Aug '13

----- Forwarded message from "Perry E. Metzger" <perry(a)piermont.com> ----- Date: Thu, 29 Aug 2013 16:46:30 -0400 From: "Perry E. Metzger" <perry(a)piermont.com> To: cryptography(a)metzdowd.com Subject: [Cryptography] The Case for Formal Verification X-Mailer: Claws Mail 3.9.0 (GTK+ 2.24.20; x86_64-apple-darwin12.4.0) Taking a break from our discussion of new privacy enhancing protocols, I thought I'd share something I've been mumbling about in various private groups for a while. This is almost 100% on the security side of things, and almost 0% on the cryptography side of things. It is long, but I promise that I think it is interesting to people doing security work. When I was a student the first time, in the early to mid 1980s, formal verification was clearly a dead end that would never get anywhere. A boss of mine once asserted (circa 1988) that there would never be a verified program that did anything terribly interesting, and at time he seemed right. Today, there is a formally verified microkernel called seL4, a formally verified C compiler called CompCert, a formally verified experimental web browser called Quark, and lots of other stuff, much of which I doubtless don't even know about. _Things have changed_. Much of what has changed is proof technology, and it is a technology. The tools for doing formal verification are now, for the first time, just barely usable for real work on interesting programs, and getting better all the time. Over the last twenty five years, we figured out a lot of stuff people didn't know before about how to write verification tools and how to verify programs, and the results have been impressive. There are usually several arguments against formal verification: 1) We don't know what to specify, so what help does proving a buggy specification do us? 2) Who would bother writing a proof vastly larger than their program? 3) You can't prove programs of interesting size anyway. So, taking these in reverse order: For 3 ("you can't prove anything big enough to be useful!"), the Quark project: http://goto.ucsd.edu/quark/ showed you don't need to prove a program of interesting size. You can defend millions of lines of buggy code with a "software firewall" made of formally verified code. Verify the right thousand lines of code that the rest needs to use to talk to anything else, and you have very strong security properties for the rest of the code. seL4 and CompCert are clearly also quite useful programs. For 2 ("Who would bother with all that work?"), we have libraries in daily use like sqlite: https://www.sqlite.org/testing.html where the system has a fairly small amount of production code and literally 1000 times more lines of test code than production code. If you're willing to write ninety million lines of test to defend ninety thousand lines of code, formal verification is totally doable. Sure, it might not be worth it for throw away code or for your new video game or conference room scheduler where failure isn't a big deal, but it is *very* clear why you would want to do this for foundational code of all sorts. For 1 ("We'll never write a correct spec anyway, so what good is the proof?"), I think we've been suffering from sour grapes. We didn't have the ability to prove big things anyway, so why not tell ourselves that there's nothing interesting and large we could prove that would be worth proving? CompCert is a fine counterexample, a formally verified C compiler: http://compcert.inria.fr/ It works by having a formal spec for C, and a formal spec for the machine language output. The theorem they prove is that the compilation process preserves observational equivalence between the behavior of the C program and the output, which, given correct notation, is a very small theorem to write down. You might claim "so what, it is probably actually buggy as hell, the spec probably isn't really correct anyway, etc." -- except when John Regehr's group built tools to torture test C compilers, the only compiler they did *not* find bugs in was CompCert. They found hundreds of bugs each in every other compiler tested. (They actually found one, but arguably it was a bug in a Linux include file, not in the CompCert compiler.) Similarly, one might claim "there is no way to formally specify a web browser that won't be just as buggy as the web browser!", but Quark's formal verification doesn't try to show that the entire Web browser is correct, and doesn't need to -- it shows that some insecure behaviors are simply impossible. *Those* are much simpler to describe. Certainly there may be other properties that turn out to be important that no one has considered yet. However, unlike testing, if people discovered a hole in the set of theorems being proven -- some property that was important but which had not been considered -- then that could be added to what was proved, and _then the problem would be gone forever_. Verification means you get actual incremental progress that you can trust. Testing is much less powerful. (Furthermore, future systems can learn from what you did and add the needed theorem to what they prove about their own system.) I don't think the technology is up to proving huge systems correct -- a fairly unambitious C compiler or a microkernel is the current limit -- but it is up to proving the right thousand lines of code here and there without much fuss, and that might make an incredible difference in systems security if people actually take it seriously. So, if you're interested, how do you get started doing such things? At the moment, the best system for doing this sort of work is Coq: http://coq.inria.fr/ Coq is sort of a programming language (although it is not quite Turing equivalent -- all programs must be guaranteed to terminate for technical reasons), sort of a form of constructivist logic (i.e. all existence proofs construct examples, no law of the excluded middle). It uses a neat trick called the Curry-Howard isomorphism that may take some getting used to for people not exposed to modern type theory. In it, types and logical propositions are the same thing, and programs and proofs are the same thing. You can write a function that adds two numbers, or a function that proves that there are an infinite number of primes. The type of the former is clearly an integer, but the type of the latter is the theorem itself. A proof that proposition A implies proposition B is function of type A -> B -- any function that takes a proof of A and yields a proof of B is after all a proof that if A is true then B is true. (This is why all functions in Coq itself must terminate -- otherwise all types would be inhabited so all theorems would be true. That in no way restricts one's ability to build verified non-terminating programs using the system, you just have to build them by reasoning about programs that Coq itself can't execute.) Proofs in Coq are generally not written by hand, though. Instead one uses a sublanguage called the "tactic language" in which one invokes help from Coq to interactively assemble a proof, which makes doing the proof far easier. For many theorems, you can almost completely automate the proof, while for others, you need to help Coq along more. (Some of the tactics are quite amazing, "Omega" for example will prove any assertion about numbers that does not involve multiplication by a variable, aka "Presburger arithmetic".) Often, one builds software using Coq by constructing a sort of formally verified assertion about what the program would do, and then using a built in Coq facility to mechanically extract that into a working verified program written in OCaml, Haskell or Scheme. Nothing in theory prevents you from doing things many in other ways, though -- the system is quite general. Coq is, sadly, needlessly hard for the beginner. It has poor documentation, bad error messages and bad error behavior. These are not inherent problems, they're problems just with this instance of things -- people could build better if there was enough interest, and I hope that as these technologies become more popular people will build far better versions of the tools. However, bad documentation or no, at the moment, this is the right place to go I think. It is the system Quark and CompCert were built in, and not by accident. It is not for the faint of heart -- the learning curve is very steep. Still, it is quite doable. The right places to start with Coq are probably Benjamin Pierce's online Software Foundations textbook: http://www.cis.upenn.edu/~bcpierce/sf/ and, when one is done with that, possibly Adam Chlipala's online book "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ (There's also a manual for the system itself, as well as this book on Coq: https://www.springer.com/computer/swe/book/978-3-540-20854-9 ) I'm happy to give help to anyone trying to learn how to do this sort of thing -- we need more people in the world experimenting with verification if we're going to get truly trustworthy software going forward. Let me assert that we *do* need truly trustworthy software, too. We've been very, very good for years now at finding hole after hole in running code and making the systems we depend on every day into a minefield that we dare not take an unconsidered step in. Wouldn't it be nice to make some progress in the other direction? Perry -- Perry E. Metzger perry(a)piermont.com _______________________________________________ The cryptography mailing list cryptography(a)metzdowd.com http://www.metzdowd.com/mailman/listinfo/cryptography ----- End forwarded message ----- -- Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org ______________________________________________________________ ICBM: 48.07100, 11.36820 http://ativel.com http://postbiota.org AC894EC5: 38A5 5F46 A4FF 59B8 336B 47EE F46E 3489 AC89 4EC5

2 1

[cypherpunks] Signed vCards
by DataPacRat 30 Aug '13

30 Aug '13

I've just submitted the first draft of an Internet-Draft to the IETF. If it makes it through the whole editing process, it will take an existing file format used for identity-description, and adds a few details to allow crypto algorithms to be used for identity-/assertion/. It may not seem like much, but it could improve some aspects of hierarchical certificate authorities, encrypted email, and suchlike. It’s the most important thing I think I’ve been able to work on in the last little while, and I hope the editing process goes well. ---------- Forwarded message ---------- From: <internet-drafts(a)ietf.org> Date: Fri, Aug 30, 2013 at 3:33 AM Subject: New Version Notification for draft-boese-vcarddav-signedvcard-00.txt To: Daniel Eliot Boese <datapacrat(a)datapacrat.com> A new version of I-D, draft-boese-vcarddav-signedvcard-00.txt has been successfully submitted by Daniel Eliot Boese and posted to the IETF repository. Filename: draft-boese-vcarddav-signedvcard Revision: 00 Title: vCard Format Extensions : Signed vCards Creation date: 2013-08-30 Group: Individual Submission Number of pages: 11 URL: http://www.ietf.org/internet-drafts/draft-boese-vcarddav-signedvcard-00.txt Status: http://datatracker.ietf.org/doc/draft-boese-vcarddav-signedvcard Htmlized: http://tools.ietf.org/html/draft-boese-vcarddav-signedvcard-00 Abstract: The base vCard 4.0 specification defines a large number of properties. This specification adds two new parameters and six new properties to vCard 4.0, which allow the use of cryptography and public-key infrastructure (PKI) for identity assertion. Note Discussion and suggestions for improvement are requested, and should be sent to vcarddav(a)ietf.org. Please note that it may take a couple of minutes from the time of submission until the htmlized version and diff are available at tools.ietf.org. The IETF Secretariat Thank you for your time, -- DataPacRat "Then again, I could be wrong."

1 0