View Full Document

# SPi Calculus: Outline

View Full Document
View Full Document

13 views

Unformatted text preview:

SPi Calculus Outline What is it Basic SPi Calculus Notation Basic Example Example with Channel Establishment Example using Cryptography SPi Calculus What is it SPi Calculus is an executable model for the description and analysis of cryptographic protocols Spi Calculus is an extension to Pi Calculus SPi Calculus Processes Spi Calculus is made up of Processes When all the processes are combined we have a program or protocol SPi Calculus Processes Processes are defined as follows P some action our process does Where P is our process SPi Calculus Processes Processes can do many things They can create other processes They can send messages They can receive messages They can run other processes You can think of a process as the set of actions a principal takes Alice Bob Malory etc SPi Calculus Processes When processes send or receive messages they do this over channels SPi Calculus Basic Definitions Channels A channel is a named communications medium Channels can be restricted so that only certain processes can communicate on them SPi Calculus Basic Definitions Channel Example A B cAB Process A communicates to Process B through ChannelAB SPi Calculus Basic Definitions Unfortunately we can t just say Process A Listen on Channel AB for a Message M We have to use SPi Calculus Notation Pi Calc Basic Notation 1 Process Grammar Output Sequential Operator The above is how we state Output the message M on Channel C and then run process P Pi Calc Basic Notation 2 Process Grammar Input C x P Input the message x on the channel C and then run process P P will have access to x Pi Calc Basic Notation 3 Process Grammar Composition P Q A composition P Q behaves as processes P and Q running in parallel Each may interact with the other on channels known to both or with the outside world independently of the other Pi Calc Basic Notation 4 Process Grammar Restriction vn P A restriction vn P is a process that makes a new private name n and then behaves as P Note that n is restricted to P Pi

Unlocking...