Automated Protocol Verification
Computer Security and Networks
The material in this lecture is not relevant for the exam
1
The Applied Pi Calculus
Want formal languages to model security protocols so that automatic verification can be done
Here: use Applied Pi-Calculus, a suitable adaptation of process calculi
Intuition:
Processes correspond to agents (Alice, Bob, Mallory etc.) Sending messages modelled as communication in process calculus Attacker modelled as arbitrary process which runs in parallel with processes modelling Alice and Bob
Applied pi calculus: Grammar
Terms
Equational theory
M,N ::=
a,b,c,k,m,n,s,t,r,… name
x, y, z variable g(M1,…,Ml) function
adec(aenc(x, pk(y)), y) fst((x, y)) snd((x, y))
= x = x = y
Applied pi calculus: Grammar
Processes
P, Q, R ::= 0
processes
null process parallel comp. replication name restriction message input messageoutput
P | Q
!P
new n.P
in(u, x).P
out(u,M).P ifM=NthenPelseQ cond¡¯nl
Proverif
Several tools available for automated verification Consider a tool called Proverif (Blanchet 2001) Capabilities of ProVerif:
Reachability properties: Is a certain event reachable (eg leaking secret keys to the attacker)
Correspondence assertions: If event e has been executed, then event e¡ä has been previously been executed
Observational equivalences: The attacker cannot identify which one of two processes has been executed
Example:
Process 1: Voter A chooses option 1, voter B chooses option 2 Process 2: Voter A chooses option 2, voter B chooses option 1
Demo
Privacy in Mobile Telephony Systems
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Mobile phone communication
Mobile phones are carried by large parts of the population most of the time
Wireless communication always on Emitting their identity
Answer without agreement of their bearers
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Previous work on security of mobile phones
Content security, Integrity and Authentication
Weaknesses in cryptographic algorithms used (Biryutov et al. 2000)
Eavesdropping on mobile communication (Nohl et al. 2010)
Weaknesses in the authentication and key agreement protocol (Ahamdian et al. 2009, Arapinis et al. 2012)
Privacy
use paging procedure to locate mobile phone users (Foo Kune et al. 2012)
IMSI-catchers: force mobile phone to reveal identity (recognised weakness in the standard)
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Mobile phone privacy
Privacy is explicit goal of UMTS standard:
UMTS specification [3GPP TS 33.102 V9.3.0 (2010-10)] An intruder cannot deduce whether different services are delivered
to the same user.
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Tracking via mobile phones
Tracking of mobile phone user done in reality
Example: Market research companies use signal strength to track customers (eg. Smart Flow)
anonymous, but linkable.
No consent of mobile phone owner.
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Mobile phone identifiers
Every phone has unique identifier (IMSI)
If IMSI appears in cleartext, identification of mobile phone user would be easily possible
Problem recognised in the UMTS standard
temporary identifiers (TMSI) used which should be changed periodically
Talk is about correct usage of TMSIs.
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
TMSI reallocation
Initiated by the MS to update its location
MS unique identity stored in the SIM card: IMSI
The network assigns a temporary identity TMSI
A new TMSI is assigned during the location update
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
TMSI reallocation
Initiated by the MS to update its location
MS unique identity stored in the SIM card: IMSI
The network assigns a temporary identity TMSI
A new TMSI is assigned during the location update
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Problems with TMSI reallocation
1 TMSI reallocation rarely executed: Experimentally verified
2 Old keys for encrypting traffic are reused after TMSI-reallocation
Gives rise to protocol attack
Both issues make it possible to track mobile phone users
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Experimental Setup
Osmocom-BB project implements GSM mobile station controlled by host
Radio communication executed via flashed firmware on mobile phone
Can use wireshark to analyse the communication
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Experimental Setup, continued
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Experimental results
TMSI reallocation procedure rarely executed:
Same TMSI allocated for hours and even days
Observed for major operators in UK, France, Italy and Greece
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Experimental results, continued
Change of location area does not imply a change of TMSI Example: couch journey between different cities in the UK
First new TMSI assigned after about 45 min (53km)
Second new TMSI assigned after about 60 min (70km) However: location update procedure performed every 5 min (3km)
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Reuse of previous ciphering keys
Previously established keys are used for the TMSI reallocation procedure
Observed for major UK and Italian network operators
Gives rise to replay attack
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
TMSI reallocation protocol
MS Network
IMSI,oTMSI,CK IMSI,oTMSI,CK L3 MSG, oTMSI
Management of means for ciphering: CK established new nTMSI
{TMSI reall cmd, nTMSI, nLAI}rCK {TMSI reall complete}rCK
Deallocate oTMSI Deallocate oTMSI
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Replay Attack
MS v MitM Network IMSI,oTMSI,CK IMSI,oTMSI,CK
L3 MSG, oTMSI Management of means for ciphering
new nTMSI {TMSI reall cmd,nTMSI, LAI}rCK
Store TMSI reallocation command
{TMSI reall complete}rCK
Deallocate oTMSI Deallocate oTMSI
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
MS v MitM Network IMSI,oTMSI,CK IMSI,oTMSI,CK
next session
L3 MSG, nTMSI1 after k sessions
L3 MSG, nTMSIk Management of means for ciphering
Replay stored TMSI reall cmd
{TMSI reall cmd,nTMSI, LAI}rCK {TMSI reall complete}rCK
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Fix for replay attack
MS
IMSI , oTMSI , CK , SQNMS
Network
IMSI , oTMSI , CK , SQNSN
L3 MSG, oTMSI
Management of means for ciphering: CK established
new nTMSI {TMSI reall cmd, nTMSI, LAI, SQNSN}rCK
if SQNMS ¡Ü SQNSN
{TMSI reall complete}rCK
Deallocate oTMSI Deallocate oTMSI
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Privacy properties of fix
Have formally specified and verified privacy properties of fix Applied ¦Ð-calculus used for formalisation
Agents modelled as processes
communication between agents modelled as messages on channels
have terms and reduction rules corresponding to cryptographic primitives
nonces and private keys modelled by scope restriction of identifiers
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Desired privacy property formalised as unlinkability: Attacker cannot distinguish two scenarios
Formally:
¦Ídck.(!(Init|MS)|!SN) ¡Ö ¦Ídck.(!(Init|!MS)|!SN)
Have automated tool (Proverif) to verify such equivalences
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Modelling TMSI
Issue: How to handle TMSI (stored in phone memory)? Instance of global mutable state
Encoding of state in applied ¦Ð-calculus leads to large amount of false positives in Proverif
Solution: add mutable global state as primitive Leads to StatVerif
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Have shown following theorem
Theorem
Proof works by constructing suitable bisimulation
Key point: multiple sessions of same mobile phone can be simulated by multiple phones executing one session each
¦Ídck.(!(Init|MS)|!SN) ¡Ö ¦Ídck.(!(Init|!MS)|!SN)
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob
Conclusions
Temporary identifiers used by mobile phones are used incorrectly changed rarely
old ciphering keys are reused
Weaknesses make it possible to track mobile phone users Second problem can be fixed by not reusing keys
Based on a paper in Network and Distributed Systems Symposium 2014 by Arapinis, Mancini, Ritter and Ryan Privacy in Mob