Name
Abstract | ||
|---|---|---|
To provide privacy protection, cryptographic primitives are frequently applied to communication protocols in an open environment (e.g. the Internet). We call these protocols privacy enhancing protocols (PEPs) which constitute a class of cryptographic protocols. Proof of the security properties, in terms of the privacy compliance, of PEPs is desirable before they can be deployed. However, the traditional provable security approach, though well-established for proving the security of cryptographic primitives, is not applicable to PEPs. We apply the formal language of Coloured Petri Nets (CPNs) to construct an executable specification of a representative PEP, namely the Private Information Escrow Bound to Multiple Conditions Protocol (PIEMCP). Formal semantics of the CPN specification allow us to reason about various privacy properties of PIEMCP using state space analysis techniques. This investigation provides insights into the modelling and analysis of PEPs in general, and demonstrates the benefit of applying a CPN-based formal approach to the privacy compliance verification of PEPs. |
Year | Venue | Keywords |
|---|---|---|
2012 | Lecture Notes in Computer Science | cryptographic protocols,ctl |
Field | DocType | Volume |
Petri net,Formal language,Cryptographic protocol,Computer security,Computer science,Trusted Platform Module,Cryptographic primitive,Provable security,Communications protocol,Executable | Journal | 7400 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.45 |
References | Authors | |
8 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Suriadi Suriadi | 1 | 210 | 18.89 |
| Chun Ouyang | 2 | 850 | 43.82 |
| Ernest Foo | 3 | 276 | 28.76 |