Secrecy, Group Creation

We lift Cardelli, Ghelli and Gordon's secrecy group creation operator [1] to a relative of the spicalculus that supports symmetric key cryptography, and show a natural extension of the associated type system. We then formulate a notion of secrecy preservation in the presence of cryptography, and prove that well-typed processes in the extended type system preserve secrecy of declared secrets, even in the presence of untyped opponents. 1 Organization We largely follow the outline of Cardelli, Ghelli and Gordon's paper on "Secrecy and Group Creation" [1],

• Type: Journal
• Year: 2000
• Where: ENTCS
• Authors: Luca Cardelli, Andy Gordon, Giorgio Ghelli
• Keywords: ENTCS 2000, Secrecy, Secrecy Group Creation, Type System