[Openid-specs-heart] HEART WG AGENDA Monday April 20, 2020

Wed Apr 22 07:13:10 UTC 2020

Hi Debbie,

Am 21.04.20 um 22:15 schrieb Debbie Bucci:
> Tom,
>
> Given you raised the concern in the first place - is there a specific
> document  - section of FAPI 2.0 spec you are referring to?  This
> article seem rather broad. Its up to the organization to do their own
> risk assessment - preferably based on recognized frameworks NIST/ISO
> etc.      Given many of us have experience with this type of analysis
> - what are you comparing it too? 

I'm not Tom, but maybe I can help to clarify this.

He is referring to the FAPI 2.0 Attacker Model draft that has been
adopted by the FAPI working group [1].

One of the "lessons learned" from FAPI 1.0 was that there is a need for
a clear definition of which attacks the protocol aims to defend against
(and which not). More specifically, that was one of the takeaways from
an detailed security analysis of FAPI 1.0 [2]. In this paper, of which I
am a coauthor, we used formal methods that enable a very comprehensive
and in-depth analysis of the security properties of web protocols. We
previously used the same methods to find the mix-up and code injection
attacks on OAuth [3], to verify the security of OpenID Connect [4], and
other protocols [5,6,7].

Formal analysis of web protocols is a relatively young field with a lot
of pioneering work still to do. In general, however, formal methods are
a very well-established standard tool in network protocol security. For
example, formal models were very successfully used to develop and secure
TLS 1.3. Formal analysis requires a defined attacker model to verify the
protocol's security against. Within the bounds of the model, formal
methods can the provide very strong security guarantees. But it is not
the purpose of the attacker model to hide other potential attacks. The
attacker model itself rather tells us about the boundaries of the formal
guarantees where we then have to apply other methods.

For FAPI 2.0 I wrote down the attacker model to inform decisions in the
protocol design, to enable a formal analysis of FAPI 2.0, and to tell
readers where the boundaries of the guaranteed security are.

To address Tom's concerns: Neither the attacker model itself nor a
formal analysis obsoletes a thorough risk analysis and all the other
methods we have to secure deployments, but they complement each other.
Formal methods provide guarantees on protocols - in isolation! - whereas
organizational risk analyses and other security measures are needed to
secure deployed systems. (You can't pentest a piece of paper.)

- Daniel

[1] https://bitbucket.org/openid/fapi/src/master/FAPI_2_0_Attacker_Model.md

[2] https://arxiv.org/abs/1901.11520

[3] https://arxiv.org/abs/1601.01229

[4] https://arxiv.org/abs/1704.08539

[5] https://arxiv.org/abs/1403.1866

[6] https://arxiv.org/abs/1411.7210

[7] https://arxiv.org/abs/1508.01719

>
> On Tue, Apr 21, 2020 at 2:01 PM Tom Jones
> <thomasclinganjones at gmail.com <mailto:thomasclinganjones at gmail.com>>
> wrote:
>
>     not in this forum - it is not appropriate.
>     Peace ..tom
>
>
>     On Tue, Apr 21, 2020 at 10:51 AM Daniel Fett <fett at danielfett.de
>     <mailto:fett at danielfett.de>> wrote:
>
>         https://cacm.acm.org/magazines/2020/4/243625-why-is-cybersecurity-not-a-human-scale-problem-anymore/fulltext
>
>         Could you please elaborate in which way this article critizes
>         the attacker model used in formal protocol security analyses?
>         This critique must then apply equally for the way in which TLS
>         1.3 was designed and evaluated (see, e.g.,
>         https://tools.ietf.org/html/rfc8446#appendix-E).
>
>         -Daniel
>
>         Am 21.04.20 um 19:41 schrieb Tom Jones:
>>         DOI:10.1145/3347144.  CACM 63 no 4 p 30ff
>>         Peace ..tom
>>
>>
>>         On Tue, Apr 21, 2020 at 10:38 AM Daniel Fett
>>         <fett at danielfett.de <mailto:fett at danielfett.de>> wrote:
>>
>>             Am 21.04.20 um 18:30 schrieb Tom Jones:
>>>             Well, I am a member of the FAPI wg and do not like their
>>>             current direction. Specifically I strongly disagree with
>>>             Fett's attack model which has come under increasing
>>>             attack in, for example the current issue of the CACM.
>>
>>             Which article?
>>
>>             _______________________________________________
>>             Openid-specs-heart mailing list
>>             Openid-specs-heart at lists.openid.net
>>             <mailto:Openid-specs-heart at lists.openid.net>
>>             http://lists.openid.net/mailman/listinfo/openid-specs-heart
>>
>
>     _______________________________________________
>     Openid-specs-heart mailing list
>     Openid-specs-heart at lists.openid.net
>     <mailto:Openid-specs-heart at lists.openid.net>
>     http://lists.openid.net/mailman/listinfo/openid-specs-heart
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.openid.net/pipermail/openid-specs-heart/attachments/20200422/ba1330fb/attachment-0001.html>