Prev: two definitions of RSA?
Next: It's not science, it's sci.
From: Rainer Urian on 3 Feb 2010 15:47
Hi,
I think, this article of N. Koblitz is very enilghtening ....
www.ams.org/notices/200708/tx070800972p.pdf


"Kristian Gj�steen" <kristiag+news(a)math.ntnu.no> schrieb im Newsbeitrag
news:hk7io5$b8n$1(a)orkan.itea.ntnu.no...
> Simon Johnson <simon.johnson(a)gmail.com> wrote:
>>However, I feel that some people write the papers in such a way as
>>they don't want them to be understood.
>
> I don't think it's intentional. Certainly not for me. But most people
> could put more effort into presentation.
>
> --
> Kristian Gj�steen

From: Paul Rubin on 4 Feb 2010 23:19
Kristian Gjøsteen <kristiag+news(a)math.ntnu.no> writes:
> That said, there is an argument for applying formal methods and
> computer verification to cryptographic protocols. In my experience,
> I lose confidence in my "proofs" as my cryptographic protocols become
> more complicated. Formal, automatically verifiable proofs may work
> well here.

Quite a lot of programming language theory papers these days include
machine-checked proofs. I've been wondering wondering why they're not
more common in cryptography. Any idea?
From: Greg Rose on 5 Feb 2010 01:15
In article <7xaavotiu3.fsf(a)ruckus.brouhaha.com>,
Paul Rubin <no.email(a)nospam.invalid> wrote:
>Kristian Gjøsteen <kristiag+news(a)math.ntnu.no> writes:
>> That said, there is an argument for applying formal methods and
>> computer verification to cryptographic protocols. In my experience,
>> I lose confidence in my "proofs" as my cryptographic protocols become
>> more complicated. Formal, automatically verifiable proofs may work
>> well here.
>
>Quite a lot of programming language theory papers these days include
>machine-checked proofs. I've been wondering wondering why they're not
>more common in cryptography. Any idea?

Very little in cryptography is actually reducible
to axioms. It's very difficult to state things like
"factoring is hard" in a way that provers can use.

Greg.
--
Greg Rose
232B EC8F 44C6 C853 D68F E107 E6BF CD2F 1081 A37C
From: Paul Rubin on 5 Feb 2010 02:08
ggr(a)nope.ucsd.edu (Greg Rose) writes:
> Very little in cryptography is actually reducible
> to axioms. It's very difficult to state things like
> "factoring is hard" in a way that provers can use.

One idea is to formalize reduction-based proofs: if there is a function
that breaks this new protocol, then it can be used as an oracle to
factor arbitrary numbers, or break some existing believed-secure
protocol, etc.
From: Mok-Kong Shen on 5 Feb 2010 04:19
Paul Rubin wrote:
> Kristian Gjøsteen<kristiag+news(a)math.ntnu.no> writes:
>> That said, there is an argument for applying formal methods and
>> computer verification to cryptographic protocols. In my experience,
>> I lose confidence in my "proofs" as my cryptographic protocols become
>> more complicated. Formal, automatically verifiable proofs may work
>> well here.
>
> Quite a lot of programming language theory papers these days include
> machine-checked proofs. I've been wondering wondering why they're not
> more common in cryptography. Any idea?

The goal of a math proof is to show something to be either true or
false, not something "in-between". However, in crypto, with the
exception of the theoretical OTP, nothing is absolutely perfectly
secure. Could this be a problem of application of machine proofs
to crypto? (Maybe there exist systems of proofs in fuzzy logics etc.
but I don't know.)

M. K. Shen


First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: two definitions of RSA?
Next: It's not science, it's sci.