Re: [Lake] Security levels for EDHOC for formal verification

John Mattsson <john.mattsson@ericsson.com> Thu, 11 February 2021 16:01 UTC

Return-Path: <john.mattsson@ericsson.com>
X-Original-To: lake@ietfa.amsl.com
Delivered-To: lake@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 0FAAB3A16F1 for <lake@ietfa.amsl.com>; Thu, 11 Feb 2021 08:01:18 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.35
X-Spam-Level:
X-Spam-Status: No, score=-2.35 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIMWL_WL_HIGH=-0.25, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_PASS=-0.001, URIBL_BLOCKED=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (1024-bit key) header.d=ericsson.com
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id OQTOa1NIzhAH for <lake@ietfa.amsl.com>; Thu, 11 Feb 2021 08:01:16 -0800 (PST)
Received: from EUR01-HE1-obe.outbound.protection.outlook.com (mail-he1eur01on0620.outbound.protection.outlook.com [IPv6:2a01:111:f400:fe1e::620]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 8453C3A16EC for <lake@ietf.org>; Thu, 11 Feb 2021 08:01:15 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=AK5hLNFvmWFahndp1Rmbva1sL5VG3h/aPtqbr3TqVE5wpzpzBuK1oWtVKWe2VyddcOgV8xXY0TmQ+ojYPbEnwD6uzdUuaynhLh8JHmO9NUlNZJwoYZsJ++g6V2tSvEx6Rg5sOv7B77iU2r1A5v11tixj/iDpdCjw9fV3dKOEbUp6Lfp7hfnz83ScDMJfYZkAkjq6rWLPQNX854BrPGp7kwgcGeKD7bFNyYRTbA0CByPoxuDbmSlOWUVo/EHVTJELqkfE8QJjh26hzK+gYV+v1V54IiFa/Lp9KL86xuVOGYwvqVFlP+2R2iL+gArHUt9jY2cvMuWLYz56ao64a724YA==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=KmaGZKUR86E5qEnOa5zWk8PM9atfB4LRPnFF7YFooH4=; b=DkymfsyXSjJqw/gDlJFUTXNDEVqfqSr1ML1n6x9LfQdDziVKgE1JYwI0VmyVXQ1Q/vEPaDIpqt38KauOP9Ox7TpMFmqua2DF+ctYhB2xsWpoOmFDOBykKQys8kt1JY+HCa/rXFG+bAULlO6E1UZ2o0srLgynbzw3wTYl42ZQaLrXAUWZHdOsAeNsN7lZMN3TklXuLBvzwjxy7jJqf5c353ngUpRwm18cv7brcJ5cEFQyzS49wx3q9oczFaVFnc8452nE75o+i4gGNKuSv9gMn9cyIe1FEevjPueM7tSutB5JCckZw2YSvdGvLNiDWa6OVSC0E5NiAV9ejlOm0r1QDA==
ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=ericsson.com; dmarc=pass action=none header.from=ericsson.com; dkim=pass header.d=ericsson.com; arc=none
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ericsson.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=KmaGZKUR86E5qEnOa5zWk8PM9atfB4LRPnFF7YFooH4=; b=DE+7wuM+enNW3wJxNdyinmaCbY09HoAD834XqFpad9hGCnzJ+CBEM4OK10PUvLbTcRN81elPKI+83fjxXytkPsrCgweS9JPUgfb385eC3BWqGM11jlFBl9NlqMPwwWXG4sA2p+WHaWOCsspLygTquDuY5LxWVBkpgw5cgaGWPs0=
Received: from (2603:10a6:3:4b::8) by HE1PR07MB4362.eurprd07.prod.outlook.com (2603:10a6:7:9a::30) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.3825.15; Thu, 11 Feb 2021 16:01:08 +0000
Received: from HE1PR0701MB3050.eurprd07.prod.outlook.com ([fe80::c555:6e47:970c:1268]) by HE1PR0701MB3050.eurprd07.prod.outlook.com ([fe80::c555:6e47:970c:1268%11]) with mapi id 15.20.3846.027; Thu, 11 Feb 2021 16:01:07 +0000
From: John Mattsson <john.mattsson@ericsson.com>
To: Rene Struik <rstruik.ext@gmail.com>, "lake@ietf.org" <lake@ietf.org>
Thread-Topic: [Lake] Security levels for EDHOC for formal verification
Thread-Index: AQHXAE3CIo84kXTI0k20kQP+0TZxfqpTDgUAgAAgWYA=
Date: Thu, 11 Feb 2021 16:01:07 +0000
Message-ID: <3E4FB0B6-DB20-4072-9208-D58B1BA027A4@ericsson.com>
References: <87582CFB-7166-49DB-85F1-E6D389A966F0@ericsson.com> <fce0ff38-3ad0-49f2-3555-67e3926aac76@gmail.com>
In-Reply-To: <fce0ff38-3ad0-49f2-3555-67e3926aac76@gmail.com>
Accept-Language: en-US
Content-Language: en-GB
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
user-agent: Microsoft-MacOutlook/16.45.21011103
authentication-results: gmail.com; dkim=none (message not signed) header.d=none;gmail.com; dmarc=none action=none header.from=ericsson.com;
x-originating-ip: [81.225.97.222]
x-ms-publictraffictype: Email
x-ms-office365-filtering-correlation-id: 92805d9a-ec16-44b9-64ac-08d8cea63e62
x-ms-traffictypediagnostic: HE1PR07MB4362:
x-microsoft-antispam-prvs: <HE1PR07MB436229EF6A96FB04CA84E469898C9@HE1PR07MB4362.eurprd07.prod.outlook.com>
x-ms-oob-tlc-oobclassifiers: OLM:10000;
x-ms-exchange-senderadcheck: 1
x-microsoft-antispam: BCL:0;
x-microsoft-antispam-message-info: N/rG3aU7E+nO9/hPyDfo3nMBIK6ieSQMAvYu9MrlIUMMi0Wy9fsmnINrTPGJfBYg+c6Ueqapi30Ocfd+dqFPDqLqnH+IDECWvHXE83mXkpgXSmkI1gf7LXqE/RWlkubUcyKYZ+kLiv24XxGs38DsNZaLi4mcMhfeG9fIS51z2GK+mDYxsy3fdTRxDomxRY4hhjlko9CsGoFXIh+OstW/y7Y4Y567CDiTvcAWMojKCE8S89HJTnyFsLdo4Q2S8HE4yoUJObGl5UgL8cMMsNHCDAV86Zx/H+QuPM5OceHZ4Krwnpdco7SOsZQYmKuWyMtqN19DsIDUAyVqqCiJgg9pG8Phch9Y0giDZxhPLwEddq30LLNJtEAQbVDbdYrGcdrMinWgpHMJAwqzeqQvUytvdCoYbJ15hDnbH0x7RiteDv1muFJF4Xmt89S/b8NZZziHtjmj460su4Xx63iPkYlLwQv16QzE2ftG2RBmVmPznYcrOT4lscg0MvDIRy3QskhdhNImHjnVZXC1sOab74bW76Tqlombji6XGiwdg5IxzJlcKDiHxDRuGGrY30xi8xL+BOlumEyWrx9tsjKt7YxvG/2Dv0ukveAZblo8lDBZTGrr+TJbXYgfnnSgx/eiu3f3QB2Vde9T1+SW2DH31YdESA==
x-forefront-antispam-report: CIP:255.255.255.255; CTRY:; LANG:en; SCL:1; SRV:; IPV:NLI; SFV:NSPM; H:HE1PR0701MB3050.eurprd07.prod.outlook.com; PTR:; CAT:NONE; SFS:(4636009)(136003)(39860400002)(376002)(346002)(396003)(366004)(8676002)(6512007)(6506007)(53546011)(2616005)(26005)(44832011)(478600001)(966005)(186003)(316002)(110136005)(66946007)(66476007)(86362001)(36756003)(5660300002)(71200400001)(76116006)(66556008)(66446008)(64756008)(33656002)(83380400001)(2906002)(15650500001)(8936002)(6486002)(45980500001); DIR:OUT; SFP:1101;
x-ms-exchange-antispam-messagedata: =?utf-8?B?R2ZISUgxcGl6eGVUNlIrSXA2SmNHdEs3MkEyRko3eis0a2JKUTYzTVUxa2Zh?= =?utf-8?B?bmYzMnNuU0NFa1EyNitpNDRZMU9wS2czQ2Z3OEhYUFM2Ukk2MWk0WUFDVVpK?= =?utf-8?B?Q3BUMTh0U0dnUnkvbkJsYXI0UTdsb0MvbmxtU0RRN3JsS0hkMU1NVkNLdTZB?= =?utf-8?B?anIwTFdYSVhBZWg0dnQwWVJ1S0ZiV2wyR2cvTDhaOE0xcUtPcnQxQVVZRUl6?= =?utf-8?B?RkFoellXRUhnaDdRVS9tN05uVmM4aFJMT25qbWRJbEZZZGwwRmFUSk42S0gw?= =?utf-8?B?czkya0JBc2IxRGZKRVRvU09MLytOQVpsMkFHT3FrbFNOTkpONEsrVFlIYkQ3?= =?utf-8?B?NEI3aUdRRGZyejJQc0pQaTBxNW1kMWdCYnlab0ptR1d4SnlZdjJVRzZpbEZw?= =?utf-8?B?MXNXdWliR2lYRG16cVRkaGhtU1FjQWxEejVNc3ljaTQ2dk52aXAyWER6dzJy?= =?utf-8?B?L3lWUW1yUHlQUjc0MkJZaEQzMVM4bnVBTlBkVTlsd1BXREwxNGpUNG9XZVNL?= =?utf-8?B?emNWcm0yMU03bXowMXF6VkRLc3MzS0REMjA0NysxNnpqZEppYjdUT1RYN2Jt?= =?utf-8?B?TlhLM2o1Y3V6aFpqQVBVNnhaaXZMazNVSUkyanM4emtabTZCSG4ycWZRenlm?= =?utf-8?B?Wm1PWFo1c2YzQmpDU0pNanJXL0hIcFZXVWFjdzY3M3lVN1A2NzFUNGNRREZL?= =?utf-8?B?M0NmSS9Qd0pFV2RwbE1udGM1NVJHNUxoVWdvZ0dhRDdURXNQMEVkQ0VzSXRO?= =?utf-8?B?WHZwOVRLN2JDdG9Qc0ZZTURnZXpzM3pDaTVVZU5VOVdvZnpLS3F1SC9VaVpa?= =?utf-8?B?dFZvTjNqd0k4VHVhdWF3dWUzbFJablc5SE13dVVCSGY1ckxjOU9YcXNXRjdO?= =?utf-8?B?L2ZqTUVWTkFyZ1IrNUx0bW9PVUpwNDZoTnJYVENiTkxYVUYrbzY2UTR2Tzc0?= =?utf-8?B?OThUWmRBbFFWNnByUEZMYmprNzBUbGhqZTExVHhJVXladjFJU1JmSUJiMlFR?= =?utf-8?B?NWsrMG1Jb0lXTWZOWkV3dG1HSXhCREdZejdqS0oxbXYrcGU0cDBHT3RrZjJJ?= =?utf-8?B?UkpSMzcwL0Nnem5YWlFocnZqOXpEbHlwUDQyVVVZOXo2bkw2MjVidElKRzlS?= =?utf-8?B?SzdtejVZb0VFMlJBLzFMRFNoQjdoaE93Qy82a1QrOGV3cSs2aVptUEhySk8z?= =?utf-8?B?bzZ1Q3gvRTZ1TUxDd3JLZ1g3WU1FSXFOUS9rOFpxNlVkTkpaQlh2Skh2S2dq?= =?utf-8?B?WW5hcEhicnl0ZzVXR0NBZjBwaWdIQTRWWG9WdjFEeFowMEFkTWI1YmZxUGhY?= =?utf-8?B?LzdtVStXdlpJenN1dGRwbEhKSjMrQjZWdlh5U2pVUjdqTkdZVFpISXhOZHpj?= =?utf-8?B?MzhFaWhkMm5CWUphZHNFaHBib3d5Y0ZQU3RwQkpzS2tMZXZoRlljYVhGcllo?= =?utf-8?B?SEY4SzBjVzI0ajM3bGoyV29pbUJCVG5SOE8raXNTeUJYYTZYM2gxQTFpVkk0?= =?utf-8?B?SnRTaU0zQjlYZzBhcThFbVdQMEZ5dEw4VERnTXNzS0xOSUNjSi9lZ2xlWW5x?= =?utf-8?B?bXpVWVN1QU1rOExteStqVktZYVNmSEVGYjdUa3hPK0FwUkE2Z3d4UmpJTXht?= =?utf-8?B?ckJqUHdRMmJSNzlzNFM3c056QmtPVzdzN1dua29MODVFcmdURERWNGxTTC81?= =?utf-8?B?RFZrWk5MekxsWXA1d3dzcWNjaVFBQ0xSeHBiUTdKWFh5S09ZMUh2blR0UGZV?= =?utf-8?Q?j9d5ynbGmukTHuKnQcy6KKI5X/Zso6ae1Pf7zXZ?=
x-ms-exchange-transport-forked: True
Content-Type: text/plain; charset="utf-8"
Content-ID: <D0843FE0CA2F20419ADFE30BA2089449@eurprd07.prod.outlook.com>
Content-Transfer-Encoding: base64
MIME-Version: 1.0
X-OriginatorOrg: ericsson.com
X-MS-Exchange-CrossTenant-AuthAs: Internal
X-MS-Exchange-CrossTenant-AuthSource: HE1PR0701MB3050.eurprd07.prod.outlook.com
X-MS-Exchange-CrossTenant-Network-Message-Id: 92805d9a-ec16-44b9-64ac-08d8cea63e62
X-MS-Exchange-CrossTenant-originalarrivaltime: 11 Feb 2021 16:01:07.7984 (UTC)
X-MS-Exchange-CrossTenant-fromentityheader: Hosted
X-MS-Exchange-CrossTenant-id: 92e84ceb-fbfd-47ab-be52-080c6b87953f
X-MS-Exchange-CrossTenant-mailboxtype: HOSTED
X-MS-Exchange-CrossTenant-userprincipalname: pJcj3HMx0iUWVIIJAKeD2XcBL8MRirh4r5r6+0FclP/39FaQvrH/8fK7wQBbX/qTWGDwkcg+f+TYVNqMWTwesSG3X/CkvDlheg1FQ+iJ+nI=
X-MS-Exchange-Transport-CrossTenantHeadersStamped: HE1PR07MB4362
Archived-At: <https://mailarchive.ietf.org/arch/msg/lake/UYaV56yxz_zUWOqU32SoVozSw4I>
Subject: Re: [Lake] Security levels for EDHOC for formal verification
X-BeenThere: lake@ietf.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Lightweight Authenticated Key Exchange <lake.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/lake>, <mailto:lake-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/lake/>
List-Post: <mailto:lake@ietf.org>
List-Help: <mailto:lake-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/lake>, <mailto:lake-request@ietf.org?subject=subscribe>
X-List-Received-Date: Thu, 11 Feb 2021 16:01:18 -0000

Hi Rene,

-----Original Message-----
From: Rene Struik <rstruik.ext@gmail.com>
Date: Thursday, 11 February 2021 at 16:06
To: John Mattsson <john.mattsson@ericsson.com>om>, "lake@ietf.org" <lake@ietf.org>
Subject: Re: [Lake] Security levels for EDHOC for formal verification

Hi John:

Perhaps, it would be good adding ECDSA w/ SHA256 and Wei25519 to the mix 
(i.e., add Wei25519 to the list "EDHOC signature algorithm curve" - see 
[1], Suite Z).

[John] Yes, I just missed to add it there. Wei25519 is expected to be standardized for use with ECDSA in COSE.

If I understand correctly, the formal analysis assumes specific 
properties (such as - with signature schemes - existential 
unforgeability under chosen message attack). If so and if ECDSA is 
instantiated as specified in FIPS 186-4, this should not make a 
difference for the analysis, compared to analyzing ECDSA w/ SHA256 and 
P-256.

[John] That is my understanding as well. I assume P-256, Ed25519, secp256k1, and Wei25519 might all be treated the same.

One note: technically, one could use secp256k1 not just for signing, but 
also for key agreement (below, this curve as only allowed for signing).

[John] Yes, but COSE decided to specify secp256k1 for ECDSA only. EDHOC is not planning to change this.

Ref: [1] 
https://datatracker.ietf.org/meeting/interim-2020-lake-04/materials/slides-interim-2020-lake-04-sessa-ecc-cipher-suites-01.pdf

Rene

On 2021-02-11 3:13 a.m., John Mattsson wrote:
> Hi,
>
> There was a request from Karthik to have specified security levels for EDHOC so that formal verification can verify or falsify the claims. This is not trivial. Below is a first try. Let's discuss if this is enough or if more or different information is needed.
>
> The design objectives of EDHOC has been to have approximatly the same security level as TLS when the same algorithms are used, but to have much smaller messages. Just like TLS I think the expected security level depends heavily on the chosen algorithms and the method. Method 3 should be comparable with TLS 1.3 with mutual certificate based authentication. Methed 0 is a bit trickier to compare to TLS.
>
> In general there should not be much difference between EDHOC and TLS 1.3 when certificate based authentication is used. The exported keys should be a bit stronger as EDHOC include message_2 and the for Static DH also the private authentication keys. The Static DH Method with 64 bit tags does not offer the same security level as TLS 1.3 with certificate-based authentication, but should offer better security than TLS 1.3 with PSK authentication and short tags.
>
> EDHOC can use all algorithms defined for COSE (but maybe you will restrict your work to
> the pre-defined cipher suites). Below are the relevant algorithms defined for COSE.
>
> EDHOC AEAD algorithm:
> ---------------------------
> AES-CCM-16-64-128
> AES-CCM-16-64-256
> AES-CCM-64-64-128
> AES-CCM-64-64-256
> AES-CCM-16-128-128
> AES-CCM-16-128-256
> AES-CCM-64-128-128
> AES-CCM-64-128-256
> A128GCM
> A192GCM
> A256GCM
> ChaCha20/Poly1305
>
> EDHOC hash algorithm
> ---------------------------
> SHAKE256
> SHA-512
> SHA-384
> SHAKE128
> SHA-512/256
> SHA-256
> [SHA-1 and SHA-256/64 not allowed]
>
> EDHOC ECDH curve
> ---------------------------
> P-256
> P-384
> P-521
> X25519
> X448
> Wei25519 (expected to be registered soon)
> [Ed25519, Ed448, secp256k1 are not allowed]
>
> EDHOC signature algorithm
> ---------------------------
> ES256
> ES512
> ES384
> EdDSA
> ES256K
>
> EDHOC signature algorithm curve
> ---------------------------
> P-256 (ECDSA only)
> P-384 (ECDSA only)
> P-521 (ECDSA only)
> Ed25519 (EdDSA only)
> Ed448 (EdDSA only)
> secp256k1 (ECDSA only)
> [X25519, X448 are not allowed]
>
> (Non-ECC signatures algorithms are supposed to be allowed as well. I think the draft needs to be updated.)
>
> Below are two initial ways to express the security level, one as a function of the Mehtod and algorithms. The second as a comparision with TLS 1.3. In general, EDHOC with the weakest options SHALL offer 64-bit security against on-line attacks and 128-bit security against off-line attacks. I think this aligns with TLS 1.3.
>
> Let me know if this is enough for the formal verification, if you need something different, or if something is missing. It would be good if somebody reviews the information is this mail.
>
>
> EDHOC security levels for different aspects
> ---------------------------
>
> The security level of confidenciality protection against passive attackers should be the key length of the AEAD (128, 192, or 256 bits).
>
> The security lebel of integrity protection and confidentiality against active attackers should be the tag length of the AEAD (64 or 128 bits)
>
> The authentication security in the static DH modes are determined by the  tag length of the AEAD (64 or 128 bits)
>
> The authentication security in the Signature Key modes are determined by the security level of the signature algorithm (128, 192, or 256 bit)
>
> The integrity protection of some fields are detemined by the security level of the signature algorithm (128, 192, or 256 bit).
>
>
>
> EDHOC security levels compared with TLS 1.3
> ---------------------------
>
> Method 0 (2* Signature Key ) should offer the same security level as TLS 1.3 with the same algorithms.
>
> 0. (AES-CCM-16-64-128, SHA-256, X25519, EdDSA, Ed25519)
> 1. (AES-CCM-16-128-128, SHA-256, X25519, EdDSA, Ed25519)
> 4. (A128GCM, SHA-256, X25519, ES256, P-256)
> 5  (A256GCM, SHA-384, P-384, ES384, P-384)
>
>
> Method 0 (2* Static DH Key ) is a bit trickier.
>
> 0. (AES-CCM-16-64-128, SHA-256, X25519, EdDSA,
>
> The authentication security level here is bounded by the 128-bit tag. Should offer at least the same security level as TLS 1.3 with PSK authentication with CCM_8, and the other algorithms the same.
>
> 1. (AES-CCM-16-128-128, SHA-256, X25519, EdDSA, Ed25519)
> 4. (A128GCM, SHA-256, X25519, ES256, P-256)
>
> Should both offer similar security level as TLS 1.3 with certificate authentication and the the other algorithms the same.
>
> 5	(A256GCM, SHA-384, P-384, ES384, P-384)
>
> The authentication security level here is bounded by the 128-bit tag.
>
> Cheers,
> John
>
>

-- 
email: rstruik.ext@gmail.com | Skype: rstruik
cell: +1 (647) 867-5658 | US: +1 (415) 287-3867