Sökning: "pi-calculus"

Hittade 3 uppsatser innehållade ordet pi-calculus.

1. 1. Verification of security protocols with state in ProVerif : Avoiding false attacks when verifying freshness

   Master-uppsats, KTH/Skolan för datavetenskap och kommunikation (CSC)

   Författare :Pasi Saarinen; [2015]
   Nyckelord :formal verification ProVerif state counter applied pi calculus freshness security protocols;

   Sammanfattning : One of the issues when attempting to verify security properties of a protocol is how to model the protocol. We introduce a method for verifying event freshness in tools which use the applied π-calculus and are able to verify secrecy. Event freshness can be used to prove that a protocol never generates the same key twice. LÄS MER

3. 2. Algorithmic Analysis of Name-Bounded Programs : From Java programs to Petri Nets via π-calculus

   Master-uppsats, Blekinge Tekniska Högskola/Institutionen för programvaruteknik

   Författare :Matteo Settenvini; [2014]
   Nyckelord :pi-calculus; static verification; static analysis; concurrency; petri nets; name boundedness;

   Sammanfattning : Context. Name-bounded analysis is a type of static analysis that allows us to take a concurrent program, abstract away from it, and check for some interesting properties, such as deadlock-freedom, or watching the propagation of variables across different components or layers of the system. Objectives. LÄS MER

4. 3. Verifying Psi-calculi

   Magister-uppsats, Institutionen för informationsteknologi

   Författare :Johannes Åman Pohjola; [2010]
   Nyckelord :;

   Sammanfattning : Psi-calculi are mobile process calculi, parametrised with arbitrary nominal datatypes representing data, communication channels, assertions and conditions, as well as morphisms over those datatypes. The framework for psi-calculi has been formalised in the interactive theorem prover Isabelle, along with both strong and weak bisimulation. LÄS MER