Prev: two definitions of RSA?
Next: It's not science, it's sci.
From: Tom St Denis on 5 Feb 2010 07:43
On Feb 5, 1:15 am, g...(a)nope.ucsd.edu (Greg Rose) wrote:
> In article <7xaavotiu3....(a)ruckus.brouhaha.com>,
> Paul Rubin  <no.em...(a)nospam.invalid> wrote:
>
> >Kristian Gjøsteen <kristiag+n...(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.

I think it's hard to state factoring is hard regardless of writing
style because that has NEVER been proven to be true.

Tom
From: Kristian Gj�steen on 5 Feb 2010 12:19
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?

I'm guessing that you need to adapt the techniques to apply to
cryptographic proofs as they are currently phrased.

--
Kristian Gj�steen
From: WTShaw on 9 Feb 2010 04:04
On Feb 5, 11:19 am, Kristian Gjøsteen <kristiag+n...(a)math.ntnu.no>
wrote:
> Paul Rubin  <no.em...(a)nospam.invalid> wrote:
>
> >Kristian Gjøsteen <kristiag+n...(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?
>
> I'm guessing that you need to adapt the techniques to apply to
> cryptographic proofs as they are currently phrased.
>
> --
> Kristian Gjøsteen

Having used several computer languages in writing crypto, I have long
ago become aware that hand calculated values are at times necessary to
verify that machine results are true. From my experience as a digital
designer, the physics and pointed hat wizardry to get layouts right
can't be assumed. Delicate wiring loops can cause improper results.
As for languages, sins by omission on the part of programmers can be a
problem, surely for different versions and platforms. It's a pain to
verify but necessary, even more to validate your own programs by
trying them on different machines, systems, and any other available
variations. Theory goes nowhere without field testing.

Yes in reference to proving induction, somewhere mentioned the above
entries, surely such might sometimes be done with deduction especially
as those classes of algorithm usage, not necessarily the inverse or
with forward acting inductions with escape mechanisms.
First  |  Prev  | 
Pages: 1 2 3 4 5
Prev: two definitions of RSA?
Next: It's not science, it's sci.