Analysis of Industrial Protocols Cuellar, Tschofenig Siemens Automated

Analysis of Industrial Protocols Cuellar, Tschofenig Siemens Automated Validation of Internet Security Protocols and Applications Shared cost RTD (FET open) project IST-2001-39252

2 Context: Standardisation Committees for Internet Protocols OMA W3C html IETF xml HTTP TCP UDP IP 3GPP 802.11 GSM IEEE They are all doing a good job, but . Seoul, March, 2004 AVISPA IETF - saag

3 They need help Even using perfect cryptographic algorithms – they may be used in insecure ways. Errors in security are very costly: – Updates are costing hundreds of millions, e.g. WLAN/WEP – Other protocols are delayed by years, e.g. Mobile-IP, Geopriv – Eroding confidence in Internet Security and e-commerce Security protocol design is very difficult, needs – abundance of caution, – experienced cryptographers and security protocol designers – and fast, scalable, and usable protocol analysis tools! This is where AVISPA is making the difference Seoul, March, 2004 AVISPA IETF - saag

4 Project Objectives 1. Develop a rich specification language for formalising industrial strength security protocols and their properties. 2. Advance state-of-the-art analysis techniques to scale up to this complexity. 3. Develop the AVISPA tool based on these techniques. 4. Tune and assess the AVISPA tool on a large collection of practically relevant, industrial protocols. 5. Migrate this technology to developers and standardisation organisations. Seoul, March, 2004 AVISPA IETF - saag

5 Coverage of the AVISPA Protocol Candidates The IETF, IEEE, 3GPP, OMA etc. need tools that cover a wide range of protocols and security properties: 11 different areas (in 33 groups) 5 layers 20 security goals (as understood at IETF, 3GPP, OMA, etc) Seoul, March, 2004 AVISPA IETF - saag

6 Areas Infrastructure (DHCP, DNS, BGP, stime) Network Access (WLAN, Pana) Mobility (Mobile IP, HIP, Seamoby) VoIP, messaging, presence (SIP, ITU-T H530, impp, simple) Internet Security (IKE, IKEv2, UMTS-AKA, TLS, Kerberos, EAP & EAP Methoden, OTP, Sacred, ssh, telnet,.) Privacy (pseudonym agreement protocols) AAA, Identity Management, Single Sign On (Liberty Alliance) Security for QoS and NAT/FW signaling, etc. (NSIS) Broadcast/Multicast Authentication (TESLA) E-Commerce (Payment) Perhaps: Secure Download, Content protection (DRM) Seoul, March, 2004 AVISPA IETF - saag

7 Layers impp impp Application SET SIP / http SIP / http Middleware Kerberos tcp / udp tcp / udp Transport Layer ip ip Ethernet Ethernet Network Layer Data Link Layer TLS IPsec-IKE WLAN-Wep Physical Layer Host Seoul, March, 2004 Access Point, Gateway or Host AVISPA IETF - saag

8 Security Goals Authentication Secrecy (unicast multicast) – Peer Entity , Data Origin, Implicit Destination Authn, Replay Protection Key Agreement Properties – Key authentication (implicit key authentication) – Key confirmation (Key Proof of Possession) – Fresh Key Derivation (key freshness) “Anonymity” (aka passive user identity confidentiality) – Identity Protection against Eavesdroppers Non-repudiation – Proof of Origin – Proof of Delivery All of them reduce to classical authentication secrecy properties Seoul, March, 2004 AVISPA IETF - saag

9 Security Goals Authentication Secrecy (unicast multicast) Authorisation (by a Trusted Third Party) Key Agreement Properties – Perfect Forward Secrecy (PFS) – Secure capabilities negotiation (Resistance against Downgrading and Negotiation Attacks) “Anonymity” – Identity Protection against Peer Non-repudiation – Proof of Origin – Proof of Delivery – “Accountability” Limited DoS Resistance Sender Invariance Safety Temporal Property Seoul, March, 2004 In some cases they reduce to classical authentication secrecy properties, but other properties may also be necessary. AVISPA IETF - saag

10 Security Goals Authentication Secrecy (unicast multicast) Authorisation (by a Trusted Third Party) Key Agreement Properties – Perfect Forward Secrecy (PFS) – Secure capabilities negotiation (Resistance against Downgrading and Negotiation Attacks) “Anonymity” – Identity Protection against Peer Non-repudiation – Proof of Origin – Proof of Delivery – “Accountability” Limited DoS Resistance Sender Invariance Safety Temporal Property Session Formation Consistent View (synchronization) Key naming Seoul, March, 2004 AVISPA IETF - saag

11 Coverage of established IETF Security Specifications IETF Source I AB Rec ommendation (RFC 2316) AVISPA "Core" "Useful" Sec urity mec hanisms (RFC 3631) Authentic ation Mechanisms (draft- iab- auth- mech- 02.txt) No of different Specifications containers 5 prim itives Sys tem s 1 9 2 8 2 18 3 24 3 3 2 Other Total 1 7 3 17 1 13 21 3 4 Firewalls , 4 GSS, has hes , Sas l, EAP s ignatures , trans vers al PGP, certificate API CMP, profiles PfKey 38 Ips ec, AVISPA covers 86% (24 of the 28) of the Security Protocols listed in RFC 2316,RFC 3631, Auth-mech (plus very current ones) Total of more than 90 protocols Seoul, March, 2004 AVISPA IETF - saag

12 New Problems offer new Challenges Internet offers agent many identities – Location of adversaries – over the air – “safer” routes Many types of DoS attacks – user, ip, mac, tcp port, . What is “A”, “ID A”? flodding, bombing, starving, disrupting New types of security goals – DoS – key control, perfect forward secrecy, . – layered properties if attacker weak then guarantee DoS resilience confidentiality integrity if attacker strong then guarantee at least confidentiality integrity Seoul, March, 2004 AVISPA IETF - saag

13 Conclusions The standardisation organisations need us: – Avoid delays in the standardisation process – Avoid errors in deployed standards Help to restore the trust on e-commerce, privacy Automatic tools are needed – Fast evaluation of alternatives Our candidates cover: – all 5 IP layers – most (11) IP Areas – almost all security goals – 86% of the “recommended” IETF security Protocols – further information on http://www.tschofenig.com/avispa/ We still have many challenges ahead of us! Seoul, March, 2004 AVISPA IETF - saag