Team Automata for Security Analysis of
Multicast/Broadcast Communication
Maurice ter Beek, Gabriele Lenzini, Marinella Petrocchi
 Istituto di Scienza e Tecnologia dell’Informazione
 Istituto di Informatica e Telematica
CNR - Pisa - Italy
WISP 2003
1st Workshop on Issues in Security and Petri nets
Eindhoven, 23 June 2003
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Outline
• multicast/broadcast technology and EMSS protocol
• Team Automata:
– informal definition
– example showing multicast/broadcast communication
– relation to Petri nets
– (in paper: instance of EMSS modelled by TA)
• formulate GNDC schema for security analysis in terms of TA
• conclusions and future work
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Multicast/Broadcast technology
Unicast: “sending a message through a point-to-point connection”
Broadcast: “flooding a message to all the connected recipients
using a single local transmit operation” (e.g. ordinary TV)
Multicast: “sending a message to a set of designated recipients
using a single local transmit operation” (e.g. pay-per-view TV)
M/B technology was born with the intent of saving resources
(e.g. bandwidth & CPU time) w.r.t. unicast
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Stream signature protocols
• send digital streams, i.e. long (potentially infinite)
sequences of bits, as packets
• guarantee authenticity and integrity
• aim at minimizing the computational cost of signing and
verifying packets
a sender broadcasts a continuous stream to a
possibly unbounded number of receivers
Features
receivers use information retrieved in earlier
packets to authenticate later packets (or v.v.)
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Tolerating packet loss
• digital streams are usually sent over the User Data
Protocol, an unreliable transport protocol
• this may cause packet loss, i.e. the stream may be
received incomplete by (a part of) the recipients
• a stream signature protocol tolerates packet loss if it still
allows a recipient to verify all packets that are not lost
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
The EMSS family of protocols
Efficient Multi-chained Stream Signature: family of protocols
to sign digital streams (Perrig et al., IEEE S&P 2000)
• basic idea: a hash of packet Pi is appended to packet Pi-1
(whose hash is in turn appended to packet Pi-2 , etc.)
• signature packet Psign at the end of the stream
• each packet contains multiple hashes of previous packets
and the signature packet contains hashes of multiple
packets
• multiple copies of the signature packet are sent
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
The (1,2) deterministic EMSS
Packet Pi-1
Packet Pi
Packet Pi+1
Mi-1
Mi
Mi+1
Hash(Pi-2)
Hash(Pi-3)
Hash(Pi-1)
Hash(Pi-2)
Hash(Pi)
Hash(Pi-1)
Packet PSign
...
Hash(PLAST)
Hash(PLAST-1)
SIGNATURE
Time / Number of packets
EMSS achieves (some) robustness against packet loss
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Team Automata
• model logical architecture of a design
• abstract from concrete data and actions
• describe behaviour in terms of:
– state-action diagram (automaton)
– role of actions (input, output, internal)
– synchronizations (simultaneous execution of actions)
• crux: automata composition
(Ellis, GROUP’97 & ter Beek et al., ECSCW’99 –> CSCW 2003)
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Multicast/broadcast communication in TA
S:
Ri:
p
a
p’
qi
a
qi’
broadcast TA |||{S,R1,…,Ri,…,Rn}:
(p,q1,…,qi,…,qn)
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
a
23 June 2003
(p’,q1’,…,qi’,…,qn’)
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Team Automata vs. Petri nets
• extension of I/O automata (Lynch + Tuttle, 1987)
• to visualize potential concurrency in TA: switch to vector TA
• VTA related to vector-labelled Petri nets, e.g. translation to
Individual Token Net Controllers (Keesmaat et al., 1990): a
particular type of state-machine decomposable nets
• more details in paper and its references
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
The insecure communication scenario
TR
private
send/receive
TR
TS
public send
public receive
TIC
eavesdrop
inject
TX
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
TR
23 June 2003
TP
TI
(Lynch, CSFW’99)
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
P  GNDC

(P)
iff X 


: (P || X) \C
C

Generalized Non-Deducibility on Compositions
(P)
(P)



A system specification P satisfies GNDC if the behaviour of P,

despite the presence of a hostile environment
,
C
appears to be the same (w.r.t. a behavioural relation )
as the expected (correct) behaviour (P of P
)
(Focardi-Martinelli, FM’99 & Focardi et al., ICALP’00)
D() bounded knowledge,
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
C
communication channels,
23 June 2003
|| composition, \ hiding
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
GNDC schema in terms of TA
Hostile environments:
C = { (Q, (out, inp, int), , I) | inp  C , out  C }
C = { X  C
| Idout (X)  (D())* }
Idout (X) = {   BT |   (out)*}
Observational behaviour:
C
OT = Id
preserve symbols
ext–C
(pres
ext-com
ext-com
(BT))
com communicating actions
GNDC in terms of TA:
C
hide actions C: unobservable
T  GNDC iff X 
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
C
C : Ohide
23 June 2003
C
C (|||{T,X})
 OT
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy
Conclusions
• TA naturally suited to model multicast/broadcast
communication
• GNDC schema reformulated in terms of TA
Future work
• use this new setting for the formal verification of
security properties for stream signature protocols
Istituto di Informatica e Telematica,
CNR – Pisa, Italy
23 June 2003
Istituto di Scienza e Tecnologie dell’Informazione
CNR – Pisa, Italy